%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : COM147+1 : TPTP v8.2.0. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n024.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 04:53:01 EDT 2024
% Result : Theorem 0.55s 1.03s
% Output : CNFRefutation 0.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : COM147+1 : TPTP v8.2.0. Released v6.4.0.
% 0.04/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n024.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu Jun 20 23:58:09 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.51/0.57 start to proof:theBenchmark
% 0.55/1.02 %-------------------------------------------
% 0.55/1.02 % File :CSE---1.7
% 0.55/1.02 % Problem :theBenchmark
% 0.55/1.02 % Transform :cnf
% 0.55/1.02 % Format :tptp:raw
% 0.55/1.02 % Command :java -jar mcs_scs.jar %d %s
% 0.55/1.02
% 0.55/1.02 % Result :Theorem 0.130000s
% 0.55/1.02 % Output :CNFRefutation 0.130000s
% 0.55/1.02 %-------------------------------------------
% 0.55/1.03 %------------------------------------------------------------------------------
% 0.55/1.03 % File : COM147+1 : TPTP v8.2.0. Released v6.4.0.
% 0.55/1.03 % Domain : Computing Theory
% 0.55/1.03 % Problem : T-Progress-T-abs step in progress/preservation proof
% 0.55/1.03 % Version : Augmented > Especial.
% 0.55/1.03 % English : This problem is a step within the proof of progress and
% 0.55/1.03 % preservation for the standard type system for the simply-typed
% 0.55/1.03 % lambda calculus.
% 0.55/1.03
% 0.55/1.03 % Refs : [Pie02] Pierce (2002), Programming Languages
% 0.55/1.03 % : [Gre15] Grewe (2015), Email to Geoff Sutcliffe
% 0.55/1.03 % : [GE+15] Grewe et al. (2015), Type Systems for the Masses: Deri
% 0.55/1.03 % Source : [Gre15]
% 0.55/1.03 % Names : Progress-T-Progress-T-abs [Gre15]
% 0.55/1.03
% 0.55/1.03 % Status : Theorem
% 0.55/1.03 % Rating : 0.17 v8.2.0, 0.14 v7.5.0, 0.16 v7.4.0, 0.17 v7.3.0, 0.14 v7.1.0, 0.17 v7.0.0, 0.23 v6.4.0
% 0.55/1.03 % Syntax : Number of formulae : 58 ( 6 unt; 0 def)
% 0.55/1.03 % Number of atoms : 297 ( 230 equ)
% 0.55/1.03 % Maximal formula atoms : 33 ( 5 avg)
% 0.55/1.03 % Number of connectives : 278 ( 39 ~; 17 |; 124 &)
% 0.55/1.03 % ( 0 <=>; 98 =>; 0 <=; 0 <~>)
% 0.55/1.03 % Maximal formula depth : 23 ( 8 avg)
% 0.55/1.03 % Maximal term depth : 5 ( 1 avg)
% 0.55/1.03 % Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% 0.55/1.03 % Number of functors : 17 ( 17 usr; 4 con; 0-3 aty)
% 0.55/1.03 % Number of variables : 323 ( 253 !; 70 ?)
% 0.55/1.03 % SPC : FOF_THM_RFO_SEQ
% 0.55/1.03
% 0.55/1.03 % Comments : Generated by Veritas: https://github.com/stg-tud/type-pragmatics
% 0.55/1.03 % : This is an expanded version of the original, with most axioms
% 0.55/1.03 % combined into COM001+0.ax.
% 0.55/1.03 %------------------------------------------------------------------------------
% 0.55/1.03 include('Axioms/COM001+0.ax').
% 0.55/1.03 %------------------------------------------------------------------------------
% 0.55/1.03 fof('T-Weak',axiom,
% 0.55/1.03 ! [Vx,VS,VC,Ve,VT] :
% 0.55/1.03 ( ( vlookup(Vx,VC) = vnoType
% 0.55/1.03 & vtcheck(VC,Ve,VT) )
% 0.55/1.03 => vtcheck(vbind(Vx,VS,VC),Ve,VT) ) ).
% 0.55/1.03
% 0.55/1.03 fof('T-Strong',axiom,
% 0.55/1.03 ! [Vx,VS,VC,Ve,VT] :
% 0.55/1.03 ( ( ~ visFreeVar(Vx,Ve)
% 0.55/1.03 & vtcheck(vbind(Vx,VS,VC),Ve,VT) )
% 0.55/1.03 => vtcheck(VC,Ve,VT) ) ).
% 0.55/1.03
% 0.55/1.03 fof('T-Progress-T-abs-IH',axiom,
% 0.55/1.03 ! [VT] :
% 0.55/1.03 ( ( vtcheck(vempty,ve1,VT)
% 0.55/1.03 & ~ visValue(ve1) )
% 0.55/1.03 => ? [Veout] : vreduce(ve1) = vsomeExp(Veout) ) ).
% 0.55/1.03
% 0.55/1.03 fof('T-Progress-T-abs',conjecture,
% 0.55/1.03 ! [VTin,Vx,VS] :
% 0.55/1.03 ( ( vtcheck(vempty,vabs(Vx,VS,ve1),VTin)
% 0.55/1.03 & ~ visValue(vabs(Vx,VS,ve1)) )
% 0.55/1.03 => ? [Veout] : vreduce(vabs(Vx,VS,ve1)) = vsomeExp(Veout) ) ).
% 0.55/1.03
% 0.55/1.03 %------------------------------------------------------------------------------
% 0.55/1.03 %-------------------------------------------
% 0.55/1.03 % Proof found
% 0.55/1.03 % SZS status Theorem for theBenchmark
% 0.55/1.03 % SZS output start Proof
% 0.55/1.03 %ClaNum:688(EqnAxiom:277)
% 0.55/1.03 %VarNum:8970(SingletonVarNum:1325)
% 0.55/1.03 %MaxLitNum:8
% 0.55/1.03 %MaxfuncDepth:4
% 0.55/1.03 %SharedTerms:16
% 0.55/1.03 %goalClause: 278 285 286
% 0.55/1.03 %singleGoalClaCount:3
% 0.55/1.03 [278]P1(a1,f31(a2,a29,a30),a3)
% 0.55/1.03 [285]~P2(f31(a2,a29,a30))
% 0.55/1.03 [279]~E(f85(x2791),a86)
% 0.55/1.03 [280]~E(f92(x2801),a87)
% 0.55/1.03 [286]~E(f93(f31(a2,a29,a30)),f92(x2861))
% 0.55/1.03 [281]~E(f94(x2811),f82(x2812,x2813))
% 0.55/1.03 [282]~E(f83(x2821,x2822,x2823),a1)
% 0.55/1.03 [283]~E(f94(x2831),f31(x2832,x2833,x2834))
% 0.55/1.03 [284]~E(f31(x2841,x2842,x2843),f82(x2844,x2845))
% 0.55/1.03 [287]~P3(x2871)+~E(x2871,a86)
% 0.55/1.03 [288]~P4(x2881)+~E(x2881,a87)
% 0.55/1.03 [289]P3(x2891)+~E(x2891,f85(x2892))
% 0.55/1.03 [290]P4(x2901)+~E(x2901,f92(x2902))
% 0.55/1.03 [291]E(x2911,x2912)+~E(f94(x2911),f94(x2912))
% 0.55/1.03 [292]E(x2921,x2922)+~E(f85(x2921),f85(x2922))
% 0.55/1.03 [293]E(x2931,x2932)+~E(f92(x2931),f92(x2932))
% 0.55/1.03 [294]~P2(x2941)+~E(x2941,f94(x2942))
% 0.55/1.03 [300]~P9(x3002,x3001)+~E(f90(x3001),x3002)
% 0.55/1.03 [301]~P2(x3011)+~E(x3011,f82(x3012,x3013))
% 0.55/1.03 [316]P1(x3161,f94(x3162),x3163)+~E(f91(x3162,x3161),f85(x3163))
% 0.55/1.03 [304]E(x3041,x3042)+~E(f82(x3043,x3041),f82(x3044,x3042))
% 0.55/1.03 [305]E(x3051,x3052)+~E(f82(x3051,x3053),f82(x3052,x3054))
% 0.55/1.03 [306]E(x3061,x3062)+~E(f84(x3063,x3061),f84(x3064,x3062))
% 0.55/1.03 [307]E(x3071,x3072)+~E(f84(x3071,x3073),f84(x3072,x3074))
% 0.55/1.03 [319]P2(x3191)+~E(x3191,f31(x3192,x3193,x3194))
% 0.55/1.03 [428]~P1(f83(x4282,x4283,x4281),x4284,x4285)+P1(x4281,f31(x4282,x4283,x4284),f84(x4283,x4285))
% 0.55/1.03 [353]E(x3531,x3532)+~E(f31(x3533,x3534,x3531),f31(x3535,x3536,x3532))
% 0.55/1.03 [354]E(x3541,x3542)+~E(f31(x3543,x3541,x3544),f31(x3545,x3542,x3546))
% 0.55/1.03 [355]E(x3551,x3552)+~E(f31(x3551,x3553,x3554),f31(x3552,x3555,x3556))
% 0.55/1.03 [356]E(x3561,x3562)+~E(f83(x3563,x3564,x3561),f83(x3565,x3566,x3562))
% 0.55/1.03 [357]E(x3571,x3572)+~E(f83(x3573,x3571,x3574),f83(x3575,x3572,x3576))
% 0.55/1.03 [358]E(x3581,x3582)+~E(f83(x3581,x3583,x3584),f83(x3582,x3585,x3586))
% 0.55/1.03 [317]~P1(a1,a30,x3171)+E(f93(a30),f92(a19))+P2(a30)
% 0.55/1.03 [298]P5(x2981,x2982)+~E(f93(x2982),x2981)+E(x2981,a87)
% 0.55/1.03 [312]P5(x3121,x3122)+~E(f93(x3122),x3121)+~P4(f18(x3122,x3121))
% 0.55/1.03 [310]P5(x3102,x3101)+~E(f93(x3101),x3102)+E(f93(f4(x3101,x3102)),f18(x3101,x3102))
% 0.55/1.03 [318]P5(x3182,x3181)+~E(f93(x3181),x3182)+E(f82(f4(x3181,x3182),f5(x3181,x3182)),x3181)
% 0.55/1.03 [295]E(x2951,a87)+~E(x2951,f93(x2952))+~E(x2952,f94(x2953))
% 0.55/1.03 [296]E(x2961,x2962)+~E(x2963,f85(x2961))+~E(x2962,f88(x2963))
% 0.55/1.03 [297]E(x2971,x2972)+~E(x2973,f92(x2971))+~E(x2972,f89(x2973))
% 0.55/1.03 [460]P7(x4604,x4603,x4602,x4601)+~E(f95(x4601,x4602,x4603),x4604)+E(f7(x4601,x4602,x4603,x4604),x4601)
% 0.55/1.03 [461]P7(x4614,x4613,x4612,x4611)+~E(f95(x4611,x4612,x4613),x4614)+E(f10(x4611,x4612,x4613,x4614),x4612)
% 0.55/1.03 [498]~P8(x4984,x4983,x4982,x4981)+E(f42(x4981,x4982,x4983,x4984),x4982)+E(f39(x4981,x4982,x4983,x4984),x4984)
% 0.55/1.03 [499]~P8(x4994,x4993,x4992,x4991)+E(f44(x4991,x4992,x4993,x4994),x4991)+E(f39(x4991,x4992,x4993,x4994),x4994)
% 0.55/1.03 [500]~P8(x5004,x5003,x5002,x5001)+E(f42(x5001,x5002,x5003,x5004),x5002)+E(f40(x5001,x5002,x5003,x5004),x5001)
% 0.55/1.03 [501]~P8(x5014,x5013,x5012,x5011)+E(f44(x5011,x5012,x5013,x5014),x5011)+E(f39(x5011,x5012,x5013,x5014),x5012)
% 0.55/1.03 [502]~P8(x5024,x5023,x5022,x5021)+E(f44(x5021,x5022,x5023,x5024),x5021)+E(f40(x5021,x5022,x5023,x5024),x5021)
% 0.55/1.03 [503]~P8(x5034,x5033,x5032,x5031)+E(f42(x5031,x5032,x5033,x5034),x5032)+E(f39(x5031,x5032,x5033,x5034),x5032)
% 0.55/1.03 [515]P7(x5151,x5152,x5153,x5154)+~E(f95(x5154,x5153,x5152),x5151)+~E(f8(x5154,x5153,x5152,x5151),f7(x5154,x5153,x5152,x5151))
% 0.55/1.03 [517]~P8(x5174,x5173,x5172,x5171)+E(f41(x5171,x5172,x5173,x5174),f40(x5171,x5172,x5173,x5174))+E(f42(x5171,x5172,x5173,x5174),x5172)
% 0.55/1.03 [518]~P8(x5184,x5183,x5182,x5181)+E(f41(x5181,x5182,x5183,x5184),f40(x5181,x5182,x5183,x5184))+E(f44(x5181,x5182,x5183,x5184),x5181)
% 0.55/1.03 [547]~P8(x5474,x5473,x5472,x5471)+~E(f45(x5471,x5472,x5473,x5474),f44(x5471,x5472,x5473,x5474))+E(f39(x5471,x5472,x5473,x5474),x5474)
% 0.55/1.03 [548]~P8(x5484,x5483,x5482,x5481)+~E(f45(x5481,x5482,x5483,x5484),f44(x5481,x5482,x5483,x5484))+E(f39(x5481,x5482,x5483,x5484),x5482)
% 0.55/1.03 [549]~P8(x5494,x5493,x5492,x5491)+~E(f45(x5491,x5492,x5493,x5494),f44(x5491,x5492,x5493,x5494))+E(f40(x5491,x5492,x5493,x5494),x5491)
% 0.55/1.03 [555]~P8(x5554,x5553,x5552,x5551)+~E(f45(x5551,x5552,x5553,x5554),f44(x5551,x5552,x5553,x5554))+E(f41(x5551,x5552,x5553,x5554),f40(x5551,x5552,x5553,x5554))
% 0.55/1.03 [558]P7(x5581,x5582,x5583,x5584)+~E(f95(x5584,x5583,x5582),x5581)+~P9(f8(x5584,x5583,x5582,x5581),f10(x5584,x5583,x5582,x5581))
% 0.55/1.03 [520]~P8(x5204,x5203,x5202,x5201)+E(f39(x5201,x5202,x5203,x5204),x5204)+E(f94(f45(x5201,x5202,x5203,x5204)),x5203)
% 0.55/1.03 [521]~P8(x5214,x5213,x5212,x5211)+E(f39(x5211,x5212,x5213,x5214),x5212)+E(f94(f45(x5211,x5212,x5213,x5214)),x5214)
% 0.55/1.04 [522]~P8(x5224,x5223,x5222,x5221)+E(f39(x5221,x5222,x5223,x5224),x5222)+E(f94(f45(x5221,x5222,x5223,x5224)),x5223)
% 0.55/1.04 [523]~P8(x5234,x5233,x5232,x5231)+E(f40(x5231,x5232,x5233,x5234),x5231)+E(f94(f45(x5231,x5232,x5233,x5234)),x5234)
% 0.55/1.04 [524]~P8(x5244,x5243,x5242,x5241)+E(f40(x5241,x5242,x5243,x5244),x5241)+E(f94(f45(x5241,x5242,x5243,x5244)),x5243)
% 0.55/1.04 [525]~P8(x5254,x5253,x5252,x5251)+E(f39(x5251,x5252,x5253,x5254),x5254)+E(f94(f45(x5251,x5252,x5253,x5254)),x5254)
% 0.55/1.04 [526]~P8(x5264,x5263,x5262,x5261)+E(f42(x5261,x5262,x5263,x5264),x5262)+E(f94(f41(x5261,x5262,x5263,x5264)),x5263)
% 0.55/1.04 [527]~P8(x5274,x5273,x5272,x5271)+E(f44(x5271,x5272,x5273,x5274),x5271)+E(f94(f41(x5271,x5272,x5273,x5274)),x5273)
% 0.55/1.04 [533]~P8(x5334,x5333,x5332,x5331)+E(f41(x5331,x5332,x5333,x5334),f40(x5331,x5332,x5333,x5334))+E(f94(f45(x5331,x5332,x5333,x5334)),x5334)
% 0.55/1.04 [534]~P8(x5344,x5343,x5342,x5341)+E(f41(x5341,x5342,x5343,x5344),f40(x5341,x5342,x5343,x5344))+E(f94(f45(x5341,x5342,x5343,x5344)),x5343)
% 0.55/1.04 [543]~P8(x5434,x5433,x5432,x5431)+E(f94(f45(x5431,x5432,x5433,x5434)),x5434)+E(f94(f41(x5431,x5432,x5433,x5434)),x5433)
% 0.55/1.04 [544]~P8(x5444,x5443,x5442,x5441)+E(f94(f45(x5441,x5442,x5443,x5444)),x5443)+E(f94(f41(x5441,x5442,x5443,x5444)),x5443)
% 0.55/1.04 [556]~P8(x5564,x5563,x5562,x5561)+~E(f45(x5561,x5562,x5563,x5564),f44(x5561,x5562,x5563,x5564))+E(f94(f41(x5561,x5562,x5563,x5564)),x5563)
% 0.55/1.04 [557]P7(x5574,x5573,x5572,x5571)+~E(f95(x5571,x5572,x5573),x5574)+E(f31(f8(x5571,x5572,x5573,x5574),f9(x5571,x5572,x5573,x5574),f12(x5571,x5572,x5573,x5574)),x5573)
% 0.55/1.04 [620]P7(x6204,x6203,x6202,x6201)+~E(f95(x6201,x6202,x6203),x6204)+E(f31(f8(x6201,x6202,x6203,x6204),f9(x6201,x6202,x6203,x6204),f95(f7(x6201,x6202,x6203,x6204),f10(x6201,x6202,x6203,x6204),f12(x6201,x6202,x6203,x6204))),x6204)
% 0.55/1.04 [320]E(x3201,a87)+~E(x3201,f93(x3202))+~E(x3202,f31(x3203,x3204,x3205))
% 0.55/1.04 [342]P5(x3421,x3422)+~E(f93(x3422),x3421)+~E(f4(x3422,x3421),f31(x3423,x3424,x3425))
% 0.55/1.04 [384]~P1(x3843,x3844,x3845)+P1(f83(x3841,x3842,x3843),x3844,x3845)+~E(f91(x3841,x3843),a86)
% 0.55/1.04 [390]~P1(x3901,x3903,x3905)+~P1(x3901,x3902,f84(x3905,x3904))+P1(x3901,f82(x3902,x3903),x3904)
% 0.55/1.04 [399]P9(x3991,x3992)+P1(x3993,x3992,x3994)+~P1(f83(x3991,x3995,x3993),x3992,x3994)
% 0.55/1.04 [478]~E(x4781,x4786)+P1(f83(x4781,x4782,x4783),x4784,x4785)+~P1(f83(x4781,x4782,f83(x4786,x4787,x4783)),x4784,x4785)
% 0.55/1.04 [508]E(x5081,x5082)+~P1(f83(x5081,x5084,f83(x5082,x5083,x5085)),x5086,x5087)+P1(f83(x5082,x5083,f83(x5081,x5084,x5085)),x5086,x5087)
% 0.55/1.04 [311]~P5(x3111,x3112)+P6(x3111,x3112)+E(x3111,a87)+P4(f32(x3112,x3111))
% 0.55/1.04 [315]~P6(x3151,x3152)+E(x3151,a87)+P4(f35(x3152,x3151))+P2(f34(x3152,x3151))
% 0.55/1.04 [323]~P6(x3231,x3232)+E(x3231,a87)+~P4(f68(x3232,x3231))+P4(f35(x3232,x3231))
% 0.55/1.04 [329]~P5(x3291,x3292)+P6(x3291,x3292)+P4(f32(x3292,x3291))+~P2(f71(x3292,x3291))
% 0.55/1.04 [330]~P5(x3301,x3302)+P6(x3301,x3302)+P4(f32(x3302,x3301))+~P4(f72(x3302,x3301))
% 0.55/1.04 [314]P6(x3141,x3142)+~P5(x3141,x3142)+E(x3141,a87)+E(f93(f33(x3142,x3141)),f32(x3142,x3141))
% 0.55/1.04 [321]~P6(x3211,x3212)+E(x3211,a87)+P2(f34(x3212,x3211))+E(f93(f36(x3212,x3211)),f35(x3212,x3211))
% 0.55/1.04 [322]~P6(x3221,x3222)+E(x3221,a87)+P4(f35(x3222,x3221))+E(f93(f34(x3222,x3221)),f68(x3222,x3221))
% 0.55/1.04 [324]P6(x3241,x3242)+~P5(x3241,x3242)+E(x3241,a87)+E(f82(f33(x3242,x3241),f78(x3242,x3241)),x3242)
% 0.55/1.04 [327]P6(x3272,x3271)+~P5(x3272,x3271)+P4(f32(x3271,x3272))+E(f93(f71(x3271,x3272)),f72(x3271,x3272))
% 0.55/1.04 [328]~P6(x3281,x3282)+E(x3281,a87)+E(f93(f34(x3282,x3281)),f68(x3282,x3281))+E(f93(f36(x3282,x3281)),f35(x3282,x3281))
% 0.55/1.04 [331]~P6(x3311,x3312)+E(x3311,a87)+~P4(f68(x3312,x3311))+E(f93(f36(x3312,x3311)),f35(x3312,x3311))
% 0.55/1.04 [335]P6(x3352,x3351)+~P5(x3352,x3351)+E(f93(f33(x3351,x3352)),f32(x3351,x3352))+E(f93(f71(x3351,x3352)),f72(x3351,x3352))
% 0.55/1.04 [337]P6(x3372,x3371)+~P5(x3372,x3371)+~P2(f71(x3371,x3372))+E(f93(f33(x3371,x3372)),f32(x3371,x3372))
% 0.57/1.04 [338]P6(x3382,x3381)+~P5(x3382,x3381)+~P4(f72(x3381,x3382))+E(f93(f33(x3381,x3382)),f32(x3381,x3382))
% 0.57/1.04 [350]P6(x3502,x3501)+~P5(x3502,x3501)+E(f82(f33(x3501,x3502),f78(x3501,x3502)),x3501)+E(f93(f71(x3501,x3502)),f72(x3501,x3502))
% 0.57/1.04 [351]P6(x3512,x3511)+~P5(x3512,x3511)+~P2(f71(x3511,x3512))+E(f82(f33(x3511,x3512),f78(x3511,x3512)),x3511)
% 0.57/1.04 [352]P6(x3522,x3521)+~P5(x3522,x3521)+~P4(f72(x3521,x3522))+E(f82(f33(x3521,x3522),f78(x3521,x3522)),x3521)
% 0.57/1.04 [404]~P6(x4041,x4042)+E(x4041,a87)+P2(f34(x4042,x4041))+E(f82(f31(f65(x4042,x4041),f66(x4042,x4041),f67(x4042,x4041)),f36(x4042,x4041)),x4042)
% 0.57/1.04 [405]~P6(x4051,x4052)+E(x4051,a87)+P4(f35(x4052,x4051))+E(f82(f31(f70(x4052,x4051),f69(x4052,x4051),f73(x4052,x4051)),f34(x4052,x4051)),x4052)
% 0.57/1.04 [415]P6(x4152,x4151)+~P5(x4152,x4151)+P4(f32(x4151,x4152))+E(f82(f31(f75(x4151,x4152),f76(x4151,x4152),f77(x4151,x4152)),f71(x4151,x4152)),x4151)
% 0.57/1.04 [416]~P6(x4161,x4162)+E(x4161,a87)+E(f82(f31(f70(x4162,x4161),f69(x4162,x4161),f73(x4162,x4161)),f34(x4162,x4161)),x4162)+E(f93(f36(x4162,x4161)),f35(x4162,x4161))
% 0.57/1.04 [417]~P6(x4171,x4172)+E(x4171,a87)+E(f82(f31(f65(x4172,x4171),f66(x4172,x4171),f67(x4172,x4171)),f36(x4172,x4171)),x4172)+E(f93(f34(x4172,x4171)),f68(x4172,x4171))
% 0.57/1.04 [418]~P6(x4181,x4182)+E(x4181,a87)+~P4(f68(x4182,x4181))+E(f82(f31(f65(x4182,x4181),f66(x4182,x4181),f67(x4182,x4181)),f36(x4182,x4181)),x4182)
% 0.57/1.04 [419]P6(x4192,x4191)+~P5(x4192,x4191)+E(f82(f31(f75(x4191,x4192),f76(x4191,x4192),f77(x4191,x4192)),f71(x4191,x4192)),x4191)+E(f93(f33(x4191,x4192)),f32(x4191,x4192))
% 0.57/1.04 [425]P6(x4252,x4251)+~P5(x4252,x4251)+E(f82(f31(f75(x4251,x4252),f76(x4251,x4252),f77(x4251,x4252)),f71(x4251,x4252)),x4251)+E(f82(f33(x4251,x4252),f78(x4251,x4252)),x4251)
% 0.57/1.04 [467]~P6(x4671,x4672)+E(x4671,a87)+E(f82(f31(f70(x4672,x4671),f69(x4672,x4671),f73(x4672,x4671)),f34(x4672,x4671)),x4672)+E(f82(f31(f65(x4672,x4671),f66(x4672,x4671),f67(x4672,x4671)),f36(x4672,x4671)),x4672)
% 0.57/1.04 [372]P6(x3721,x3722)+~P5(x3721,x3722)+E(x3721,a87)+E(f92(f82(f89(f32(x3722,x3721)),f78(x3722,x3721))),x3721)
% 0.57/1.04 [387]P6(x3872,x3871)+~P5(x3872,x3871)+E(f93(f71(x3871,x3872)),f72(x3871,x3872))+E(f92(f82(f89(f32(x3871,x3872)),f78(x3871,x3872))),x3872)
% 0.57/1.04 [388]P6(x3882,x3881)+~P5(x3882,x3881)+~P2(f71(x3881,x3882))+E(f92(f82(f89(f32(x3881,x3882)),f78(x3881,x3882))),x3882)
% 0.57/1.04 [389]P6(x3892,x3891)+~P5(x3892,x3891)+~P4(f72(x3891,x3892))+E(f92(f82(f89(f32(x3891,x3892)),f78(x3891,x3892))),x3892)
% 0.57/1.04 [398]~P6(x3981,x3982)+E(x3981,a87)+P4(f35(x3982,x3981))+E(f92(f95(f70(x3982,x3981),f34(x3982,x3981),f73(x3982,x3981))),x3981)
% 0.57/1.04 [401]~P6(x4011,x4012)+E(x4011,a87)+E(f93(f36(x4012,x4011)),f35(x4012,x4011))+E(f92(f95(f70(x4012,x4011),f34(x4012,x4011),f73(x4012,x4011))),x4011)
% 0.57/1.04 [455]P6(x4552,x4551)+~P5(x4552,x4551)+E(f82(f31(f75(x4551,x4552),f76(x4551,x4552),f77(x4551,x4552)),f71(x4551,x4552)),x4551)+E(f92(f82(f89(f32(x4551,x4552)),f78(x4551,x4552))),x4552)
% 0.57/1.04 [462]~P6(x4621,x4622)+E(x4621,a87)+E(f82(f31(f65(x4622,x4621),f66(x4622,x4621),f67(x4622,x4621)),f36(x4622,x4621)),x4622)+E(f92(f95(f70(x4622,x4621),f34(x4622,x4621),f73(x4622,x4621))),x4621)
% 0.57/1.04 [474]~P6(x4741,x4742)+E(x4741,a87)+P2(f34(x4742,x4741))+E(f92(f82(f31(f65(x4742,x4741),f66(x4742,x4741),f67(x4742,x4741)),f89(f35(x4742,x4741)))),x4741)
% 0.57/1.04 [476]~P6(x4761,x4762)+E(x4761,a87)+E(f93(f34(x4762,x4761)),f68(x4762,x4761))+E(f92(f82(f31(f65(x4762,x4761),f66(x4762,x4761),f67(x4762,x4761)),f89(f35(x4762,x4761)))),x4761)
% 0.57/1.04 [477]~P6(x4771,x4772)+E(x4771,a87)+~P4(f68(x4772,x4771))+E(f92(f82(f31(f65(x4772,x4771),f66(x4772,x4771),f67(x4772,x4771)),f89(f35(x4772,x4771)))),x4771)
% 0.57/1.04 [507]~P6(x5071,x5072)+E(x5071,a87)+E(f92(f95(f70(x5072,x5071),f34(x5072,x5071),f73(x5072,x5071))),x5071)+E(f92(f82(f31(f65(x5072,x5071),f66(x5072,x5071),f67(x5072,x5071)),f89(f35(x5072,x5071)))),x5071)
% 0.57/1.04 [512]~P6(x5121,x5122)+E(x5121,a87)+E(f82(f31(f70(x5122,x5121),f69(x5122,x5121),f73(x5122,x5121)),f34(x5122,x5121)),x5122)+E(f92(f82(f31(f65(x5122,x5121),f66(x5122,x5121),f67(x5122,x5121)),f89(f35(x5122,x5121)))),x5121)
% 0.57/1.04 [345]E(f79(x3452,x3453,x3451),x3452)+~E(f91(x3452,x3453),x3451)+E(f38(x3452,x3453,x3451),x3452)+E(x3451,a86)
% 0.57/1.04 [346]E(f79(x3462,x3461,x3463),x3462)+~E(f91(x3462,x3461),x3463)+E(f38(x3462,x3461,x3463),x3462)+E(x3461,a1)
% 0.57/1.04 [360]E(f43(x3602,x3603,x3601),f38(x3602,x3603,x3601))+~E(f91(x3602,x3603),x3601)+E(f79(x3602,x3603,x3601),x3602)+E(x3601,a86)
% 0.57/1.04 [361]E(f43(x3612,x3611,x3613),f38(x3612,x3611,x3613))+~E(f91(x3612,x3611),x3613)+E(f79(x3612,x3611,x3613),x3612)+E(x3611,a1)
% 0.57/1.04 [362]E(f38(x3621,x3622,x3623),x3621)+E(f79(x3621,x3622,x3623),x3621)+~E(f91(x3621,x3622),x3623)+E(f6(x3621,x3622,x3623),x3621)
% 0.57/1.04 [374]E(f79(x3741,x3742,x3743),x3741)+E(f43(x3741,x3742,x3743),f38(x3741,x3742,x3743))+~E(f91(x3741,x3742),x3743)+E(f6(x3741,x3742,x3743),x3741)
% 0.57/1.04 [379]~E(f91(x3792,x3793),x3791)+~E(f80(x3792,x3793,x3791),f79(x3792,x3793,x3791))+E(f38(x3792,x3793,x3791),x3792)+E(x3791,a86)
% 0.57/1.04 [380]~E(f91(x3802,x3801),x3803)+~E(f80(x3802,x3801,x3803),f79(x3802,x3801,x3803))+E(f38(x3802,x3801,x3803),x3802)+E(x3801,a1)
% 0.57/1.04 [391]~E(f91(x3912,x3913),x3911)+~E(f80(x3912,x3913,x3911),f79(x3912,x3913,x3911))+E(f43(x3912,x3913,x3911),f38(x3912,x3913,x3911))+E(x3911,a86)
% 0.57/1.04 [392]~E(f91(x3922,x3921),x3923)+~E(f80(x3922,x3921,x3923),f79(x3922,x3921,x3923))+E(f43(x3922,x3921,x3923),f38(x3922,x3921,x3923))+E(x3921,a1)
% 0.57/1.04 [393]E(f38(x3931,x3932,x3933),x3931)+~E(f91(x3931,x3932),x3933)+~E(f80(x3931,x3932,x3933),f79(x3931,x3932,x3933))+E(f6(x3931,x3932,x3933),x3931)
% 0.57/1.04 [406]E(f43(x4061,x4062,x4063),f38(x4061,x4062,x4063))+~E(f91(x4061,x4062),x4063)+~E(f80(x4061,x4062,x4063),f79(x4061,x4062,x4063))+E(f6(x4061,x4062,x4063),x4061)
% 0.57/1.04 [365]~E(f91(x3652,x3653),x3651)+E(f79(x3652,x3653,x3651),x3652)+E(x3651,a86)+E(f85(f61(x3652,x3653,x3651)),x3651)
% 0.57/1.04 [366]~E(f91(x3662,x3661),x3663)+E(f79(x3662,x3661,x3663),x3662)+E(x3661,a1)+E(f85(f61(x3662,x3661,x3663)),x3663)
% 0.57/1.04 [376]E(f79(x3761,x3762,x3763),x3761)+~E(f91(x3761,x3762),x3763)+E(f6(x3761,x3762,x3763),x3761)+E(f85(f61(x3761,x3762,x3763)),x3763)
% 0.57/1.04 [394]~E(f91(x3942,x3943),x3941)+~E(f80(x3942,x3943,x3941),f79(x3942,x3943,x3941))+E(x3941,a86)+E(f85(f61(x3942,x3943,x3941)),x3941)
% 0.57/1.04 [395]~E(f91(x3952,x3951),x3953)+~E(f80(x3952,x3951,x3953),f79(x3952,x3951,x3953))+E(x3951,a1)+E(f85(f61(x3952,x3951,x3953)),x3953)
% 0.57/1.04 [396]~E(f91(x3962,x3961),x3963)+E(f38(x3962,x3961,x3963),x3962)+E(x3961,a1)+E(f91(f79(x3962,x3961,x3963),f81(x3962,x3961,x3963)),x3963)
% 0.57/1.04 [397]~E(f91(x3972,x3973),x3971)+E(f38(x3972,x3973,x3971),x3972)+E(x3971,a86)+E(f91(f79(x3972,x3973,x3971),f81(x3972,x3973,x3971)),x3971)
% 0.57/1.04 [408]~E(f91(x4081,x4082),x4083)+~E(f80(x4081,x4082,x4083),f79(x4081,x4082,x4083))+E(f6(x4081,x4082,x4083),x4081)+E(f85(f61(x4081,x4082,x4083)),x4083)
% 0.57/1.04 [409]~E(f91(x4092,x4091),x4093)+E(f43(x4092,x4091,x4093),f38(x4092,x4091,x4093))+E(x4091,a1)+E(f91(f79(x4092,x4091,x4093),f81(x4092,x4091,x4093)),x4093)
% 0.57/1.04 [410]~E(f91(x4102,x4103),x4101)+E(f43(x4102,x4103,x4101),f38(x4102,x4103,x4101))+E(x4101,a86)+E(f91(f79(x4102,x4103,x4101),f81(x4102,x4103,x4101)),x4101)
% 0.57/1.04 [411]E(f38(x4111,x4112,x4113),x4111)+~E(f91(x4111,x4112),x4113)+E(f6(x4111,x4112,x4113),x4111)+E(f91(f79(x4111,x4112,x4113),f81(x4111,x4112,x4113)),x4113)
% 0.57/1.04 [412]~E(f91(x4122,x4121),x4123)+E(x4121,a1)+E(f91(f79(x4122,x4121,x4123),f81(x4122,x4121,x4123)),x4123)+E(f85(f61(x4122,x4121,x4123)),x4123)
% 0.57/1.04 [413]~E(f91(x4132,x4133),x4131)+E(x4131,a86)+E(f91(f79(x4132,x4133,x4131),f81(x4132,x4133,x4131)),x4131)+E(f85(f61(x4132,x4133,x4131)),x4131)
% 0.57/1.04 [426]E(f43(x4261,x4262,x4263),f38(x4261,x4262,x4263))+~E(f91(x4261,x4262),x4263)+E(f6(x4261,x4262,x4263),x4261)+E(f91(f79(x4261,x4262,x4263),f81(x4261,x4262,x4263)),x4263)
% 0.57/1.04 [427]~E(f91(x4271,x4272),x4273)+E(f6(x4271,x4272,x4273),x4271)+E(f85(f61(x4271,x4272,x4273)),x4273)+E(f91(f79(x4271,x4272,x4273),f81(x4271,x4272,x4273)),x4273)
% 0.57/1.04 [431]~E(f91(x4312,x4313),x4311)+E(f38(x4312,x4313,x4311),x4312)+E(x4311,a86)+E(f83(f80(x4312,x4313,x4311),f74(x4312,x4313,x4311),f81(x4312,x4313,x4311)),x4313)
% 0.57/1.04 [432]~E(f91(x4322,x4323),x4321)+E(f79(x4322,x4323,x4321),x4322)+E(x4321,a86)+E(f83(f43(x4322,x4323,x4321),f61(x4322,x4323,x4321),f20(x4322,x4323,x4321)),x4323)
% 0.57/1.04 [433]~E(f91(x4332,x4331),x4333)+E(f79(x4332,x4331,x4333),x4332)+E(x4331,a1)+E(f83(f43(x4332,x4331,x4333),f61(x4332,x4331,x4333),f20(x4332,x4331,x4333)),x4331)
% 0.57/1.04 [434]~E(f91(x4342,x4341),x4343)+E(f38(x4342,x4341,x4343),x4342)+E(x4341,a1)+E(f83(f80(x4342,x4341,x4343),f74(x4342,x4341,x4343),f81(x4342,x4341,x4343)),x4341)
% 0.57/1.04 [444]~E(f91(x4442,x4443),x4441)+E(f43(x4442,x4443,x4441),f38(x4442,x4443,x4441))+E(x4441,a86)+E(f83(f80(x4442,x4443,x4441),f74(x4442,x4443,x4441),f81(x4442,x4443,x4441)),x4443)
% 0.57/1.04 [445]~E(f91(x4452,x4451),x4453)+E(f43(x4452,x4451,x4453),f38(x4452,x4451,x4453))+E(x4451,a1)+E(f83(f80(x4452,x4451,x4453),f74(x4452,x4451,x4453),f81(x4452,x4451,x4453)),x4451)
% 0.57/1.04 [446]E(f38(x4461,x4462,x4463),x4461)+~E(f91(x4461,x4462),x4463)+E(f6(x4461,x4462,x4463),x4461)+E(f83(f80(x4461,x4462,x4463),f74(x4461,x4462,x4463),f81(x4461,x4462,x4463)),x4462)
% 0.57/1.04 [447]E(f79(x4471,x4472,x4473),x4471)+~E(f91(x4471,x4472),x4473)+E(f6(x4471,x4472,x4473),x4471)+E(f83(f43(x4471,x4472,x4473),f61(x4471,x4472,x4473),f20(x4471,x4472,x4473)),x4472)
% 0.57/1.04 [448]~E(f91(x4482,x4483),x4481)+E(x4481,a86)+E(f83(f80(x4482,x4483,x4481),f74(x4482,x4483,x4481),f81(x4482,x4483,x4481)),x4483)+E(f85(f61(x4482,x4483,x4481)),x4481)
% 0.57/1.04 [449]~E(f91(x4492,x4491),x4493)+E(x4491,a1)+E(f83(f80(x4492,x4491,x4493),f74(x4492,x4491,x4493),f81(x4492,x4491,x4493)),x4491)+E(f85(f61(x4492,x4491,x4493)),x4493)
% 0.57/1.04 [456]E(f43(x4561,x4562,x4563),f38(x4561,x4562,x4563))+~E(f91(x4561,x4562),x4563)+E(f6(x4561,x4562,x4563),x4561)+E(f83(f80(x4561,x4562,x4563),f74(x4561,x4562,x4563),f81(x4561,x4562,x4563)),x4562)
% 0.57/1.04 [457]~E(f91(x4571,x4572),x4573)+E(f6(x4571,x4572,x4573),x4571)+E(f85(f61(x4571,x4572,x4573)),x4573)+E(f83(f80(x4571,x4572,x4573),f74(x4571,x4572,x4573),f81(x4571,x4572,x4573)),x4572)
% 0.57/1.04 [458]~E(f91(x4582,x4583),x4581)+~E(f80(x4582,x4583,x4581),f79(x4582,x4583,x4581))+E(x4581,a86)+E(f83(f43(x4582,x4583,x4581),f61(x4582,x4583,x4581),f20(x4582,x4583,x4581)),x4583)
% 0.57/1.04 [459]~E(f91(x4592,x4591),x4593)+~E(f80(x4592,x4591,x4593),f79(x4592,x4591,x4593))+E(x4591,a1)+E(f83(f43(x4592,x4591,x4593),f61(x4592,x4591,x4593),f20(x4592,x4591,x4593)),x4591)
% 0.57/1.04 [464]~E(f91(x4641,x4642),x4643)+~E(f80(x4641,x4642,x4643),f79(x4641,x4642,x4643))+E(f6(x4641,x4642,x4643),x4641)+E(f83(f43(x4641,x4642,x4643),f61(x4641,x4642,x4643),f20(x4641,x4642,x4643)),x4642)
% 0.57/1.04 [465]~E(f91(x4652,x4651),x4653)+E(x4651,a1)+E(f83(f43(x4652,x4651,x4653),f61(x4652,x4651,x4653),f20(x4652,x4651,x4653)),x4651)+E(f91(f79(x4652,x4651,x4653),f81(x4652,x4651,x4653)),x4653)
% 0.57/1.04 [466]~E(f91(x4662,x4663),x4661)+E(x4661,a86)+E(f83(f43(x4662,x4663,x4661),f61(x4662,x4663,x4661),f20(x4662,x4663,x4661)),x4663)+E(f91(f79(x4662,x4663,x4661),f81(x4662,x4663,x4661)),x4661)
% 0.57/1.04 [468]~P1(x4683,x4681,x4682)+E(f84(f22(x4681,x4682,x4683),f25(x4681,x4682,x4683)),x4682)+E(f82(f26(x4681,x4682,x4683),f27(x4681,x4682,x4683)),x4681)+E(f94(f21(x4681,x4682,x4683)),x4681)
% 0.57/1.04 [470]~P1(x4703,x4701,x4702)+E(f84(f22(x4701,x4702,x4703),f25(x4701,x4702,x4703)),x4702)+E(f82(f26(x4701,x4702,x4703),f27(x4701,x4702,x4703)),x4701)+E(f91(f21(x4701,x4702,x4703),x4703),f85(x4702))
% 0.57/1.04 [471]~E(f91(x4711,x4712),x4713)+E(f6(x4711,x4712,x4713),x4711)+E(f91(f79(x4711,x4712,x4713),f81(x4711,x4712,x4713)),x4713)+E(f83(f43(x4711,x4712,x4713),f61(x4711,x4712,x4713),f20(x4711,x4712,x4713)),x4712)
% 0.57/1.04 [472]~P1(x4723,x4721,x4722)+P1(x4723,f27(x4721,x4722,x4723),f28(x4721,x4722,x4723))+E(f84(f22(x4721,x4722,x4723),f25(x4721,x4722,x4723)),x4722)+E(f94(f21(x4721,x4722,x4723)),x4721)
% 0.57/1.04 [473]~P1(x4733,x4731,x4732)+P1(x4733,f27(x4731,x4732,x4733),f28(x4731,x4732,x4733))+E(f84(f22(x4731,x4732,x4733),f25(x4731,x4732,x4733)),x4732)+E(f91(f21(x4731,x4732,x4733),x4733),f85(x4732))
% 0.57/1.04 [485]~E(f91(x4852,x4853),x4851)+E(x4851,a86)+E(f83(f80(x4852,x4853,x4851),f74(x4852,x4853,x4851),f81(x4852,x4853,x4851)),x4853)+E(f83(f43(x4852,x4853,x4851),f61(x4852,x4853,x4851),f20(x4852,x4853,x4851)),x4853)
% 0.57/1.04 [486]~E(f91(x4862,x4861),x4863)+E(x4861,a1)+E(f83(f80(x4862,x4861,x4863),f74(x4862,x4861,x4863),f81(x4862,x4861,x4863)),x4861)+E(f83(f43(x4862,x4861,x4863),f61(x4862,x4861,x4863),f20(x4862,x4861,x4863)),x4861)
% 0.57/1.04 [488]~P1(x4883,x4881,x4882)+E(f82(f26(x4881,x4882,x4883),f27(x4881,x4882,x4883)),x4881)+E(f31(f23(x4881,x4882,x4883),f22(x4881,x4882,x4883),f24(x4881,x4882,x4883)),x4881)+E(f94(f21(x4881,x4882,x4883)),x4881)
% 0.57/1.04 [489]~P1(x4893,x4891,x4892)+E(f82(f26(x4891,x4892,x4893),f27(x4891,x4892,x4893)),x4891)+E(f31(f23(x4891,x4892,x4893),f22(x4891,x4892,x4893),f24(x4891,x4892,x4893)),x4891)+E(f91(f21(x4891,x4892,x4893),x4893),f85(x4892))
% 0.57/1.04 [490]~P1(x4903,x4901,x4902)+P1(x4903,f26(x4901,x4902,x4903),f84(f28(x4901,x4902,x4903),x4902))+E(f84(f22(x4901,x4902,x4903),f25(x4901,x4902,x4903)),x4902)+E(f94(f21(x4901,x4902,x4903)),x4901)
% 0.57/1.04 [491]~E(f91(x4911,x4912),x4913)+E(f6(x4911,x4912,x4913),x4911)+E(f83(f43(x4911,x4912,x4913),f61(x4911,x4912,x4913),f20(x4911,x4912,x4913)),x4912)+E(f83(f80(x4911,x4912,x4913),f74(x4911,x4912,x4913),f81(x4911,x4912,x4913)),x4912)
% 0.57/1.04 [492]~P1(x4923,x4921,x4922)+P1(x4923,f26(x4921,x4922,x4923),f84(f28(x4921,x4922,x4923),x4922))+E(f84(f22(x4921,x4922,x4923),f25(x4921,x4922,x4923)),x4922)+E(f91(f21(x4921,x4922,x4923),x4923),f85(x4922))
% 0.57/1.04 [493]~P1(x4933,x4931,x4932)+P1(x4933,f27(x4931,x4932,x4933),f28(x4931,x4932,x4933))+E(f31(f23(x4931,x4932,x4933),f22(x4931,x4932,x4933),f24(x4931,x4932,x4933)),x4931)+E(f94(f21(x4931,x4932,x4933)),x4931)
% 0.57/1.04 [494]~P1(x4943,x4941,x4942)+P1(x4943,f27(x4941,x4942,x4943),f28(x4941,x4942,x4943))+E(f31(f23(x4941,x4942,x4943),f22(x4941,x4942,x4943),f24(x4941,x4942,x4943)),x4941)+E(f91(f21(x4941,x4942,x4943),x4943),f85(x4942))
% 0.57/1.04 [509]~P1(x5093,x5091,x5092)+P1(x5093,f26(x5091,x5092,x5093),f84(f28(x5091,x5092,x5093),x5092))+E(f31(f23(x5091,x5092,x5093),f22(x5091,x5092,x5093),f24(x5091,x5092,x5093)),x5091)+E(f94(f21(x5091,x5092,x5093)),x5091)
% 0.57/1.04 [510]~P1(x5103,x5101,x5102)+P1(x5103,f26(x5101,x5102,x5103),f84(f28(x5101,x5102,x5103),x5102))+E(f31(f23(x5101,x5102,x5103),f22(x5101,x5102,x5103),f24(x5101,x5102,x5103)),x5101)+E(f91(f21(x5101,x5102,x5103),x5103),f85(x5102))
% 0.57/1.04 [529]~P1(x5293,x5291,x5292)+P1(f83(f23(x5291,x5292,x5293),f22(x5291,x5292,x5293),x5293),f24(x5291,x5292,x5293),f25(x5291,x5292,x5293))+E(f82(f26(x5291,x5292,x5293),f27(x5291,x5292,x5293)),x5291)+E(f94(f21(x5291,x5292,x5293)),x5291)
% 0.57/1.04 [530]~P1(x5303,x5301,x5302)+P1(f83(f23(x5301,x5302,x5303),f22(x5301,x5302,x5303),x5303),f24(x5301,x5302,x5303),f25(x5301,x5302,x5303))+E(f82(f26(x5301,x5302,x5303),f27(x5301,x5302,x5303)),x5301)+E(f91(f21(x5301,x5302,x5303),x5303),f85(x5302))
% 0.57/1.04 [531]~P1(x5313,x5311,x5312)+P1(x5313,f27(x5311,x5312,x5313),f28(x5311,x5312,x5313))+P1(f83(f23(x5311,x5312,x5313),f22(x5311,x5312,x5313),x5313),f24(x5311,x5312,x5313),f25(x5311,x5312,x5313))+E(f94(f21(x5311,x5312,x5313)),x5311)
% 0.57/1.04 [532]~P1(x5323,x5321,x5322)+P1(x5323,f27(x5321,x5322,x5323),f28(x5321,x5322,x5323))+P1(f83(f23(x5321,x5322,x5323),f22(x5321,x5322,x5323),x5323),f24(x5321,x5322,x5323),f25(x5321,x5322,x5323))+E(f91(f21(x5321,x5322,x5323),x5323),f85(x5322))
% 0.57/1.04 [545]~P1(x5453,x5451,x5452)+P1(x5453,f26(x5451,x5452,x5453),f84(f28(x5451,x5452,x5453),x5452))+P1(f83(f23(x5451,x5452,x5453),f22(x5451,x5452,x5453),x5453),f24(x5451,x5452,x5453),f25(x5451,x5452,x5453))+E(f94(f21(x5451,x5452,x5453)),x5451)
% 0.57/1.04 [546]~P1(x5463,x5461,x5462)+P1(x5463,f26(x5461,x5462,x5463),f84(f28(x5461,x5462,x5463),x5462))+P1(f83(f23(x5461,x5462,x5463),f22(x5461,x5462,x5463),x5463),f24(x5461,x5462,x5463),f25(x5461,x5462,x5463))+E(f91(f21(x5461,x5462,x5463),x5463),f85(x5462))
% 0.57/1.04 [299]P9(x2991,x2992)+~E(x2993,x2991)+~E(x2994,x2993)+~E(x2992,f94(x2994))
% 0.57/1.04 [302]~E(x3022,x3023)+~E(x3021,f91(x3022,x3024))+E(x3021,a86)+~E(x3024,a1)
% 0.57/1.04 [303]~P9(x3033,x3034)+E(x3031,x3032)+~E(x3033,x3032)+~E(x3034,f94(x3031))
% 0.57/1.04 [308]~P9(x3083,x3085)+P9(x3081,x3082)+~E(x3083,x3081)+~E(x3082,f82(x3084,x3085))
% 0.57/1.04 [309]~P9(x3093,x3094)+P9(x3091,x3092)+~E(x3093,x3091)+~E(x3092,f82(x3094,x3095))
% 0.57/1.04 [348]~P5(x3481,x3482)+P6(x3481,x3482)+E(x3481,a87)+~E(f33(x3482,x3481),f31(x3483,x3484,x3485))
% 0.57/1.04 [363]~P5(x3631,x3632)+P6(x3631,x3632)+~E(f33(x3632,x3631),f31(x3633,x3634,x3635))+~P2(f71(x3632,x3631))
% 0.57/1.04 [364]~P5(x3641,x3642)+P6(x3641,x3642)+~E(f33(x3642,x3641),f31(x3643,x3644,x3645))+~P4(f72(x3642,x3641))
% 0.57/1.04 [359]P6(x3592,x3591)+~P5(x3592,x3591)+~E(f33(x3591,x3592),f31(x3593,x3594,x3595))+E(f93(f71(x3591,x3592)),f72(x3591,x3592))
% 0.57/1.04 [429]P6(x4292,x4291)+~P5(x4292,x4291)+~E(f33(x4291,x4292),f31(x4293,x4294,x4295))+E(f82(f31(f75(x4291,x4292),f76(x4291,x4292),f77(x4291,x4292)),f71(x4291,x4292)),x4291)
% 0.57/1.04 [333]~P9(x3332,x3334)+~E(x3331,x3332)+~E(x3333,x3331)+~E(x3334,f31(x3333,x3335,x3336))
% 0.57/1.04 [336]~P9(x3363,x3364)+P9(x3361,x3362)+~E(x3361,x3363)+~E(x3364,f31(x3365,x3366,x3362))
% 0.57/1.04 [377]~P6(x3772,x3771)+E(f31(f62(x3771,x3772),f63(x3771,x3772),f64(x3771,x3772)),x3771)+P2(f34(x3771,x3772))+P4(f35(x3771,x3772))+E(f94(f37(x3771,x3772)),x3771)
% 0.57/1.04 [381]~P6(x3812,x3811)+E(f93(f36(x3811,x3812)),f35(x3811,x3812))+E(f31(f62(x3811,x3812),f63(x3811,x3812),f64(x3811,x3812)),x3811)+P2(f34(x3811,x3812))+E(f94(f37(x3811,x3812)),x3811)
% 0.57/1.04 [382]~P6(x3822,x3821)+E(f93(f34(x3821,x3822)),f68(x3821,x3822))+E(f31(f62(x3821,x3822),f63(x3821,x3822),f64(x3821,x3822)),x3821)+P4(f35(x3821,x3822))+E(f94(f37(x3821,x3822)),x3821)
% 0.57/1.04 [383]~P6(x3832,x3831)+E(f31(f62(x3831,x3832),f63(x3831,x3832),f64(x3831,x3832)),x3831)+P4(f35(x3831,x3832))+~P4(f68(x3831,x3832))+E(f94(f37(x3831,x3832)),x3831)
% 0.57/1.04 [385]~P6(x3852,x3851)+E(f93(f36(x3851,x3852)),f35(x3851,x3852))+E(f93(f34(x3851,x3852)),f68(x3851,x3852))+E(f31(f62(x3851,x3852),f63(x3851,x3852),f64(x3851,x3852)),x3851)+E(f94(f37(x3851,x3852)),x3851)
% 0.57/1.04 [386]~P6(x3862,x3861)+E(f93(f36(x3861,x3862)),f35(x3861,x3862))+E(f31(f62(x3861,x3862),f63(x3861,x3862),f64(x3861,x3862)),x3861)+~P4(f68(x3861,x3862))+E(f94(f37(x3861,x3862)),x3861)
% 0.57/1.04 [450]~P6(x4502,x4501)+E(f31(f62(x4501,x4502),f63(x4501,x4502),f64(x4501,x4502)),x4501)+E(f82(f31(f65(x4501,x4502),f66(x4501,x4502),f67(x4501,x4502)),f36(x4501,x4502)),x4501)+P2(f34(x4501,x4502))+E(f94(f37(x4501,x4502)),x4501)
% 0.57/1.04 [451]~P6(x4512,x4511)+E(f31(f62(x4511,x4512),f63(x4511,x4512),f64(x4511,x4512)),x4511)+E(f82(f31(f70(x4511,x4512),f69(x4511,x4512),f73(x4511,x4512)),f34(x4511,x4512)),x4511)+P4(f35(x4511,x4512))+E(f94(f37(x4511,x4512)),x4511)
% 0.57/1.04 [452]~P6(x4522,x4521)+E(f93(f36(x4521,x4522)),f35(x4521,x4522))+E(f31(f62(x4521,x4522),f63(x4521,x4522),f64(x4521,x4522)),x4521)+E(f82(f31(f70(x4521,x4522),f69(x4521,x4522),f73(x4521,x4522)),f34(x4521,x4522)),x4521)+E(f94(f37(x4521,x4522)),x4521)
% 0.57/1.04 [453]~P6(x4532,x4531)+E(f93(f34(x4531,x4532)),f68(x4531,x4532))+E(f31(f62(x4531,x4532),f63(x4531,x4532),f64(x4531,x4532)),x4531)+E(f82(f31(f65(x4531,x4532),f66(x4531,x4532),f67(x4531,x4532)),f36(x4531,x4532)),x4531)+E(f94(f37(x4531,x4532)),x4531)
% 0.57/1.04 [454]~P6(x4542,x4541)+E(f31(f62(x4541,x4542),f63(x4541,x4542),f64(x4541,x4542)),x4541)+E(f82(f31(f65(x4541,x4542),f66(x4541,x4542),f67(x4541,x4542)),f36(x4541,x4542)),x4541)+~P4(f68(x4541,x4542))+E(f94(f37(x4541,x4542)),x4541)
% 0.57/1.04 [487]~P6(x4872,x4871)+E(f31(f62(x4871,x4872),f63(x4871,x4872),f64(x4871,x4872)),x4871)+E(f82(f31(f65(x4871,x4872),f66(x4871,x4872),f67(x4871,x4872)),f36(x4871,x4872)),x4871)+E(f82(f31(f70(x4871,x4872),f69(x4871,x4872),f73(x4871,x4872)),f34(x4871,x4872)),x4871)+E(f94(f37(x4871,x4872)),x4871)
% 0.57/1.04 [437]~P6(x4372,x4371)+E(f31(f62(x4371,x4372),f63(x4371,x4372),f64(x4371,x4372)),x4371)+P4(f35(x4371,x4372))+E(f94(f37(x4371,x4372)),x4371)+E(f92(f95(f70(x4371,x4372),f34(x4371,x4372),f73(x4371,x4372))),x4372)
% 0.57/1.04 [440]~P6(x4402,x4401)+E(f93(f36(x4401,x4402)),f35(x4401,x4402))+E(f31(f62(x4401,x4402),f63(x4401,x4402),f64(x4401,x4402)),x4401)+E(f94(f37(x4401,x4402)),x4401)+E(f92(f95(f70(x4401,x4402),f34(x4401,x4402),f73(x4401,x4402))),x4402)
% 0.57/1.04 [481]~P6(x4812,x4811)+E(f31(f62(x4811,x4812),f63(x4811,x4812),f64(x4811,x4812)),x4811)+E(f82(f31(f65(x4811,x4812),f66(x4811,x4812),f67(x4811,x4812)),f36(x4811,x4812)),x4811)+E(f94(f37(x4811,x4812)),x4811)+E(f92(f95(f70(x4811,x4812),f34(x4811,x4812),f73(x4811,x4812))),x4812)
% 0.57/1.04 [504]~P6(x5042,x5041)+E(f31(f62(x5041,x5042),f63(x5041,x5042),f64(x5041,x5042)),x5041)+P2(f34(x5041,x5042))+E(f94(f37(x5041,x5042)),x5041)+E(f92(f82(f31(f65(x5041,x5042),f66(x5041,x5042),f67(x5041,x5042)),f89(f35(x5041,x5042)))),x5042)
% 0.57/1.04 [505]~P6(x5052,x5051)+E(f93(f34(x5051,x5052)),f68(x5051,x5052))+E(f31(f62(x5051,x5052),f63(x5051,x5052),f64(x5051,x5052)),x5051)+E(f94(f37(x5051,x5052)),x5051)+E(f92(f82(f31(f65(x5051,x5052),f66(x5051,x5052),f67(x5051,x5052)),f89(f35(x5051,x5052)))),x5052)
% 0.57/1.04 [506]~P6(x5062,x5061)+E(f31(f62(x5061,x5062),f63(x5061,x5062),f64(x5061,x5062)),x5061)+~P4(f68(x5061,x5062))+E(f94(f37(x5061,x5062)),x5061)+E(f92(f82(f31(f65(x5061,x5062),f66(x5061,x5062),f67(x5061,x5062)),f89(f35(x5061,x5062)))),x5062)
% 0.57/1.04 [516]~P6(x5162,x5161)+E(f31(f62(x5161,x5162),f63(x5161,x5162),f64(x5161,x5162)),x5161)+E(f94(f37(x5161,x5162)),x5161)+E(f92(f95(f70(x5161,x5162),f34(x5161,x5162),f73(x5161,x5162))),x5162)+E(f92(f82(f31(f65(x5161,x5162),f66(x5161,x5162),f67(x5161,x5162)),f89(f35(x5161,x5162)))),x5162)
% 0.57/1.04 [528]~P6(x5282,x5281)+E(f31(f62(x5281,x5282),f63(x5281,x5282),f64(x5281,x5282)),x5281)+E(f82(f31(f70(x5281,x5282),f69(x5281,x5282),f73(x5281,x5282)),f34(x5281,x5282)),x5281)+E(f94(f37(x5281,x5282)),x5281)+E(f92(f82(f31(f65(x5281,x5282),f66(x5281,x5282),f67(x5281,x5282)),f89(f35(x5281,x5282)))),x5282)
% 0.57/1.04 [535]P8(x5354,x5353,x5352,x5351)+~P7(x5354,x5353,x5352,x5351)+E(f48(x5351,x5352,x5353,x5354),x5351)+E(f54(x5351,x5352,x5353,x5354),x5352)+E(f46(x5351,x5352,x5353,x5354),x5351)
% 0.57/1.04 [536]P8(x5364,x5363,x5362,x5361)+~P7(x5364,x5363,x5362,x5361)+E(f49(x5361,x5362,x5363,x5364),x5362)+E(f54(x5361,x5362,x5363,x5364),x5362)+E(f46(x5361,x5362,x5363,x5364),x5361)
% 0.57/1.04 [537]P8(x5374,x5373,x5372,x5371)+~P7(x5374,x5373,x5372,x5371)+E(f49(x5371,x5372,x5373,x5374),x5372)+E(f55(x5371,x5372,x5373,x5374),x5371)+E(f50(x5371,x5372,x5373,x5374),x5372)
% 0.57/1.04 [538]P8(x5384,x5383,x5382,x5381)+~P7(x5384,x5383,x5382,x5381)+E(f48(x5381,x5382,x5383,x5384),x5381)+E(f55(x5381,x5382,x5383,x5384),x5381)+E(f50(x5381,x5382,x5383,x5384),x5382)
% 0.57/1.04 [539]P8(x5394,x5393,x5392,x5391)+~P7(x5394,x5393,x5392,x5391)+E(f46(x5391,x5392,x5393,x5394),x5391)+E(f55(x5391,x5392,x5393,x5394),x5391)+E(f49(x5391,x5392,x5393,x5394),x5392)
% 0.57/1.04 [540]P8(x5404,x5403,x5402,x5401)+~P7(x5404,x5403,x5402,x5401)+E(f50(x5401,x5402,x5403,x5404),x5402)+E(f54(x5401,x5402,x5403,x5404),x5402)+E(f48(x5401,x5402,x5403,x5404),x5401)
% 0.57/1.04 [541]P8(x5414,x5413,x5412,x5411)+~P7(x5414,x5413,x5412,x5411)+E(f48(x5411,x5412,x5413,x5414),x5411)+E(f55(x5411,x5412,x5413,x5414),x5411)+E(f46(x5411,x5412,x5413,x5414),x5411)
% 0.57/1.04 [542]P8(x5424,x5423,x5422,x5421)+~P7(x5424,x5423,x5422,x5421)+E(f49(x5421,x5422,x5423,x5424),x5422)+E(f54(x5421,x5422,x5423,x5424),x5422)+E(f50(x5421,x5422,x5423,x5424),x5422)
% 0.57/1.04 [551]P8(x5514,x5513,x5512,x5511)+~P7(x5514,x5513,x5512,x5511)+E(f54(x5511,x5512,x5513,x5514),x5512)+E(f52(x5511,x5512,x5513,x5514),f48(x5511,x5512,x5513,x5514))+E(f46(x5511,x5512,x5513,x5514),x5511)
% 0.57/1.04 [552]P8(x5524,x5523,x5522,x5521)+~P7(x5524,x5523,x5522,x5521)+E(f55(x5521,x5522,x5523,x5524),x5521)+E(f52(x5521,x5522,x5523,x5524),f48(x5521,x5522,x5523,x5524))+E(f50(x5521,x5522,x5523,x5524),x5522)
% 0.57/1.04 [553]P8(x5534,x5533,x5532,x5531)+~P7(x5534,x5533,x5532,x5531)+E(f55(x5531,x5532,x5533,x5534),x5531)+E(f52(x5531,x5532,x5533,x5534),f48(x5531,x5532,x5533,x5534))+E(f46(x5531,x5532,x5533,x5534),x5531)
% 0.57/1.04 [554]P8(x5544,x5543,x5542,x5541)+~P7(x5544,x5543,x5542,x5541)+E(f54(x5541,x5542,x5543,x5544),x5542)+E(f52(x5541,x5542,x5543,x5544),f48(x5541,x5542,x5543,x5544))+E(f50(x5541,x5542,x5543,x5544),x5542)
% 0.57/1.04 [559]P8(x5594,x5593,x5592,x5591)+~P7(x5594,x5593,x5592,x5591)+E(f49(x5591,x5592,x5593,x5594),x5592)+~E(f57(x5591,x5592,x5593,x5594),f55(x5591,x5592,x5593,x5594))+E(f50(x5591,x5592,x5593,x5594),x5592)
% 0.57/1.04 [560]P8(x5604,x5603,x5602,x5601)+~P7(x5604,x5603,x5602,x5601)+E(f48(x5601,x5602,x5603,x5604),x5601)+~E(f57(x5601,x5602,x5603,x5604),f55(x5601,x5602,x5603,x5604))+E(f50(x5601,x5602,x5603,x5604),x5602)
% 0.57/1.04 [561]P8(x5614,x5613,x5612,x5611)+~P7(x5614,x5613,x5612,x5611)+E(f46(x5611,x5612,x5613,x5614),x5611)+~E(f57(x5611,x5612,x5613,x5614),f55(x5611,x5612,x5613,x5614))+E(f49(x5611,x5612,x5613,x5614),x5612)
% 0.57/1.04 [562]P8(x5624,x5623,x5622,x5621)+~P7(x5624,x5623,x5622,x5621)+E(f48(x5621,x5622,x5623,x5624),x5621)+~E(f57(x5621,x5622,x5623,x5624),f55(x5621,x5622,x5623,x5624))+E(f46(x5621,x5622,x5623,x5624),x5621)
% 0.57/1.04 [563]P8(x5634,x5633,x5632,x5631)+~P7(x5634,x5633,x5632,x5631)+E(f49(x5631,x5632,x5633,x5634),x5632)+P9(f57(x5631,x5632,x5633,x5634),f54(x5631,x5632,x5633,x5634))+E(f50(x5631,x5632,x5633,x5634),x5632)
% 0.57/1.04 [564]P8(x5644,x5643,x5642,x5641)+~P7(x5644,x5643,x5642,x5641)+E(f48(x5641,x5642,x5643,x5644),x5641)+P9(f57(x5641,x5642,x5643,x5644),f54(x5641,x5642,x5643,x5644))+E(f50(x5641,x5642,x5643,x5644),x5642)
% 0.57/1.04 [565]P8(x5654,x5653,x5652,x5651)+~P7(x5654,x5653,x5652,x5651)+E(f46(x5651,x5652,x5653,x5654),x5651)+P9(f57(x5651,x5652,x5653,x5654),f54(x5651,x5652,x5653,x5654))+E(f49(x5651,x5652,x5653,x5654),x5652)
% 0.57/1.04 [566]P8(x5664,x5663,x5662,x5661)+~P7(x5664,x5663,x5662,x5661)+E(f48(x5661,x5662,x5663,x5664),x5661)+P9(f57(x5661,x5662,x5663,x5664),f54(x5661,x5662,x5663,x5664))+E(f46(x5661,x5662,x5663,x5664),x5661)
% 0.57/1.04 [571]P8(x5714,x5713,x5712,x5711)+~P7(x5714,x5713,x5712,x5711)+E(f52(x5711,x5712,x5713,x5714),f48(x5711,x5712,x5713,x5714))+~E(f57(x5711,x5712,x5713,x5714),f55(x5711,x5712,x5713,x5714))+E(f50(x5711,x5712,x5713,x5714),x5712)
% 0.57/1.04 [572]P8(x5724,x5723,x5722,x5721)+~P7(x5724,x5723,x5722,x5721)+E(f52(x5721,x5722,x5723,x5724),f48(x5721,x5722,x5723,x5724))+~E(f57(x5721,x5722,x5723,x5724),f55(x5721,x5722,x5723,x5724))+E(f46(x5721,x5722,x5723,x5724),x5721)
% 0.57/1.04 [573]P8(x5734,x5733,x5732,x5731)+~P7(x5734,x5733,x5732,x5731)+E(f52(x5731,x5732,x5733,x5734),f48(x5731,x5732,x5733,x5734))+P9(f57(x5731,x5732,x5733,x5734),f54(x5731,x5732,x5733,x5734))+E(f50(x5731,x5732,x5733,x5734),x5732)
% 0.57/1.04 [574]P8(x5744,x5743,x5742,x5741)+~P7(x5744,x5743,x5742,x5741)+E(f52(x5741,x5742,x5743,x5744),f48(x5741,x5742,x5743,x5744))+P9(f57(x5741,x5742,x5743,x5744),f54(x5741,x5742,x5743,x5744))+E(f46(x5741,x5742,x5743,x5744),x5741)
% 0.57/1.04 [567]P8(x5674,x5673,x5672,x5671)+~P7(x5674,x5673,x5672,x5671)+E(f55(x5671,x5672,x5673,x5674),x5671)+E(f49(x5671,x5672,x5673,x5674),x5672)+E(f82(f47(x5671,x5672,x5673,x5674),f51(x5671,x5672,x5673,x5674)),x5673)
% 0.57/1.04 [568]P8(x5684,x5683,x5682,x5681)+~P7(x5684,x5683,x5682,x5681)+E(f54(x5681,x5682,x5683,x5684),x5682)+E(f48(x5681,x5682,x5683,x5684),x5681)+E(f82(f47(x5681,x5682,x5683,x5684),f51(x5681,x5682,x5683,x5684)),x5683)
% 0.57/1.04 [569]P8(x5694,x5693,x5692,x5691)+~P7(x5694,x5693,x5692,x5691)+E(f54(x5691,x5692,x5693,x5694),x5692)+E(f49(x5691,x5692,x5693,x5694),x5692)+E(f82(f47(x5691,x5692,x5693,x5694),f51(x5691,x5692,x5693,x5694)),x5693)
% 0.57/1.04 [570]P8(x5704,x5703,x5702,x5701)+~P7(x5704,x5703,x5702,x5701)+E(f55(x5701,x5702,x5703,x5704),x5701)+E(f48(x5701,x5702,x5703,x5704),x5701)+E(f82(f47(x5701,x5702,x5703,x5704),f51(x5701,x5702,x5703,x5704)),x5703)
% 0.57/1.04 [575]P8(x5754,x5753,x5752,x5751)+~P7(x5754,x5753,x5752,x5751)+E(f52(x5751,x5752,x5753,x5754),f48(x5751,x5752,x5753,x5754))+E(f55(x5751,x5752,x5753,x5754),x5751)+E(f82(f47(x5751,x5752,x5753,x5754),f51(x5751,x5752,x5753,x5754)),x5753)
% 0.57/1.04 [576]P8(x5764,x5763,x5762,x5761)+~P7(x5764,x5763,x5762,x5761)+E(f52(x5761,x5762,x5763,x5764),f48(x5761,x5762,x5763,x5764))+E(f54(x5761,x5762,x5763,x5764),x5762)+E(f82(f47(x5761,x5762,x5763,x5764),f51(x5761,x5762,x5763,x5764)),x5763)
% 0.57/1.04 [577]P8(x5774,x5773,x5772,x5771)+~P7(x5774,x5773,x5772,x5771)+~E(f57(x5771,x5772,x5773,x5774),f55(x5771,x5772,x5773,x5774))+E(f49(x5771,x5772,x5773,x5774),x5772)+E(f82(f47(x5771,x5772,x5773,x5774),f51(x5771,x5772,x5773,x5774)),x5773)
% 0.57/1.04 [578]P8(x5784,x5783,x5782,x5781)+~P7(x5784,x5783,x5782,x5781)+~E(f57(x5781,x5782,x5783,x5784),f55(x5781,x5782,x5783,x5784))+E(f48(x5781,x5782,x5783,x5784),x5781)+E(f82(f47(x5781,x5782,x5783,x5784),f51(x5781,x5782,x5783,x5784)),x5783)
% 0.57/1.04 [579]P8(x5794,x5793,x5792,x5791)+~P7(x5794,x5793,x5792,x5791)+E(f49(x5791,x5792,x5793,x5794),x5792)+E(f50(x5791,x5792,x5793,x5794),x5792)+E(f31(f57(x5791,x5792,x5793,x5794),f58(x5791,x5792,x5793,x5794),f59(x5791,x5792,x5793,x5794)),x5793)
% 0.57/1.04 [580]P8(x5804,x5803,x5802,x5801)+~P7(x5804,x5803,x5802,x5801)+E(f48(x5801,x5802,x5803,x5804),x5801)+E(f50(x5801,x5802,x5803,x5804),x5802)+E(f31(f57(x5801,x5802,x5803,x5804),f58(x5801,x5802,x5803,x5804),f59(x5801,x5802,x5803,x5804)),x5803)
% 0.57/1.04 [581]P8(x5814,x5813,x5812,x5811)+~P7(x5814,x5813,x5812,x5811)+E(f46(x5811,x5812,x5813,x5814),x5811)+E(f49(x5811,x5812,x5813,x5814),x5812)+E(f31(f57(x5811,x5812,x5813,x5814),f58(x5811,x5812,x5813,x5814),f59(x5811,x5812,x5813,x5814)),x5813)
% 0.57/1.04 [582]P8(x5824,x5823,x5822,x5821)+~P7(x5824,x5823,x5822,x5821)+E(f48(x5821,x5822,x5823,x5824),x5821)+E(f46(x5821,x5822,x5823,x5824),x5821)+E(f31(f57(x5821,x5822,x5823,x5824),f58(x5821,x5822,x5823,x5824),f59(x5821,x5822,x5823,x5824)),x5823)
% 0.57/1.04 [583]P8(x5834,x5833,x5832,x5831)+~P7(x5834,x5833,x5832,x5831)+E(f54(x5831,x5832,x5833,x5834),x5832)+E(f46(x5831,x5832,x5833,x5834),x5831)+E(f31(f52(x5831,x5832,x5833,x5834),f53(x5831,x5832,x5833,x5834),f56(x5831,x5832,x5833,x5834)),x5834)
% 0.57/1.04 [584]P8(x5844,x5843,x5842,x5841)+~P7(x5844,x5843,x5842,x5841)+E(f54(x5841,x5842,x5843,x5844),x5842)+E(f46(x5841,x5842,x5843,x5844),x5841)+E(f31(f52(x5841,x5842,x5843,x5844),f53(x5841,x5842,x5843,x5844),f56(x5841,x5842,x5843,x5844)),x5843)
% 0.57/1.04 [585]P8(x5854,x5853,x5852,x5851)+~P7(x5854,x5853,x5852,x5851)+E(f55(x5851,x5852,x5853,x5854),x5851)+E(f50(x5851,x5852,x5853,x5854),x5852)+E(f31(f52(x5851,x5852,x5853,x5854),f53(x5851,x5852,x5853,x5854),f56(x5851,x5852,x5853,x5854)),x5854)
% 0.57/1.04 [586]P8(x5864,x5863,x5862,x5861)+~P7(x5864,x5863,x5862,x5861)+E(f55(x5861,x5862,x5863,x5864),x5861)+E(f50(x5861,x5862,x5863,x5864),x5862)+E(f31(f52(x5861,x5862,x5863,x5864),f53(x5861,x5862,x5863,x5864),f56(x5861,x5862,x5863,x5864)),x5863)
% 0.57/1.04 [587]P8(x5874,x5873,x5872,x5871)+~P7(x5874,x5873,x5872,x5871)+E(f55(x5871,x5872,x5873,x5874),x5871)+E(f46(x5871,x5872,x5873,x5874),x5871)+E(f31(f52(x5871,x5872,x5873,x5874),f53(x5871,x5872,x5873,x5874),f56(x5871,x5872,x5873,x5874)),x5874)
% 0.57/1.04 [588]P8(x5884,x5883,x5882,x5881)+~P7(x5884,x5883,x5882,x5881)+E(f55(x5881,x5882,x5883,x5884),x5881)+E(f46(x5881,x5882,x5883,x5884),x5881)+E(f31(f52(x5881,x5882,x5883,x5884),f53(x5881,x5882,x5883,x5884),f56(x5881,x5882,x5883,x5884)),x5883)
% 0.57/1.04 [589]P8(x5894,x5893,x5892,x5891)+~P7(x5894,x5893,x5892,x5891)+E(f54(x5891,x5892,x5893,x5894),x5892)+E(f50(x5891,x5892,x5893,x5894),x5892)+E(f31(f52(x5891,x5892,x5893,x5894),f53(x5891,x5892,x5893,x5894),f56(x5891,x5892,x5893,x5894)),x5894)
% 0.57/1.04 [590]P8(x5904,x5903,x5902,x5901)+~P7(x5904,x5903,x5902,x5901)+E(f54(x5901,x5902,x5903,x5904),x5902)+E(f50(x5901,x5902,x5903,x5904),x5902)+E(f31(f52(x5901,x5902,x5903,x5904),f53(x5901,x5902,x5903,x5904),f56(x5901,x5902,x5903,x5904)),x5903)
% 0.57/1.04 [591]P8(x5914,x5913,x5912,x5911)+~P7(x5914,x5913,x5912,x5911)+P9(f57(x5911,x5912,x5913,x5914),f54(x5911,x5912,x5913,x5914))+E(f49(x5911,x5912,x5913,x5914),x5912)+E(f82(f47(x5911,x5912,x5913,x5914),f51(x5911,x5912,x5913,x5914)),x5913)
% 0.57/1.04 [592]P8(x5924,x5923,x5922,x5921)+~P7(x5924,x5923,x5922,x5921)+P9(f57(x5921,x5922,x5923,x5924),f54(x5921,x5922,x5923,x5924))+E(f48(x5921,x5922,x5923,x5924),x5921)+E(f82(f47(x5921,x5922,x5923,x5924),f51(x5921,x5922,x5923,x5924)),x5923)
% 0.57/1.04 [593]P8(x5934,x5933,x5932,x5931)+~P7(x5934,x5933,x5932,x5931)+~E(f57(x5931,x5932,x5933,x5934),f55(x5931,x5932,x5933,x5934))+E(f52(x5931,x5932,x5933,x5934),f48(x5931,x5932,x5933,x5934))+E(f82(f47(x5931,x5932,x5933,x5934),f51(x5931,x5932,x5933,x5934)),x5933)
% 0.57/1.04 [594]P8(x5944,x5943,x5942,x5941)+~P7(x5944,x5943,x5942,x5941)+E(f52(x5941,x5942,x5943,x5944),f48(x5941,x5942,x5943,x5944))+E(f50(x5941,x5942,x5943,x5944),x5942)+E(f31(f57(x5941,x5942,x5943,x5944),f58(x5941,x5942,x5943,x5944),f59(x5941,x5942,x5943,x5944)),x5943)
% 0.57/1.04 [595]P8(x5954,x5953,x5952,x5951)+~P7(x5954,x5953,x5952,x5951)+E(f52(x5951,x5952,x5953,x5954),f48(x5951,x5952,x5953,x5954))+E(f46(x5951,x5952,x5953,x5954),x5951)+E(f31(f57(x5951,x5952,x5953,x5954),f58(x5951,x5952,x5953,x5954),f59(x5951,x5952,x5953,x5954)),x5953)
% 0.57/1.04 [596]P8(x5964,x5963,x5962,x5961)+~P7(x5964,x5963,x5962,x5961)+P9(f57(x5961,x5962,x5963,x5964),f54(x5961,x5962,x5963,x5964))+E(f52(x5961,x5962,x5963,x5964),f48(x5961,x5962,x5963,x5964))+E(f82(f47(x5961,x5962,x5963,x5964),f51(x5961,x5962,x5963,x5964)),x5963)
% 0.57/1.04 [597]P8(x5974,x5973,x5972,x5971)+~P7(x5974,x5973,x5972,x5971)+~E(f57(x5971,x5972,x5973,x5974),f55(x5971,x5972,x5973,x5974))+E(f50(x5971,x5972,x5973,x5974),x5972)+E(f31(f52(x5971,x5972,x5973,x5974),f53(x5971,x5972,x5973,x5974),f56(x5971,x5972,x5973,x5974)),x5974)
% 0.57/1.04 [598]P8(x5984,x5983,x5982,x5981)+~P7(x5984,x5983,x5982,x5981)+~E(f57(x5981,x5982,x5983,x5984),f55(x5981,x5982,x5983,x5984))+E(f50(x5981,x5982,x5983,x5984),x5982)+E(f31(f52(x5981,x5982,x5983,x5984),f53(x5981,x5982,x5983,x5984),f56(x5981,x5982,x5983,x5984)),x5983)
% 0.57/1.04 [599]P8(x5994,x5993,x5992,x5991)+~P7(x5994,x5993,x5992,x5991)+~E(f57(x5991,x5992,x5993,x5994),f55(x5991,x5992,x5993,x5994))+E(f46(x5991,x5992,x5993,x5994),x5991)+E(f31(f52(x5991,x5992,x5993,x5994),f53(x5991,x5992,x5993,x5994),f56(x5991,x5992,x5993,x5994)),x5994)
% 0.57/1.05 [600]P8(x6004,x6003,x6002,x6001)+~P7(x6004,x6003,x6002,x6001)+~E(f57(x6001,x6002,x6003,x6004),f55(x6001,x6002,x6003,x6004))+E(f46(x6001,x6002,x6003,x6004),x6001)+E(f31(f52(x6001,x6002,x6003,x6004),f53(x6001,x6002,x6003,x6004),f56(x6001,x6002,x6003,x6004)),x6003)
% 0.57/1.05 [601]P8(x6014,x6013,x6012,x6011)+~P7(x6014,x6013,x6012,x6011)+P9(f57(x6011,x6012,x6013,x6014),f54(x6011,x6012,x6013,x6014))+E(f50(x6011,x6012,x6013,x6014),x6012)+E(f31(f52(x6011,x6012,x6013,x6014),f53(x6011,x6012,x6013,x6014),f56(x6011,x6012,x6013,x6014)),x6014)
% 0.57/1.05 [602]P8(x6024,x6023,x6022,x6021)+~P7(x6024,x6023,x6022,x6021)+P9(f57(x6021,x6022,x6023,x6024),f54(x6021,x6022,x6023,x6024))+E(f50(x6021,x6022,x6023,x6024),x6022)+E(f31(f52(x6021,x6022,x6023,x6024),f53(x6021,x6022,x6023,x6024),f56(x6021,x6022,x6023,x6024)),x6023)
% 0.57/1.05 [603]P8(x6034,x6033,x6032,x6031)+~P7(x6034,x6033,x6032,x6031)+P9(f57(x6031,x6032,x6033,x6034),f54(x6031,x6032,x6033,x6034))+E(f46(x6031,x6032,x6033,x6034),x6031)+E(f31(f52(x6031,x6032,x6033,x6034),f53(x6031,x6032,x6033,x6034),f56(x6031,x6032,x6033,x6034)),x6034)
% 0.57/1.05 [604]P8(x6044,x6043,x6042,x6041)+~P7(x6044,x6043,x6042,x6041)+P9(f57(x6041,x6042,x6043,x6044),f54(x6041,x6042,x6043,x6044))+E(f46(x6041,x6042,x6043,x6044),x6041)+E(f31(f52(x6041,x6042,x6043,x6044),f53(x6041,x6042,x6043,x6044),f56(x6041,x6042,x6043,x6044)),x6043)
% 0.57/1.05 [605]P8(x6054,x6053,x6052,x6051)+~P7(x6054,x6053,x6052,x6051)+E(f49(x6051,x6052,x6053,x6054),x6052)+E(f82(f47(x6051,x6052,x6053,x6054),f51(x6051,x6052,x6053,x6054)),x6053)+E(f31(f57(x6051,x6052,x6053,x6054),f58(x6051,x6052,x6053,x6054),f59(x6051,x6052,x6053,x6054)),x6053)
% 0.57/1.05 [606]P8(x6064,x6063,x6062,x6061)+~P7(x6064,x6063,x6062,x6061)+E(f48(x6061,x6062,x6063,x6064),x6061)+E(f82(f47(x6061,x6062,x6063,x6064),f51(x6061,x6062,x6063,x6064)),x6063)+E(f31(f57(x6061,x6062,x6063,x6064),f58(x6061,x6062,x6063,x6064),f59(x6061,x6062,x6063,x6064)),x6063)
% 0.57/1.05 [607]P8(x6074,x6073,x6072,x6071)+~P7(x6074,x6073,x6072,x6071)+E(f55(x6071,x6072,x6073,x6074),x6071)+E(f82(f47(x6071,x6072,x6073,x6074),f51(x6071,x6072,x6073,x6074)),x6073)+E(f31(f52(x6071,x6072,x6073,x6074),f53(x6071,x6072,x6073,x6074),f56(x6071,x6072,x6073,x6074)),x6074)
% 0.57/1.05 [608]P8(x6084,x6083,x6082,x6081)+~P7(x6084,x6083,x6082,x6081)+E(f55(x6081,x6082,x6083,x6084),x6081)+E(f82(f47(x6081,x6082,x6083,x6084),f51(x6081,x6082,x6083,x6084)),x6083)+E(f31(f52(x6081,x6082,x6083,x6084),f53(x6081,x6082,x6083,x6084),f56(x6081,x6082,x6083,x6084)),x6083)
% 0.57/1.05 [609]P8(x6094,x6093,x6092,x6091)+~P7(x6094,x6093,x6092,x6091)+E(f54(x6091,x6092,x6093,x6094),x6092)+E(f82(f47(x6091,x6092,x6093,x6094),f51(x6091,x6092,x6093,x6094)),x6093)+E(f31(f52(x6091,x6092,x6093,x6094),f53(x6091,x6092,x6093,x6094),f56(x6091,x6092,x6093,x6094)),x6094)
% 0.57/1.05 [610]P8(x6104,x6103,x6102,x6101)+~P7(x6104,x6103,x6102,x6101)+E(f54(x6101,x6102,x6103,x6104),x6102)+E(f82(f47(x6101,x6102,x6103,x6104),f51(x6101,x6102,x6103,x6104)),x6103)+E(f31(f52(x6101,x6102,x6103,x6104),f53(x6101,x6102,x6103,x6104),f56(x6101,x6102,x6103,x6104)),x6103)
% 0.57/1.05 [611]P8(x6114,x6113,x6112,x6111)+~P7(x6114,x6113,x6112,x6111)+E(f52(x6111,x6112,x6113,x6114),f48(x6111,x6112,x6113,x6114))+E(f82(f47(x6111,x6112,x6113,x6114),f51(x6111,x6112,x6113,x6114)),x6113)+E(f31(f57(x6111,x6112,x6113,x6114),f58(x6111,x6112,x6113,x6114),f59(x6111,x6112,x6113,x6114)),x6113)
% 0.57/1.05 [612]P8(x6124,x6123,x6122,x6121)+~P7(x6124,x6123,x6122,x6121)+~E(f57(x6121,x6122,x6123,x6124),f55(x6121,x6122,x6123,x6124))+E(f31(f52(x6121,x6122,x6123,x6124),f53(x6121,x6122,x6123,x6124),f56(x6121,x6122,x6123,x6124)),x6124)+E(f82(f47(x6121,x6122,x6123,x6124),f51(x6121,x6122,x6123,x6124)),x6123)
% 0.57/1.05 [613]P8(x6134,x6133,x6132,x6131)+~P7(x6134,x6133,x6132,x6131)+~E(f57(x6131,x6132,x6133,x6134),f55(x6131,x6132,x6133,x6134))+E(f31(f52(x6131,x6132,x6133,x6134),f53(x6131,x6132,x6133,x6134),f56(x6131,x6132,x6133,x6134)),x6133)+E(f82(f47(x6131,x6132,x6133,x6134),f51(x6131,x6132,x6133,x6134)),x6133)
% 0.57/1.05 [614]P8(x6144,x6143,x6142,x6141)+~P7(x6144,x6143,x6142,x6141)+E(f50(x6141,x6142,x6143,x6144),x6142)+E(f31(f52(x6141,x6142,x6143,x6144),f53(x6141,x6142,x6143,x6144),f56(x6141,x6142,x6143,x6144)),x6144)+E(f31(f57(x6141,x6142,x6143,x6144),f58(x6141,x6142,x6143,x6144),f59(x6141,x6142,x6143,x6144)),x6143)
% 0.57/1.05 [615]P8(x6154,x6153,x6152,x6151)+~P7(x6154,x6153,x6152,x6151)+E(f50(x6151,x6152,x6153,x6154),x6152)+E(f31(f52(x6151,x6152,x6153,x6154),f53(x6151,x6152,x6153,x6154),f56(x6151,x6152,x6153,x6154)),x6153)+E(f31(f57(x6151,x6152,x6153,x6154),f58(x6151,x6152,x6153,x6154),f59(x6151,x6152,x6153,x6154)),x6153)
% 0.57/1.05 [616]P8(x6164,x6163,x6162,x6161)+~P7(x6164,x6163,x6162,x6161)+E(f46(x6161,x6162,x6163,x6164),x6161)+E(f31(f52(x6161,x6162,x6163,x6164),f53(x6161,x6162,x6163,x6164),f56(x6161,x6162,x6163,x6164)),x6164)+E(f31(f57(x6161,x6162,x6163,x6164),f58(x6161,x6162,x6163,x6164),f59(x6161,x6162,x6163,x6164)),x6163)
% 0.57/1.05 [617]P8(x6174,x6173,x6172,x6171)+~P7(x6174,x6173,x6172,x6171)+E(f46(x6171,x6172,x6173,x6174),x6171)+E(f31(f52(x6171,x6172,x6173,x6174),f53(x6171,x6172,x6173,x6174),f56(x6171,x6172,x6173,x6174)),x6173)+E(f31(f57(x6171,x6172,x6173,x6174),f58(x6171,x6172,x6173,x6174),f59(x6171,x6172,x6173,x6174)),x6173)
% 0.57/1.05 [618]P8(x6184,x6183,x6182,x6181)+~P7(x6184,x6183,x6182,x6181)+P9(f57(x6181,x6182,x6183,x6184),f54(x6181,x6182,x6183,x6184))+E(f31(f52(x6181,x6182,x6183,x6184),f53(x6181,x6182,x6183,x6184),f56(x6181,x6182,x6183,x6184)),x6184)+E(f82(f47(x6181,x6182,x6183,x6184),f51(x6181,x6182,x6183,x6184)),x6183)
% 0.57/1.05 [619]P8(x6194,x6193,x6192,x6191)+~P7(x6194,x6193,x6192,x6191)+P9(f57(x6191,x6192,x6193,x6194),f54(x6191,x6192,x6193,x6194))+E(f31(f52(x6191,x6192,x6193,x6194),f53(x6191,x6192,x6193,x6194),f56(x6191,x6192,x6193,x6194)),x6193)+E(f82(f47(x6191,x6192,x6193,x6194),f51(x6191,x6192,x6193,x6194)),x6193)
% 0.57/1.05 [621]P8(x6214,x6213,x6212,x6211)+~P7(x6214,x6213,x6212,x6211)+E(f31(f52(x6211,x6212,x6213,x6214),f53(x6211,x6212,x6213,x6214),f56(x6211,x6212,x6213,x6214)),x6214)+E(f31(f57(x6211,x6212,x6213,x6214),f58(x6211,x6212,x6213,x6214),f59(x6211,x6212,x6213,x6214)),x6213)+E(f82(f47(x6211,x6212,x6213,x6214),f51(x6211,x6212,x6213,x6214)),x6213)
% 0.57/1.05 [622]P8(x6224,x6223,x6222,x6221)+~P7(x6224,x6223,x6222,x6221)+E(f31(f52(x6221,x6222,x6223,x6224),f53(x6221,x6222,x6223,x6224),f56(x6221,x6222,x6223,x6224)),x6223)+E(f31(f57(x6221,x6222,x6223,x6224),f58(x6221,x6222,x6223,x6224),f59(x6221,x6222,x6223,x6224)),x6223)+E(f82(f47(x6221,x6222,x6223,x6224),f51(x6221,x6222,x6223,x6224)),x6223)
% 0.57/1.05 [623]P8(x6234,x6233,x6232,x6231)+~P7(x6234,x6233,x6232,x6231)+E(f55(x6231,x6232,x6233,x6234),x6231)+E(f49(x6231,x6232,x6233,x6234),x6232)+E(f82(f95(f46(x6231,x6232,x6233,x6234),f50(x6231,x6232,x6233,x6234),f47(x6231,x6232,x6233,x6234)),f95(f46(x6231,x6232,x6233,x6234),f50(x6231,x6232,x6233,x6234),f51(x6231,x6232,x6233,x6234))),x6234)
% 0.57/1.05 [624]P8(x6244,x6243,x6242,x6241)+~P7(x6244,x6243,x6242,x6241)+E(f54(x6241,x6242,x6243,x6244),x6242)+E(f48(x6241,x6242,x6243,x6244),x6241)+E(f82(f95(f46(x6241,x6242,x6243,x6244),f50(x6241,x6242,x6243,x6244),f47(x6241,x6242,x6243,x6244)),f95(f46(x6241,x6242,x6243,x6244),f50(x6241,x6242,x6243,x6244),f51(x6241,x6242,x6243,x6244))),x6244)
% 0.57/1.05 [625]P8(x6254,x6253,x6252,x6251)+~P7(x6254,x6253,x6252,x6251)+E(f54(x6251,x6252,x6253,x6254),x6252)+E(f49(x6251,x6252,x6253,x6254),x6252)+E(f82(f95(f46(x6251,x6252,x6253,x6254),f50(x6251,x6252,x6253,x6254),f47(x6251,x6252,x6253,x6254)),f95(f46(x6251,x6252,x6253,x6254),f50(x6251,x6252,x6253,x6254),f51(x6251,x6252,x6253,x6254))),x6254)
% 0.57/1.05 [626]P8(x6264,x6263,x6262,x6261)+~P7(x6264,x6263,x6262,x6261)+E(f55(x6261,x6262,x6263,x6264),x6261)+E(f48(x6261,x6262,x6263,x6264),x6261)+E(f82(f95(f46(x6261,x6262,x6263,x6264),f50(x6261,x6262,x6263,x6264),f47(x6261,x6262,x6263,x6264)),f95(f46(x6261,x6262,x6263,x6264),f50(x6261,x6262,x6263,x6264),f51(x6261,x6262,x6263,x6264))),x6264)
% 0.57/1.05 [632]P8(x6324,x6323,x6322,x6321)+~P7(x6324,x6323,x6322,x6321)+E(f52(x6321,x6322,x6323,x6324),f48(x6321,x6322,x6323,x6324))+E(f55(x6321,x6322,x6323,x6324),x6321)+E(f82(f95(f46(x6321,x6322,x6323,x6324),f50(x6321,x6322,x6323,x6324),f47(x6321,x6322,x6323,x6324)),f95(f46(x6321,x6322,x6323,x6324),f50(x6321,x6322,x6323,x6324),f51(x6321,x6322,x6323,x6324))),x6324)
% 0.57/1.05 [633]P8(x6334,x6333,x6332,x6331)+~P7(x6334,x6333,x6332,x6331)+E(f52(x6331,x6332,x6333,x6334),f48(x6331,x6332,x6333,x6334))+E(f54(x6331,x6332,x6333,x6334),x6332)+E(f82(f95(f46(x6331,x6332,x6333,x6334),f50(x6331,x6332,x6333,x6334),f47(x6331,x6332,x6333,x6334)),f95(f46(x6331,x6332,x6333,x6334),f50(x6331,x6332,x6333,x6334),f51(x6331,x6332,x6333,x6334))),x6334)
% 0.57/1.05 [636]P8(x6364,x6363,x6362,x6361)+~P7(x6364,x6363,x6362,x6361)+~E(f57(x6361,x6362,x6363,x6364),f55(x6361,x6362,x6363,x6364))+E(f49(x6361,x6362,x6363,x6364),x6362)+E(f82(f95(f46(x6361,x6362,x6363,x6364),f50(x6361,x6362,x6363,x6364),f47(x6361,x6362,x6363,x6364)),f95(f46(x6361,x6362,x6363,x6364),f50(x6361,x6362,x6363,x6364),f51(x6361,x6362,x6363,x6364))),x6364)
% 0.57/1.05 [637]P8(x6374,x6373,x6372,x6371)+~P7(x6374,x6373,x6372,x6371)+~E(f57(x6371,x6372,x6373,x6374),f55(x6371,x6372,x6373,x6374))+E(f48(x6371,x6372,x6373,x6374),x6371)+E(f82(f95(f46(x6371,x6372,x6373,x6374),f50(x6371,x6372,x6373,x6374),f47(x6371,x6372,x6373,x6374)),f95(f46(x6371,x6372,x6373,x6374),f50(x6371,x6372,x6373,x6374),f51(x6371,x6372,x6373,x6374))),x6374)
% 0.57/1.05 [638]P8(x6384,x6383,x6382,x6381)+~P7(x6384,x6383,x6382,x6381)+P9(f57(x6381,x6382,x6383,x6384),f54(x6381,x6382,x6383,x6384))+E(f49(x6381,x6382,x6383,x6384),x6382)+E(f82(f95(f46(x6381,x6382,x6383,x6384),f50(x6381,x6382,x6383,x6384),f47(x6381,x6382,x6383,x6384)),f95(f46(x6381,x6382,x6383,x6384),f50(x6381,x6382,x6383,x6384),f51(x6381,x6382,x6383,x6384))),x6384)
% 0.57/1.05 [639]P8(x6394,x6393,x6392,x6391)+~P7(x6394,x6393,x6392,x6391)+P9(f57(x6391,x6392,x6393,x6394),f54(x6391,x6392,x6393,x6394))+E(f48(x6391,x6392,x6393,x6394),x6391)+E(f82(f95(f46(x6391,x6392,x6393,x6394),f50(x6391,x6392,x6393,x6394),f47(x6391,x6392,x6393,x6394)),f95(f46(x6391,x6392,x6393,x6394),f50(x6391,x6392,x6393,x6394),f51(x6391,x6392,x6393,x6394))),x6394)
% 0.57/1.05 [640]P8(x6404,x6403,x6402,x6401)+~P7(x6404,x6403,x6402,x6401)+~E(f57(x6401,x6402,x6403,x6404),f55(x6401,x6402,x6403,x6404))+E(f52(x6401,x6402,x6403,x6404),f48(x6401,x6402,x6403,x6404))+E(f82(f95(f46(x6401,x6402,x6403,x6404),f50(x6401,x6402,x6403,x6404),f47(x6401,x6402,x6403,x6404)),f95(f46(x6401,x6402,x6403,x6404),f50(x6401,x6402,x6403,x6404),f51(x6401,x6402,x6403,x6404))),x6404)
% 0.57/1.05 [643]P8(x6434,x6433,x6432,x6431)+~P7(x6434,x6433,x6432,x6431)+P9(f57(x6431,x6432,x6433,x6434),f54(x6431,x6432,x6433,x6434))+E(f52(x6431,x6432,x6433,x6434),f48(x6431,x6432,x6433,x6434))+E(f82(f95(f46(x6431,x6432,x6433,x6434),f50(x6431,x6432,x6433,x6434),f47(x6431,x6432,x6433,x6434)),f95(f46(x6431,x6432,x6433,x6434),f50(x6431,x6432,x6433,x6434),f51(x6431,x6432,x6433,x6434))),x6434)
% 0.57/1.05 [645]P8(x6454,x6453,x6452,x6451)+~P7(x6454,x6453,x6452,x6451)+E(f49(x6451,x6452,x6453,x6454),x6452)+E(f31(f57(x6451,x6452,x6453,x6454),f58(x6451,x6452,x6453,x6454),f59(x6451,x6452,x6453,x6454)),x6453)+E(f82(f95(f46(x6451,x6452,x6453,x6454),f50(x6451,x6452,x6453,x6454),f47(x6451,x6452,x6453,x6454)),f95(f46(x6451,x6452,x6453,x6454),f50(x6451,x6452,x6453,x6454),f51(x6451,x6452,x6453,x6454))),x6454)
% 0.57/1.05 [646]P8(x6464,x6463,x6462,x6461)+~P7(x6464,x6463,x6462,x6461)+E(f48(x6461,x6462,x6463,x6464),x6461)+E(f31(f57(x6461,x6462,x6463,x6464),f58(x6461,x6462,x6463,x6464),f59(x6461,x6462,x6463,x6464)),x6463)+E(f82(f95(f46(x6461,x6462,x6463,x6464),f50(x6461,x6462,x6463,x6464),f47(x6461,x6462,x6463,x6464)),f95(f46(x6461,x6462,x6463,x6464),f50(x6461,x6462,x6463,x6464),f51(x6461,x6462,x6463,x6464))),x6464)
% 0.57/1.05 [647]P8(x6474,x6473,x6472,x6471)+~P7(x6474,x6473,x6472,x6471)+E(f55(x6471,x6472,x6473,x6474),x6471)+E(f31(f52(x6471,x6472,x6473,x6474),f53(x6471,x6472,x6473,x6474),f56(x6471,x6472,x6473,x6474)),x6474)+E(f82(f95(f46(x6471,x6472,x6473,x6474),f50(x6471,x6472,x6473,x6474),f47(x6471,x6472,x6473,x6474)),f95(f46(x6471,x6472,x6473,x6474),f50(x6471,x6472,x6473,x6474),f51(x6471,x6472,x6473,x6474))),x6474)
% 0.57/1.05 [648]P8(x6484,x6483,x6482,x6481)+~P7(x6484,x6483,x6482,x6481)+E(f55(x6481,x6482,x6483,x6484),x6481)+E(f31(f52(x6481,x6482,x6483,x6484),f53(x6481,x6482,x6483,x6484),f56(x6481,x6482,x6483,x6484)),x6483)+E(f82(f95(f46(x6481,x6482,x6483,x6484),f50(x6481,x6482,x6483,x6484),f47(x6481,x6482,x6483,x6484)),f95(f46(x6481,x6482,x6483,x6484),f50(x6481,x6482,x6483,x6484),f51(x6481,x6482,x6483,x6484))),x6484)
% 0.57/1.05 [649]P8(x6494,x6493,x6492,x6491)+~P7(x6494,x6493,x6492,x6491)+E(f54(x6491,x6492,x6493,x6494),x6492)+E(f31(f52(x6491,x6492,x6493,x6494),f53(x6491,x6492,x6493,x6494),f56(x6491,x6492,x6493,x6494)),x6494)+E(f82(f95(f46(x6491,x6492,x6493,x6494),f50(x6491,x6492,x6493,x6494),f47(x6491,x6492,x6493,x6494)),f95(f46(x6491,x6492,x6493,x6494),f50(x6491,x6492,x6493,x6494),f51(x6491,x6492,x6493,x6494))),x6494)
% 0.57/1.05 [650]P8(x6504,x6503,x6502,x6501)+~P7(x6504,x6503,x6502,x6501)+E(f54(x6501,x6502,x6503,x6504),x6502)+E(f31(f52(x6501,x6502,x6503,x6504),f53(x6501,x6502,x6503,x6504),f56(x6501,x6502,x6503,x6504)),x6503)+E(f82(f95(f46(x6501,x6502,x6503,x6504),f50(x6501,x6502,x6503,x6504),f47(x6501,x6502,x6503,x6504)),f95(f46(x6501,x6502,x6503,x6504),f50(x6501,x6502,x6503,x6504),f51(x6501,x6502,x6503,x6504))),x6504)
% 0.57/1.05 [655]P8(x6554,x6553,x6552,x6551)+~P7(x6554,x6553,x6552,x6551)+E(f52(x6551,x6552,x6553,x6554),f48(x6551,x6552,x6553,x6554))+E(f31(f57(x6551,x6552,x6553,x6554),f58(x6551,x6552,x6553,x6554),f59(x6551,x6552,x6553,x6554)),x6553)+E(f82(f95(f46(x6551,x6552,x6553,x6554),f50(x6551,x6552,x6553,x6554),f47(x6551,x6552,x6553,x6554)),f95(f46(x6551,x6552,x6553,x6554),f50(x6551,x6552,x6553,x6554),f51(x6551,x6552,x6553,x6554))),x6554)
% 0.57/1.05 [656]P8(x6564,x6563,x6562,x6561)+~P7(x6564,x6563,x6562,x6561)+~E(f57(x6561,x6562,x6563,x6564),f55(x6561,x6562,x6563,x6564))+E(f31(f52(x6561,x6562,x6563,x6564),f53(x6561,x6562,x6563,x6564),f56(x6561,x6562,x6563,x6564)),x6564)+E(f82(f95(f46(x6561,x6562,x6563,x6564),f50(x6561,x6562,x6563,x6564),f47(x6561,x6562,x6563,x6564)),f95(f46(x6561,x6562,x6563,x6564),f50(x6561,x6562,x6563,x6564),f51(x6561,x6562,x6563,x6564))),x6564)
% 0.57/1.05 [657]P8(x6574,x6573,x6572,x6571)+~P7(x6574,x6573,x6572,x6571)+~E(f57(x6571,x6572,x6573,x6574),f55(x6571,x6572,x6573,x6574))+E(f31(f52(x6571,x6572,x6573,x6574),f53(x6571,x6572,x6573,x6574),f56(x6571,x6572,x6573,x6574)),x6573)+E(f82(f95(f46(x6571,x6572,x6573,x6574),f50(x6571,x6572,x6573,x6574),f47(x6571,x6572,x6573,x6574)),f95(f46(x6571,x6572,x6573,x6574),f50(x6571,x6572,x6573,x6574),f51(x6571,x6572,x6573,x6574))),x6574)
% 0.57/1.05 [658]P8(x6584,x6583,x6582,x6581)+~P7(x6584,x6583,x6582,x6581)+P9(f57(x6581,x6582,x6583,x6584),f54(x6581,x6582,x6583,x6584))+E(f31(f52(x6581,x6582,x6583,x6584),f53(x6581,x6582,x6583,x6584),f56(x6581,x6582,x6583,x6584)),x6584)+E(f82(f95(f46(x6581,x6582,x6583,x6584),f50(x6581,x6582,x6583,x6584),f47(x6581,x6582,x6583,x6584)),f95(f46(x6581,x6582,x6583,x6584),f50(x6581,x6582,x6583,x6584),f51(x6581,x6582,x6583,x6584))),x6584)
% 0.57/1.05 [659]P8(x6594,x6593,x6592,x6591)+~P7(x6594,x6593,x6592,x6591)+P9(f57(x6591,x6592,x6593,x6594),f54(x6591,x6592,x6593,x6594))+E(f31(f52(x6591,x6592,x6593,x6594),f53(x6591,x6592,x6593,x6594),f56(x6591,x6592,x6593,x6594)),x6593)+E(f82(f95(f46(x6591,x6592,x6593,x6594),f50(x6591,x6592,x6593,x6594),f47(x6591,x6592,x6593,x6594)),f95(f46(x6591,x6592,x6593,x6594),f50(x6591,x6592,x6593,x6594),f51(x6591,x6592,x6593,x6594))),x6594)
% 0.57/1.05 [662]P8(x6624,x6623,x6622,x6621)+~P7(x6624,x6623,x6622,x6621)+E(f31(f57(x6621,x6622,x6623,x6624),f58(x6621,x6622,x6623,x6624),f59(x6621,x6622,x6623,x6624)),x6623)+E(f31(f52(x6621,x6622,x6623,x6624),f53(x6621,x6622,x6623,x6624),f56(x6621,x6622,x6623,x6624)),x6624)+E(f82(f95(f46(x6621,x6622,x6623,x6624),f50(x6621,x6622,x6623,x6624),f47(x6621,x6622,x6623,x6624)),f95(f46(x6621,x6622,x6623,x6624),f50(x6621,x6622,x6623,x6624),f51(x6621,x6622,x6623,x6624))),x6624)
% 0.57/1.05 [663]P8(x6634,x6633,x6632,x6631)+~P7(x6634,x6633,x6632,x6631)+E(f31(f57(x6631,x6632,x6633,x6634),f58(x6631,x6632,x6633,x6634),f59(x6631,x6632,x6633,x6634)),x6633)+E(f31(f52(x6631,x6632,x6633,x6634),f53(x6631,x6632,x6633,x6634),f56(x6631,x6632,x6633,x6634)),x6633)+E(f82(f95(f46(x6631,x6632,x6633,x6634),f50(x6631,x6632,x6633,x6634),f47(x6631,x6632,x6633,x6634)),f95(f46(x6631,x6632,x6633,x6634),f50(x6631,x6632,x6633,x6634),f51(x6631,x6632,x6633,x6634))),x6634)
% 0.57/1.05 [628]P8(x6284,x6283,x6282,x6281)+~P7(x6284,x6283,x6282,x6281)+E(f49(x6281,x6282,x6283,x6284),x6282)+E(f50(x6281,x6282,x6283,x6284),x6282)+E(f90(f82(f82(f54(x6281,x6282,x6283,x6284),f59(x6281,x6282,x6283,x6284)),f94(f55(x6281,x6282,x6283,x6284)))),f60(x6281,x6282,x6283,x6284))
% 0.57/1.05 [629]P8(x6294,x6293,x6292,x6291)+~P7(x6294,x6293,x6292,x6291)+E(f48(x6291,x6292,x6293,x6294),x6291)+E(f50(x6291,x6292,x6293,x6294),x6292)+E(f90(f82(f82(f54(x6291,x6292,x6293,x6294),f59(x6291,x6292,x6293,x6294)),f94(f55(x6291,x6292,x6293,x6294)))),f60(x6291,x6292,x6293,x6294))
% 0.57/1.05 [630]P8(x6304,x6303,x6302,x6301)+~P7(x6304,x6303,x6302,x6301)+E(f46(x6301,x6302,x6303,x6304),x6301)+E(f49(x6301,x6302,x6303,x6304),x6302)+E(f90(f82(f82(f54(x6301,x6302,x6303,x6304),f59(x6301,x6302,x6303,x6304)),f94(f55(x6301,x6302,x6303,x6304)))),f60(x6301,x6302,x6303,x6304))
% 0.57/1.05 [631]P8(x6314,x6313,x6312,x6311)+~P7(x6314,x6313,x6312,x6311)+E(f48(x6311,x6312,x6313,x6314),x6311)+E(f46(x6311,x6312,x6313,x6314),x6311)+E(f90(f82(f82(f54(x6311,x6312,x6313,x6314),f59(x6311,x6312,x6313,x6314)),f94(f55(x6311,x6312,x6313,x6314)))),f60(x6311,x6312,x6313,x6314))
% 0.57/1.05 [634]P8(x6344,x6343,x6342,x6341)+~P7(x6344,x6343,x6342,x6341)+E(f52(x6341,x6342,x6343,x6344),f48(x6341,x6342,x6343,x6344))+E(f50(x6341,x6342,x6343,x6344),x6342)+E(f90(f82(f82(f54(x6341,x6342,x6343,x6344),f59(x6341,x6342,x6343,x6344)),f94(f55(x6341,x6342,x6343,x6344)))),f60(x6341,x6342,x6343,x6344))
% 0.57/1.05 [635]P8(x6354,x6353,x6352,x6351)+~P7(x6354,x6353,x6352,x6351)+E(f52(x6351,x6352,x6353,x6354),f48(x6351,x6352,x6353,x6354))+E(f46(x6351,x6352,x6353,x6354),x6351)+E(f90(f82(f82(f54(x6351,x6352,x6353,x6354),f59(x6351,x6352,x6353,x6354)),f94(f55(x6351,x6352,x6353,x6354)))),f60(x6351,x6352,x6353,x6354))
% 0.57/1.05 [641]P8(x6414,x6413,x6412,x6411)+~P7(x6414,x6413,x6412,x6411)+E(f49(x6411,x6412,x6413,x6414),x6412)+E(f82(f47(x6411,x6412,x6413,x6414),f51(x6411,x6412,x6413,x6414)),x6413)+E(f90(f82(f82(f54(x6411,x6412,x6413,x6414),f59(x6411,x6412,x6413,x6414)),f94(f55(x6411,x6412,x6413,x6414)))),f60(x6411,x6412,x6413,x6414))
% 0.57/1.05 [642]P8(x6424,x6423,x6422,x6421)+~P7(x6424,x6423,x6422,x6421)+E(f48(x6421,x6422,x6423,x6424),x6421)+E(f82(f47(x6421,x6422,x6423,x6424),f51(x6421,x6422,x6423,x6424)),x6423)+E(f90(f82(f82(f54(x6421,x6422,x6423,x6424),f59(x6421,x6422,x6423,x6424)),f94(f55(x6421,x6422,x6423,x6424)))),f60(x6421,x6422,x6423,x6424))
% 0.57/1.05 [644]P8(x6444,x6443,x6442,x6441)+~P7(x6444,x6443,x6442,x6441)+E(f52(x6441,x6442,x6443,x6444),f48(x6441,x6442,x6443,x6444))+E(f82(f47(x6441,x6442,x6443,x6444),f51(x6441,x6442,x6443,x6444)),x6443)+E(f90(f82(f82(f54(x6441,x6442,x6443,x6444),f59(x6441,x6442,x6443,x6444)),f94(f55(x6441,x6442,x6443,x6444)))),f60(x6441,x6442,x6443,x6444))
% 0.57/1.05 [651]P8(x6514,x6513,x6512,x6511)+~P7(x6514,x6513,x6512,x6511)+E(f50(x6511,x6512,x6513,x6514),x6512)+E(f31(f52(x6511,x6512,x6513,x6514),f53(x6511,x6512,x6513,x6514),f56(x6511,x6512,x6513,x6514)),x6514)+E(f90(f82(f82(f54(x6511,x6512,x6513,x6514),f59(x6511,x6512,x6513,x6514)),f94(f55(x6511,x6512,x6513,x6514)))),f60(x6511,x6512,x6513,x6514))
% 0.57/1.05 [652]P8(x6524,x6523,x6522,x6521)+~P7(x6524,x6523,x6522,x6521)+E(f50(x6521,x6522,x6523,x6524),x6522)+E(f31(f52(x6521,x6522,x6523,x6524),f53(x6521,x6522,x6523,x6524),f56(x6521,x6522,x6523,x6524)),x6523)+E(f90(f82(f82(f54(x6521,x6522,x6523,x6524),f59(x6521,x6522,x6523,x6524)),f94(f55(x6521,x6522,x6523,x6524)))),f60(x6521,x6522,x6523,x6524))
% 0.57/1.05 [653]P8(x6534,x6533,x6532,x6531)+~P7(x6534,x6533,x6532,x6531)+E(f46(x6531,x6532,x6533,x6534),x6531)+E(f31(f52(x6531,x6532,x6533,x6534),f53(x6531,x6532,x6533,x6534),f56(x6531,x6532,x6533,x6534)),x6534)+E(f90(f82(f82(f54(x6531,x6532,x6533,x6534),f59(x6531,x6532,x6533,x6534)),f94(f55(x6531,x6532,x6533,x6534)))),f60(x6531,x6532,x6533,x6534))
% 0.57/1.05 [654]P8(x6544,x6543,x6542,x6541)+~P7(x6544,x6543,x6542,x6541)+E(f46(x6541,x6542,x6543,x6544),x6541)+E(f31(f52(x6541,x6542,x6543,x6544),f53(x6541,x6542,x6543,x6544),f56(x6541,x6542,x6543,x6544)),x6543)+E(f90(f82(f82(f54(x6541,x6542,x6543,x6544),f59(x6541,x6542,x6543,x6544)),f94(f55(x6541,x6542,x6543,x6544)))),f60(x6541,x6542,x6543,x6544))
% 0.57/1.05 [660]P8(x6604,x6603,x6602,x6601)+~P7(x6604,x6603,x6602,x6601)+E(f31(f52(x6601,x6602,x6603,x6604),f53(x6601,x6602,x6603,x6604),f56(x6601,x6602,x6603,x6604)),x6604)+E(f82(f47(x6601,x6602,x6603,x6604),f51(x6601,x6602,x6603,x6604)),x6603)+E(f90(f82(f82(f54(x6601,x6602,x6603,x6604),f59(x6601,x6602,x6603,x6604)),f94(f55(x6601,x6602,x6603,x6604)))),f60(x6601,x6602,x6603,x6604))
% 0.57/1.05 [661]P8(x6614,x6613,x6612,x6611)+~P7(x6614,x6613,x6612,x6611)+E(f31(f52(x6611,x6612,x6613,x6614),f53(x6611,x6612,x6613,x6614),f56(x6611,x6612,x6613,x6614)),x6613)+E(f82(f47(x6611,x6612,x6613,x6614),f51(x6611,x6612,x6613,x6614)),x6613)+E(f90(f82(f82(f54(x6611,x6612,x6613,x6614),f59(x6611,x6612,x6613,x6614)),f94(f55(x6611,x6612,x6613,x6614)))),f60(x6611,x6612,x6613,x6614))
% 0.57/1.05 [664]P8(x6644,x6643,x6642,x6641)+~P7(x6644,x6643,x6642,x6641)+E(f49(x6641,x6642,x6643,x6644),x6642)+E(f50(x6641,x6642,x6643,x6644),x6642)+E(f95(f55(x6641,x6642,x6643,x6644),f54(x6641,x6642,x6643,x6644),f31(f60(x6641,x6642,x6643,x6644),f58(x6641,x6642,x6643,x6644),f95(f57(x6641,x6642,x6643,x6644),f94(f60(x6641,x6642,x6643,x6644)),f59(x6641,x6642,x6643,x6644)))),x6644)
% 0.57/1.05 [665]P8(x6654,x6653,x6652,x6651)+~P7(x6654,x6653,x6652,x6651)+E(f48(x6651,x6652,x6653,x6654),x6651)+E(f50(x6651,x6652,x6653,x6654),x6652)+E(f95(f55(x6651,x6652,x6653,x6654),f54(x6651,x6652,x6653,x6654),f31(f60(x6651,x6652,x6653,x6654),f58(x6651,x6652,x6653,x6654),f95(f57(x6651,x6652,x6653,x6654),f94(f60(x6651,x6652,x6653,x6654)),f59(x6651,x6652,x6653,x6654)))),x6654)
% 0.57/1.05 [666]P8(x6664,x6663,x6662,x6661)+~P7(x6664,x6663,x6662,x6661)+E(f46(x6661,x6662,x6663,x6664),x6661)+E(f49(x6661,x6662,x6663,x6664),x6662)+E(f95(f55(x6661,x6662,x6663,x6664),f54(x6661,x6662,x6663,x6664),f31(f60(x6661,x6662,x6663,x6664),f58(x6661,x6662,x6663,x6664),f95(f57(x6661,x6662,x6663,x6664),f94(f60(x6661,x6662,x6663,x6664)),f59(x6661,x6662,x6663,x6664)))),x6664)
% 0.57/1.05 [667]P8(x6674,x6673,x6672,x6671)+~P7(x6674,x6673,x6672,x6671)+E(f48(x6671,x6672,x6673,x6674),x6671)+E(f46(x6671,x6672,x6673,x6674),x6671)+E(f95(f55(x6671,x6672,x6673,x6674),f54(x6671,x6672,x6673,x6674),f31(f60(x6671,x6672,x6673,x6674),f58(x6671,x6672,x6673,x6674),f95(f57(x6671,x6672,x6673,x6674),f94(f60(x6671,x6672,x6673,x6674)),f59(x6671,x6672,x6673,x6674)))),x6674)
% 0.57/1.05 [668]P8(x6684,x6683,x6682,x6681)+~P7(x6684,x6683,x6682,x6681)+E(f52(x6681,x6682,x6683,x6684),f48(x6681,x6682,x6683,x6684))+E(f50(x6681,x6682,x6683,x6684),x6682)+E(f95(f55(x6681,x6682,x6683,x6684),f54(x6681,x6682,x6683,x6684),f31(f60(x6681,x6682,x6683,x6684),f58(x6681,x6682,x6683,x6684),f95(f57(x6681,x6682,x6683,x6684),f94(f60(x6681,x6682,x6683,x6684)),f59(x6681,x6682,x6683,x6684)))),x6684)
% 0.57/1.05 [669]P8(x6694,x6693,x6692,x6691)+~P7(x6694,x6693,x6692,x6691)+E(f52(x6691,x6692,x6693,x6694),f48(x6691,x6692,x6693,x6694))+E(f46(x6691,x6692,x6693,x6694),x6691)+E(f95(f55(x6691,x6692,x6693,x6694),f54(x6691,x6692,x6693,x6694),f31(f60(x6691,x6692,x6693,x6694),f58(x6691,x6692,x6693,x6694),f95(f57(x6691,x6692,x6693,x6694),f94(f60(x6691,x6692,x6693,x6694)),f59(x6691,x6692,x6693,x6694)))),x6694)
% 0.57/1.05 [670]P8(x6704,x6703,x6702,x6701)+~P7(x6704,x6703,x6702,x6701)+E(f49(x6701,x6702,x6703,x6704),x6702)+E(f82(f47(x6701,x6702,x6703,x6704),f51(x6701,x6702,x6703,x6704)),x6703)+E(f95(f55(x6701,x6702,x6703,x6704),f54(x6701,x6702,x6703,x6704),f31(f60(x6701,x6702,x6703,x6704),f58(x6701,x6702,x6703,x6704),f95(f57(x6701,x6702,x6703,x6704),f94(f60(x6701,x6702,x6703,x6704)),f59(x6701,x6702,x6703,x6704)))),x6704)
% 0.57/1.05 [671]P8(x6714,x6713,x6712,x6711)+~P7(x6714,x6713,x6712,x6711)+E(f48(x6711,x6712,x6713,x6714),x6711)+E(f82(f47(x6711,x6712,x6713,x6714),f51(x6711,x6712,x6713,x6714)),x6713)+E(f95(f55(x6711,x6712,x6713,x6714),f54(x6711,x6712,x6713,x6714),f31(f60(x6711,x6712,x6713,x6714),f58(x6711,x6712,x6713,x6714),f95(f57(x6711,x6712,x6713,x6714),f94(f60(x6711,x6712,x6713,x6714)),f59(x6711,x6712,x6713,x6714)))),x6714)
% 0.57/1.05 [672]P8(x6724,x6723,x6722,x6721)+~P7(x6724,x6723,x6722,x6721)+E(f49(x6721,x6722,x6723,x6724),x6722)+E(f82(f95(f46(x6721,x6722,x6723,x6724),f50(x6721,x6722,x6723,x6724),f47(x6721,x6722,x6723,x6724)),f95(f46(x6721,x6722,x6723,x6724),f50(x6721,x6722,x6723,x6724),f51(x6721,x6722,x6723,x6724))),x6724)+E(f90(f82(f82(f54(x6721,x6722,x6723,x6724),f59(x6721,x6722,x6723,x6724)),f94(f55(x6721,x6722,x6723,x6724)))),f60(x6721,x6722,x6723,x6724))
% 0.57/1.05 [673]P8(x6734,x6733,x6732,x6731)+~P7(x6734,x6733,x6732,x6731)+E(f48(x6731,x6732,x6733,x6734),x6731)+E(f82(f95(f46(x6731,x6732,x6733,x6734),f50(x6731,x6732,x6733,x6734),f47(x6731,x6732,x6733,x6734)),f95(f46(x6731,x6732,x6733,x6734),f50(x6731,x6732,x6733,x6734),f51(x6731,x6732,x6733,x6734))),x6734)+E(f90(f82(f82(f54(x6731,x6732,x6733,x6734),f59(x6731,x6732,x6733,x6734)),f94(f55(x6731,x6732,x6733,x6734)))),f60(x6731,x6732,x6733,x6734))
% 0.57/1.05 [674]P8(x6744,x6743,x6742,x6741)+~P7(x6744,x6743,x6742,x6741)+E(f52(x6741,x6742,x6743,x6744),f48(x6741,x6742,x6743,x6744))+E(f82(f47(x6741,x6742,x6743,x6744),f51(x6741,x6742,x6743,x6744)),x6743)+E(f95(f55(x6741,x6742,x6743,x6744),f54(x6741,x6742,x6743,x6744),f31(f60(x6741,x6742,x6743,x6744),f58(x6741,x6742,x6743,x6744),f95(f57(x6741,x6742,x6743,x6744),f94(f60(x6741,x6742,x6743,x6744)),f59(x6741,x6742,x6743,x6744)))),x6744)
% 0.57/1.05 [675]P8(x6754,x6753,x6752,x6751)+~P7(x6754,x6753,x6752,x6751)+E(f52(x6751,x6752,x6753,x6754),f48(x6751,x6752,x6753,x6754))+E(f82(f95(f46(x6751,x6752,x6753,x6754),f50(x6751,x6752,x6753,x6754),f47(x6751,x6752,x6753,x6754)),f95(f46(x6751,x6752,x6753,x6754),f50(x6751,x6752,x6753,x6754),f51(x6751,x6752,x6753,x6754))),x6754)+E(f90(f82(f82(f54(x6751,x6752,x6753,x6754),f59(x6751,x6752,x6753,x6754)),f94(f55(x6751,x6752,x6753,x6754)))),f60(x6751,x6752,x6753,x6754))
% 0.57/1.05 [676]P8(x6764,x6763,x6762,x6761)+~P7(x6764,x6763,x6762,x6761)+E(f50(x6761,x6762,x6763,x6764),x6762)+E(f31(f52(x6761,x6762,x6763,x6764),f53(x6761,x6762,x6763,x6764),f56(x6761,x6762,x6763,x6764)),x6763)+E(f95(f55(x6761,x6762,x6763,x6764),f54(x6761,x6762,x6763,x6764),f31(f60(x6761,x6762,x6763,x6764),f58(x6761,x6762,x6763,x6764),f95(f57(x6761,x6762,x6763,x6764),f94(f60(x6761,x6762,x6763,x6764)),f59(x6761,x6762,x6763,x6764)))),x6764)
% 0.57/1.05 [677]P8(x6774,x6773,x6772,x6771)+~P7(x6774,x6773,x6772,x6771)+E(f50(x6771,x6772,x6773,x6774),x6772)+E(f31(f52(x6771,x6772,x6773,x6774),f53(x6771,x6772,x6773,x6774),f56(x6771,x6772,x6773,x6774)),x6774)+E(f95(f55(x6771,x6772,x6773,x6774),f54(x6771,x6772,x6773,x6774),f31(f60(x6771,x6772,x6773,x6774),f58(x6771,x6772,x6773,x6774),f95(f57(x6771,x6772,x6773,x6774),f94(f60(x6771,x6772,x6773,x6774)),f59(x6771,x6772,x6773,x6774)))),x6774)
% 0.57/1.05 [678]P8(x6784,x6783,x6782,x6781)+~P7(x6784,x6783,x6782,x6781)+E(f46(x6781,x6782,x6783,x6784),x6781)+E(f31(f52(x6781,x6782,x6783,x6784),f53(x6781,x6782,x6783,x6784),f56(x6781,x6782,x6783,x6784)),x6783)+E(f95(f55(x6781,x6782,x6783,x6784),f54(x6781,x6782,x6783,x6784),f31(f60(x6781,x6782,x6783,x6784),f58(x6781,x6782,x6783,x6784),f95(f57(x6781,x6782,x6783,x6784),f94(f60(x6781,x6782,x6783,x6784)),f59(x6781,x6782,x6783,x6784)))),x6784)
% 0.57/1.05 [679]P8(x6794,x6793,x6792,x6791)+~P7(x6794,x6793,x6792,x6791)+E(f46(x6791,x6792,x6793,x6794),x6791)+E(f31(f52(x6791,x6792,x6793,x6794),f53(x6791,x6792,x6793,x6794),f56(x6791,x6792,x6793,x6794)),x6794)+E(f95(f55(x6791,x6792,x6793,x6794),f54(x6791,x6792,x6793,x6794),f31(f60(x6791,x6792,x6793,x6794),f58(x6791,x6792,x6793,x6794),f95(f57(x6791,x6792,x6793,x6794),f94(f60(x6791,x6792,x6793,x6794)),f59(x6791,x6792,x6793,x6794)))),x6794)
% 0.57/1.05 [680]P8(x6804,x6803,x6802,x6801)+~P7(x6804,x6803,x6802,x6801)+E(f31(f52(x6801,x6802,x6803,x6804),f53(x6801,x6802,x6803,x6804),f56(x6801,x6802,x6803,x6804)),x6803)+E(f82(f47(x6801,x6802,x6803,x6804),f51(x6801,x6802,x6803,x6804)),x6803)+E(f95(f55(x6801,x6802,x6803,x6804),f54(x6801,x6802,x6803,x6804),f31(f60(x6801,x6802,x6803,x6804),f58(x6801,x6802,x6803,x6804),f95(f57(x6801,x6802,x6803,x6804),f94(f60(x6801,x6802,x6803,x6804)),f59(x6801,x6802,x6803,x6804)))),x6804)
% 0.57/1.05 [681]P8(x6814,x6813,x6812,x6811)+~P7(x6814,x6813,x6812,x6811)+E(f31(f52(x6811,x6812,x6813,x6814),f53(x6811,x6812,x6813,x6814),f56(x6811,x6812,x6813,x6814)),x6814)+E(f82(f47(x6811,x6812,x6813,x6814),f51(x6811,x6812,x6813,x6814)),x6813)+E(f95(f55(x6811,x6812,x6813,x6814),f54(x6811,x6812,x6813,x6814),f31(f60(x6811,x6812,x6813,x6814),f58(x6811,x6812,x6813,x6814),f95(f57(x6811,x6812,x6813,x6814),f94(f60(x6811,x6812,x6813,x6814)),f59(x6811,x6812,x6813,x6814)))),x6814)
% 0.57/1.05 [682]P8(x6824,x6823,x6822,x6821)+~P7(x6824,x6823,x6822,x6821)+E(f31(f52(x6821,x6822,x6823,x6824),f53(x6821,x6822,x6823,x6824),f56(x6821,x6822,x6823,x6824)),x6824)+E(f82(f95(f46(x6821,x6822,x6823,x6824),f50(x6821,x6822,x6823,x6824),f47(x6821,x6822,x6823,x6824)),f95(f46(x6821,x6822,x6823,x6824),f50(x6821,x6822,x6823,x6824),f51(x6821,x6822,x6823,x6824))),x6824)+E(f90(f82(f82(f54(x6821,x6822,x6823,x6824),f59(x6821,x6822,x6823,x6824)),f94(f55(x6821,x6822,x6823,x6824)))),f60(x6821,x6822,x6823,x6824))
% 0.57/1.05 [683]P8(x6834,x6833,x6832,x6831)+~P7(x6834,x6833,x6832,x6831)+E(f31(f52(x6831,x6832,x6833,x6834),f53(x6831,x6832,x6833,x6834),f56(x6831,x6832,x6833,x6834)),x6833)+E(f82(f95(f46(x6831,x6832,x6833,x6834),f50(x6831,x6832,x6833,x6834),f47(x6831,x6832,x6833,x6834)),f95(f46(x6831,x6832,x6833,x6834),f50(x6831,x6832,x6833,x6834),f51(x6831,x6832,x6833,x6834))),x6834)+E(f90(f82(f82(f54(x6831,x6832,x6833,x6834),f59(x6831,x6832,x6833,x6834)),f94(f55(x6831,x6832,x6833,x6834)))),f60(x6831,x6832,x6833,x6834))
% 0.57/1.05 [684]P8(x6844,x6843,x6842,x6841)+~P7(x6844,x6843,x6842,x6841)+E(f49(x6841,x6842,x6843,x6844),x6842)+E(f82(f95(f46(x6841,x6842,x6843,x6844),f50(x6841,x6842,x6843,x6844),f47(x6841,x6842,x6843,x6844)),f95(f46(x6841,x6842,x6843,x6844),f50(x6841,x6842,x6843,x6844),f51(x6841,x6842,x6843,x6844))),x6844)+E(f95(f55(x6841,x6842,x6843,x6844),f54(x6841,x6842,x6843,x6844),f31(f60(x6841,x6842,x6843,x6844),f58(x6841,x6842,x6843,x6844),f95(f57(x6841,x6842,x6843,x6844),f94(f60(x6841,x6842,x6843,x6844)),f59(x6841,x6842,x6843,x6844)))),x6844)
% 0.57/1.05 [685]P8(x6854,x6853,x6852,x6851)+~P7(x6854,x6853,x6852,x6851)+E(f48(x6851,x6852,x6853,x6854),x6851)+E(f82(f95(f46(x6851,x6852,x6853,x6854),f50(x6851,x6852,x6853,x6854),f47(x6851,x6852,x6853,x6854)),f95(f46(x6851,x6852,x6853,x6854),f50(x6851,x6852,x6853,x6854),f51(x6851,x6852,x6853,x6854))),x6854)+E(f95(f55(x6851,x6852,x6853,x6854),f54(x6851,x6852,x6853,x6854),f31(f60(x6851,x6852,x6853,x6854),f58(x6851,x6852,x6853,x6854),f95(f57(x6851,x6852,x6853,x6854),f94(f60(x6851,x6852,x6853,x6854)),f59(x6851,x6852,x6853,x6854)))),x6854)
% 0.57/1.05 [686]P8(x6864,x6863,x6862,x6861)+~P7(x6864,x6863,x6862,x6861)+E(f52(x6861,x6862,x6863,x6864),f48(x6861,x6862,x6863,x6864))+E(f82(f95(f46(x6861,x6862,x6863,x6864),f50(x6861,x6862,x6863,x6864),f47(x6861,x6862,x6863,x6864)),f95(f46(x6861,x6862,x6863,x6864),f50(x6861,x6862,x6863,x6864),f51(x6861,x6862,x6863,x6864))),x6864)+E(f95(f55(x6861,x6862,x6863,x6864),f54(x6861,x6862,x6863,x6864),f31(f60(x6861,x6862,x6863,x6864),f58(x6861,x6862,x6863,x6864),f95(f57(x6861,x6862,x6863,x6864),f94(f60(x6861,x6862,x6863,x6864)),f59(x6861,x6862,x6863,x6864)))),x6864)
% 0.57/1.05 [687]P8(x6874,x6873,x6872,x6871)+~P7(x6874,x6873,x6872,x6871)+E(f31(f52(x6871,x6872,x6873,x6874),f53(x6871,x6872,x6873,x6874),f56(x6871,x6872,x6873,x6874)),x6873)+E(f82(f95(f46(x6871,x6872,x6873,x6874),f50(x6871,x6872,x6873,x6874),f47(x6871,x6872,x6873,x6874)),f95(f46(x6871,x6872,x6873,x6874),f50(x6871,x6872,x6873,x6874),f51(x6871,x6872,x6873,x6874))),x6874)+E(f95(f55(x6871,x6872,x6873,x6874),f54(x6871,x6872,x6873,x6874),f31(f60(x6871,x6872,x6873,x6874),f58(x6871,x6872,x6873,x6874),f95(f57(x6871,x6872,x6873,x6874),f94(f60(x6871,x6872,x6873,x6874)),f59(x6871,x6872,x6873,x6874)))),x6874)
% 0.57/1.05 [688]P8(x6884,x6883,x6882,x6881)+~P7(x6884,x6883,x6882,x6881)+E(f31(f52(x6881,x6882,x6883,x6884),f53(x6881,x6882,x6883,x6884),f56(x6881,x6882,x6883,x6884)),x6884)+E(f82(f95(f46(x6881,x6882,x6883,x6884),f50(x6881,x6882,x6883,x6884),f47(x6881,x6882,x6883,x6884)),f95(f46(x6881,x6882,x6883,x6884),f50(x6881,x6882,x6883,x6884),f51(x6881,x6882,x6883,x6884))),x6884)+E(f95(f55(x6881,x6882,x6883,x6884),f54(x6881,x6882,x6883,x6884),f31(f60(x6881,x6882,x6883,x6884),f58(x6881,x6882,x6883,x6884),f95(f57(x6881,x6882,x6883,x6884),f94(f60(x6881,x6882,x6883,x6884)),f59(x6881,x6882,x6883,x6884)))),x6884)
% 0.57/1.05 [313]~P9(x3134,x3135)+P9(x3131,x3132)+P9(x3131,x3133)+~E(x3134,x3131)+~E(x3135,f82(x3133,x3132))
% 0.57/1.05 [341]~E(x3412,x3413)+~P9(x3412,x3416)+E(x3411,x3412)+P9(x3413,x3414)+~E(x3414,f31(x3411,x3415,x3416))
% 0.57/1.05 [334]~E(x3343,x3344)+~E(x3345,x3343)+E(x3341,f85(x3342))+~E(x3346,f83(x3344,x3342,x3347))+~E(x3341,f91(x3345,x3346))
% 0.57/1.05 [343]E(x3431,x3432)+~E(x3435,x3431)+E(x3433,f91(x3431,x3434))+~E(x3436,f83(x3432,x3437,x3434))+~E(x3433,f91(x3435,x3436))
% 0.57/1.05 [436]~P4(x4365)+~E(x4361,f93(x4366))+~E(x4365,f93(x4367))+~E(x4366,f82(f31(x4362,x4363,x4364),x4367))+E(x4361,f92(f82(f31(x4362,x4363,x4364),f89(x4365))))
% 0.57/1.05 [402]~E(x4026,x4023)+~E(x4027,x4022)+~E(x4021,f95(x4027,x4026,x4028))+~E(x4028,f82(x4024,x4025))+E(x4021,f82(f95(x4022,x4023,x4024),f95(x4022,x4023,x4025)))
% 0.57/1.05 [550]P4(x5504)+~E(x5501,f93(x5505))+~E(x5504,f93(x5503))+~E(x5505,f82(x5503,x5502))+E(x5501,a87)+E(f31(f11(x5502,x5503,x5504,x5505),f16(x5502,x5503,x5504,x5505),f17(x5502,x5503,x5504,x5505)),x5503)
% 0.57/1.05 [627]~P4(x6272)+~E(x6272,f93(x6274))+~E(x6271,f93(x6275))+~E(x6275,f82(x6274,x6273))+E(f31(f13(x6274,x6275,x6271,x6272,x6273),f14(x6274,x6275,x6271,x6272,x6273),f15(x6274,x6275,x6271,x6272,x6273)),x6274)+E(x6271,f92(f82(f89(x6272),x6273)))
% 0.57/1.05 [325]E(x3251,x3252)+~E(x3253,x3251)+~E(x3254,x3255)+~E(x3256,x3254)+~E(x3252,f95(x3256,x3253,x3257))+~E(x3257,f94(x3255))
% 0.57/1.05 [326]E(x3261,x3262)+~E(x3264,x3265)+~E(x3266,x3261)+~E(x3263,f95(x3266,x3264,x3267))+E(x3263,f94(x3262))+~E(x3267,f94(x3262))
% 0.57/1.05 [368]P2(x3682)+P4(x3683)+~E(x3683,f93(x3682))+E(x3681,a87)+~E(x3681,f93(x3684))+~E(x3684,f82(f31(x3685,x3686,x3687),x3682))
% 0.57/1.05 [400]~P2(x4003)+P4(x4005)+~E(x4005,f93(x4003))+~E(x4001,f93(x4006))+E(x4001,f92(f95(x4002,x4003,x4004)))+~E(x4006,f82(f31(x4002,x4007,x4004),x4003))
% 0.57/1.05 [373]~E(x3735,x3736)+~E(x3737,x3732)+~E(x3738,x3737)+E(x3731,f31(x3732,x3733,x3734))+~E(x3739,f31(x3732,x3733,x3734))+~E(x3731,f95(x3738,x3735,x3739))
% 0.57/1.05 [407]P9(x4072,x4075)+E(x4071,x4072)+~E(x4077,x4075)+~E(x4078,x4071)+~E(x4079,f31(x4072,x4074,x4076))+~E(x4073,f95(x4078,x4077,x4079))+E(x4073,f31(x4072,x4074,f95(x4071,x4075,x4076)))
% 0.57/1.05 [479]~P9(x4792,x4794)+E(x4791,x4792)+~E(x4798,x4794)+~E(x4799,x4791)+~E(x47910,f31(x4792,x4796,x4797))+~E(x4793,f95(x4799,x4798,x47910))+~E(x4795,f90(f82(f82(x4794,x4797),f94(x4791))))+E(x4793,f95(x4791,x4794,f31(x4795,x4796,f95(x4792,f94(x4795),x4797))))
% 0.57/1.05 %EqnAxiom
% 0.57/1.05 [1]E(x11,x11)
% 0.57/1.05 [2]E(x22,x21)+~E(x21,x22)
% 0.57/1.05 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.57/1.05 [4]~E(x41,x42)+E(f31(x41,x43,x44),f31(x42,x43,x44))
% 0.57/1.05 [5]~E(x51,x52)+E(f31(x53,x51,x54),f31(x53,x52,x54))
% 0.57/1.05 [6]~E(x61,x62)+E(f31(x63,x64,x61),f31(x63,x64,x62))
% 0.57/1.05 [7]~E(x71,x72)+E(f85(x71),f85(x72))
% 0.57/1.05 [8]~E(x81,x82)+E(f92(x81),f92(x82))
% 0.57/1.05 [9]~E(x91,x92)+E(f94(x91),f94(x92))
% 0.57/1.05 [10]~E(x101,x102)+E(f82(x101,x103),f82(x102,x103))
% 0.57/1.05 [11]~E(x111,x112)+E(f82(x113,x111),f82(x113,x112))
% 0.57/1.05 [12]~E(x121,x122)+E(f83(x121,x123,x124),f83(x122,x123,x124))
% 0.57/1.05 [13]~E(x131,x132)+E(f83(x133,x131,x134),f83(x133,x132,x134))
% 0.57/1.05 [14]~E(x141,x142)+E(f83(x143,x144,x141),f83(x143,x144,x142))
% 0.57/1.05 [15]~E(x151,x152)+E(f60(x151,x153,x154,x155),f60(x152,x153,x154,x155))
% 0.57/1.05 [16]~E(x161,x162)+E(f60(x163,x161,x164,x165),f60(x163,x162,x164,x165))
% 0.57/1.05 [17]~E(x171,x172)+E(f60(x173,x174,x171,x175),f60(x173,x174,x172,x175))
% 0.57/1.05 [18]~E(x181,x182)+E(f60(x183,x184,x185,x181),f60(x183,x184,x185,x182))
% 0.57/1.05 [19]~E(x191,x192)+E(f95(x191,x193,x194),f95(x192,x193,x194))
% 0.57/1.05 [20]~E(x201,x202)+E(f95(x203,x201,x204),f95(x203,x202,x204))
% 0.57/1.05 [21]~E(x211,x212)+E(f95(x213,x214,x211),f95(x213,x214,x212))
% 0.57/1.05 [22]~E(x221,x222)+E(f90(x221),f90(x222))
% 0.57/1.05 [23]~E(x231,x232)+E(f49(x231,x233,x234,x235),f49(x232,x233,x234,x235))
% 0.57/1.05 [24]~E(x241,x242)+E(f49(x243,x241,x244,x245),f49(x243,x242,x244,x245))
% 0.57/1.05 [25]~E(x251,x252)+E(f49(x253,x254,x251,x255),f49(x253,x254,x252,x255))
% 0.57/1.05 [26]~E(x261,x262)+E(f49(x263,x264,x265,x261),f49(x263,x264,x265,x262))
% 0.57/1.05 [27]~E(x271,x272)+E(f59(x271,x273,x274,x275),f59(x272,x273,x274,x275))
% 0.57/1.05 [28]~E(x281,x282)+E(f59(x283,x281,x284,x285),f59(x283,x282,x284,x285))
% 0.57/1.05 [29]~E(x291,x292)+E(f59(x293,x294,x291,x295),f59(x293,x294,x292,x295))
% 0.57/1.05 [30]~E(x301,x302)+E(f59(x303,x304,x305,x301),f59(x303,x304,x305,x302))
% 0.57/1.05 [31]~E(x311,x312)+E(f51(x311,x313,x314,x315),f51(x312,x313,x314,x315))
% 0.57/1.05 [32]~E(x321,x322)+E(f51(x323,x321,x324,x325),f51(x323,x322,x324,x325))
% 0.57/1.05 [33]~E(x331,x332)+E(f51(x333,x334,x331,x335),f51(x333,x334,x332,x335))
% 0.57/1.05 [34]~E(x341,x342)+E(f51(x343,x344,x345,x341),f51(x343,x344,x345,x342))
% 0.57/1.05 [35]~E(x351,x352)+E(f93(x351),f93(x352))
% 0.57/1.05 [36]~E(x361,x362)+E(f50(x361,x363,x364,x365),f50(x362,x363,x364,x365))
% 0.57/1.05 [37]~E(x371,x372)+E(f50(x373,x371,x374,x375),f50(x373,x372,x374,x375))
% 0.57/1.05 [38]~E(x381,x382)+E(f50(x383,x384,x381,x385),f50(x383,x384,x382,x385))
% 0.57/1.05 [39]~E(x391,x392)+E(f50(x393,x394,x395,x391),f50(x393,x394,x395,x392))
% 0.57/1.05 [40]~E(x401,x402)+E(f54(x401,x403,x404,x405),f54(x402,x403,x404,x405))
% 0.57/1.05 [41]~E(x411,x412)+E(f54(x413,x411,x414,x415),f54(x413,x412,x414,x415))
% 0.57/1.05 [42]~E(x421,x422)+E(f54(x423,x424,x421,x425),f54(x423,x424,x422,x425))
% 0.57/1.05 [43]~E(x431,x432)+E(f54(x433,x434,x435,x431),f54(x433,x434,x435,x432))
% 0.57/1.05 [44]~E(x441,x442)+E(f55(x441,x443,x444,x445),f55(x442,x443,x444,x445))
% 0.57/1.05 [45]~E(x451,x452)+E(f55(x453,x451,x454,x455),f55(x453,x452,x454,x455))
% 0.57/1.05 [46]~E(x461,x462)+E(f55(x463,x464,x461,x465),f55(x463,x464,x462,x465))
% 0.57/1.05 [47]~E(x471,x472)+E(f55(x473,x474,x475,x471),f55(x473,x474,x475,x472))
% 0.57/1.05 [48]~E(x481,x482)+E(f46(x481,x483,x484,x485),f46(x482,x483,x484,x485))
% 0.57/1.05 [49]~E(x491,x492)+E(f46(x493,x491,x494,x495),f46(x493,x492,x494,x495))
% 0.57/1.05 [50]~E(x501,x502)+E(f46(x503,x504,x501,x505),f46(x503,x504,x502,x505))
% 0.57/1.05 [51]~E(x511,x512)+E(f46(x513,x514,x515,x511),f46(x513,x514,x515,x512))
% 0.57/1.05 [52]~E(x521,x522)+E(f57(x521,x523,x524,x525),f57(x522,x523,x524,x525))
% 0.57/1.05 [53]~E(x531,x532)+E(f57(x533,x531,x534,x535),f57(x533,x532,x534,x535))
% 0.57/1.05 [54]~E(x541,x542)+E(f57(x543,x544,x541,x545),f57(x543,x544,x542,x545))
% 0.57/1.05 [55]~E(x551,x552)+E(f57(x553,x554,x555,x551),f57(x553,x554,x555,x552))
% 0.57/1.05 [56]~E(x561,x562)+E(f91(x561,x563),f91(x562,x563))
% 0.57/1.05 [57]~E(x571,x572)+E(f91(x573,x571),f91(x573,x572))
% 0.57/1.05 [58]~E(x581,x582)+E(f47(x581,x583,x584,x585),f47(x582,x583,x584,x585))
% 0.57/1.05 [59]~E(x591,x592)+E(f47(x593,x591,x594,x595),f47(x593,x592,x594,x595))
% 0.57/1.05 [60]~E(x601,x602)+E(f47(x603,x604,x601,x605),f47(x603,x604,x602,x605))
% 0.57/1.05 [61]~E(x611,x612)+E(f47(x613,x614,x615,x611),f47(x613,x614,x615,x612))
% 0.57/1.05 [62]~E(x621,x622)+E(f48(x621,x623,x624,x625),f48(x622,x623,x624,x625))
% 0.57/1.05 [63]~E(x631,x632)+E(f48(x633,x631,x634,x635),f48(x633,x632,x634,x635))
% 0.57/1.05 [64]~E(x641,x642)+E(f48(x643,x644,x641,x645),f48(x643,x644,x642,x645))
% 0.57/1.05 [65]~E(x651,x652)+E(f48(x653,x654,x655,x651),f48(x653,x654,x655,x652))
% 0.57/1.05 [66]~E(x661,x662)+E(f44(x661,x663,x664,x665),f44(x662,x663,x664,x665))
% 0.57/1.05 [67]~E(x671,x672)+E(f44(x673,x671,x674,x675),f44(x673,x672,x674,x675))
% 0.57/1.05 [68]~E(x681,x682)+E(f44(x683,x684,x681,x685),f44(x683,x684,x682,x685))
% 0.57/1.05 [69]~E(x691,x692)+E(f44(x693,x694,x695,x691),f44(x693,x694,x695,x692))
% 0.57/1.05 [70]~E(x701,x702)+E(f45(x701,x703,x704,x705),f45(x702,x703,x704,x705))
% 0.57/1.05 [71]~E(x711,x712)+E(f45(x713,x711,x714,x715),f45(x713,x712,x714,x715))
% 0.57/1.05 [72]~E(x721,x722)+E(f45(x723,x724,x721,x725),f45(x723,x724,x722,x725))
% 0.57/1.05 [73]~E(x731,x732)+E(f45(x733,x734,x735,x731),f45(x733,x734,x735,x732))
% 0.57/1.05 [74]~E(x741,x742)+E(f70(x741,x743),f70(x742,x743))
% 0.57/1.05 [75]~E(x751,x752)+E(f70(x753,x751),f70(x753,x752))
% 0.57/1.05 [76]~E(x761,x762)+E(f40(x761,x763,x764,x765),f40(x762,x763,x764,x765))
% 0.57/1.05 [77]~E(x771,x772)+E(f40(x773,x771,x774,x775),f40(x773,x772,x774,x775))
% 0.57/1.05 [78]~E(x781,x782)+E(f40(x783,x784,x781,x785),f40(x783,x784,x782,x785))
% 0.57/1.05 [79]~E(x791,x792)+E(f40(x793,x794,x795,x791),f40(x793,x794,x795,x792))
% 0.57/1.05 [80]~E(x801,x802)+E(f88(x801),f88(x802))
% 0.57/1.05 [81]~E(x811,x812)+E(f41(x811,x813,x814,x815),f41(x812,x813,x814,x815))
% 0.57/1.05 [82]~E(x821,x822)+E(f41(x823,x821,x824,x825),f41(x823,x822,x824,x825))
% 0.57/1.05 [83]~E(x831,x832)+E(f41(x833,x834,x831,x835),f41(x833,x834,x832,x835))
% 0.57/1.05 [84]~E(x841,x842)+E(f41(x843,x844,x845,x841),f41(x843,x844,x845,x842))
% 0.57/1.05 [85]~E(x851,x852)+E(f89(x851),f89(x852))
% 0.57/1.05 [86]~E(x861,x862)+E(f53(x861,x863,x864,x865),f53(x862,x863,x864,x865))
% 0.57/1.05 [87]~E(x871,x872)+E(f53(x873,x871,x874,x875),f53(x873,x872,x874,x875))
% 0.57/1.05 [88]~E(x881,x882)+E(f53(x883,x884,x881,x885),f53(x883,x884,x882,x885))
% 0.57/1.05 [89]~E(x891,x892)+E(f53(x893,x894,x895,x891),f53(x893,x894,x895,x892))
% 0.57/1.05 [90]~E(x901,x902)+E(f81(x901,x903,x904),f81(x902,x903,x904))
% 0.57/1.05 [91]~E(x911,x912)+E(f81(x913,x911,x914),f81(x913,x912,x914))
% 0.57/1.05 [92]~E(x921,x922)+E(f81(x923,x924,x921),f81(x923,x924,x922))
% 0.57/1.05 [93]~E(x931,x932)+E(f21(x931,x933,x934),f21(x932,x933,x934))
% 0.57/1.05 [94]~E(x941,x942)+E(f21(x943,x941,x944),f21(x943,x942,x944))
% 0.57/1.05 [95]~E(x951,x952)+E(f21(x953,x954,x951),f21(x953,x954,x952))
% 0.57/1.05 [96]~E(x961,x962)+E(f56(x961,x963,x964,x965),f56(x962,x963,x964,x965))
% 0.57/1.05 [97]~E(x971,x972)+E(f56(x973,x971,x974,x975),f56(x973,x972,x974,x975))
% 0.57/1.05 [98]~E(x981,x982)+E(f56(x983,x984,x981,x985),f56(x983,x984,x982,x985))
% 0.57/1.05 [99]~E(x991,x992)+E(f56(x993,x994,x995,x991),f56(x993,x994,x995,x992))
% 0.57/1.05 [100]~E(x1001,x1002)+E(f58(x1001,x1003,x1004,x1005),f58(x1002,x1003,x1004,x1005))
% 0.57/1.05 [101]~E(x1011,x1012)+E(f58(x1013,x1011,x1014,x1015),f58(x1013,x1012,x1014,x1015))
% 0.57/1.05 [102]~E(x1021,x1022)+E(f58(x1023,x1024,x1021,x1025),f58(x1023,x1024,x1022,x1025))
% 0.57/1.05 [103]~E(x1031,x1032)+E(f58(x1033,x1034,x1035,x1031),f58(x1033,x1034,x1035,x1032))
% 0.57/1.05 [104]~E(x1041,x1042)+E(f74(x1041,x1043,x1044),f74(x1042,x1043,x1044))
% 0.57/1.05 [105]~E(x1051,x1052)+E(f74(x1053,x1051,x1054),f74(x1053,x1052,x1054))
% 0.57/1.05 [106]~E(x1061,x1062)+E(f74(x1063,x1064,x1061),f74(x1063,x1064,x1062))
% 0.57/1.05 [107]~E(x1071,x1072)+E(f24(x1071,x1073,x1074),f24(x1072,x1073,x1074))
% 0.57/1.05 [108]~E(x1081,x1082)+E(f24(x1083,x1081,x1084),f24(x1083,x1082,x1084))
% 0.57/1.05 [109]~E(x1091,x1092)+E(f24(x1093,x1094,x1091),f24(x1093,x1094,x1092))
% 0.57/1.05 [110]~E(x1101,x1102)+E(f35(x1101,x1103),f35(x1102,x1103))
% 0.57/1.05 [111]~E(x1111,x1112)+E(f35(x1113,x1111),f35(x1113,x1112))
% 0.57/1.05 [112]~E(x1121,x1122)+E(f37(x1121,x1123),f37(x1122,x1123))
% 0.57/1.05 [113]~E(x1131,x1132)+E(f37(x1133,x1131),f37(x1133,x1132))
% 0.57/1.05 [114]~E(x1141,x1142)+E(f67(x1141,x1143),f67(x1142,x1143))
% 0.57/1.05 [115]~E(x1151,x1152)+E(f67(x1153,x1151),f67(x1153,x1152))
% 0.57/1.05 [116]~E(x1161,x1162)+E(f22(x1161,x1163,x1164),f22(x1162,x1163,x1164))
% 0.57/1.05 [117]~E(x1171,x1172)+E(f22(x1173,x1171,x1174),f22(x1173,x1172,x1174))
% 0.57/1.05 [118]~E(x1181,x1182)+E(f22(x1183,x1184,x1181),f22(x1183,x1184,x1182))
% 0.57/1.05 [119]~E(x1191,x1192)+E(f84(x1191,x1193),f84(x1192,x1193))
% 0.57/1.05 [120]~E(x1201,x1202)+E(f84(x1203,x1201),f84(x1203,x1202))
% 0.57/1.05 [121]~E(x1211,x1212)+E(f63(x1211,x1213),f63(x1212,x1213))
% 0.57/1.05 [122]~E(x1221,x1222)+E(f63(x1223,x1221),f63(x1223,x1222))
% 0.57/1.05 [123]~E(x1231,x1232)+E(f62(x1231,x1233),f62(x1232,x1233))
% 0.57/1.05 [124]~E(x1241,x1242)+E(f62(x1243,x1241),f62(x1243,x1242))
% 0.57/1.05 [125]~E(x1251,x1252)+E(f73(x1251,x1253),f73(x1252,x1253))
% 0.57/1.05 [126]~E(x1261,x1262)+E(f73(x1263,x1261),f73(x1263,x1262))
% 0.57/1.05 [127]~E(x1271,x1272)+E(f52(x1271,x1273,x1274,x1275),f52(x1272,x1273,x1274,x1275))
% 0.57/1.05 [128]~E(x1281,x1282)+E(f52(x1283,x1281,x1284,x1285),f52(x1283,x1282,x1284,x1285))
% 0.57/1.05 [129]~E(x1291,x1292)+E(f52(x1293,x1294,x1291,x1295),f52(x1293,x1294,x1292,x1295))
% 0.57/1.05 [130]~E(x1301,x1302)+E(f52(x1303,x1304,x1305,x1301),f52(x1303,x1304,x1305,x1302))
% 0.57/1.05 [131]~E(x1311,x1312)+E(f6(x1311,x1313,x1314),f6(x1312,x1313,x1314))
% 0.57/1.05 [132]~E(x1321,x1322)+E(f6(x1323,x1321,x1324),f6(x1323,x1322,x1324))
% 0.57/1.05 [133]~E(x1331,x1332)+E(f6(x1333,x1334,x1331),f6(x1333,x1334,x1332))
% 0.57/1.05 [134]~E(x1341,x1342)+E(f4(x1341,x1343),f4(x1342,x1343))
% 0.57/1.05 [135]~E(x1351,x1352)+E(f4(x1353,x1351),f4(x1353,x1352))
% 0.57/1.05 [136]~E(x1361,x1362)+E(f20(x1361,x1363,x1364),f20(x1362,x1363,x1364))
% 0.57/1.05 [137]~E(x1371,x1372)+E(f20(x1373,x1371,x1374),f20(x1373,x1372,x1374))
% 0.57/1.05 [138]~E(x1381,x1382)+E(f20(x1383,x1384,x1381),f20(x1383,x1384,x1382))
% 0.57/1.05 [139]~E(x1391,x1392)+E(f18(x1391,x1393),f18(x1392,x1393))
% 0.57/1.05 [140]~E(x1401,x1402)+E(f18(x1403,x1401),f18(x1403,x1402))
% 0.57/1.05 [141]~E(x1411,x1412)+E(f23(x1411,x1413,x1414),f23(x1412,x1413,x1414))
% 0.57/1.05 [142]~E(x1421,x1422)+E(f23(x1423,x1421,x1424),f23(x1423,x1422,x1424))
% 0.57/1.05 [143]~E(x1431,x1432)+E(f23(x1433,x1434,x1431),f23(x1433,x1434,x1432))
% 0.57/1.05 [144]~E(x1441,x1442)+E(f32(x1441,x1443),f32(x1442,x1443))
% 0.57/1.05 [145]~E(x1451,x1452)+E(f32(x1453,x1451),f32(x1453,x1452))
% 0.57/1.05 [146]~E(x1461,x1462)+E(f64(x1461,x1463),f64(x1462,x1463))
% 0.57/1.05 [147]~E(x1471,x1472)+E(f64(x1473,x1471),f64(x1473,x1472))
% 0.57/1.05 [148]~E(x1481,x1482)+E(f43(x1481,x1483,x1484),f43(x1482,x1483,x1484))
% 0.57/1.05 [149]~E(x1491,x1492)+E(f43(x1493,x1491,x1494),f43(x1493,x1492,x1494))
% 0.57/1.05 [150]~E(x1501,x1502)+E(f43(x1503,x1504,x1501),f43(x1503,x1504,x1502))
% 0.57/1.05 [151]~E(x1511,x1512)+E(f34(x1511,x1513),f34(x1512,x1513))
% 0.57/1.05 [152]~E(x1521,x1522)+E(f34(x1523,x1521),f34(x1523,x1522))
% 0.57/1.05 [153]~E(x1531,x1532)+E(f33(x1531,x1533),f33(x1532,x1533))
% 0.57/1.05 [154]~E(x1541,x1542)+E(f33(x1543,x1541),f33(x1543,x1542))
% 0.57/1.05 [155]~E(x1551,x1552)+E(f28(x1551,x1553,x1554),f28(x1552,x1553,x1554))
% 0.57/1.05 [156]~E(x1561,x1562)+E(f28(x1563,x1561,x1564),f28(x1563,x1562,x1564))
% 0.57/1.05 [157]~E(x1571,x1572)+E(f28(x1573,x1574,x1571),f28(x1573,x1574,x1572))
% 0.57/1.05 [158]~E(x1581,x1582)+E(f38(x1581,x1583,x1584),f38(x1582,x1583,x1584))
% 0.57/1.05 [159]~E(x1591,x1592)+E(f38(x1593,x1591,x1594),f38(x1593,x1592,x1594))
% 0.57/1.05 [160]~E(x1601,x1602)+E(f38(x1603,x1604,x1601),f38(x1603,x1604,x1602))
% 0.57/1.05 [161]~E(x1611,x1612)+E(f61(x1611,x1613,x1614),f61(x1612,x1613,x1614))
% 0.57/1.05 [162]~E(x1621,x1622)+E(f61(x1623,x1621,x1624),f61(x1623,x1622,x1624))
% 0.57/1.05 [163]~E(x1631,x1632)+E(f61(x1633,x1634,x1631),f61(x1633,x1634,x1632))
% 0.57/1.05 [164]~E(x1641,x1642)+E(f68(x1641,x1643),f68(x1642,x1643))
% 0.57/1.05 [165]~E(x1651,x1652)+E(f68(x1653,x1651),f68(x1653,x1652))
% 0.57/1.05 [166]~E(x1661,x1662)+E(f27(x1661,x1663,x1664),f27(x1662,x1663,x1664))
% 0.57/1.05 [167]~E(x1671,x1672)+E(f27(x1673,x1671,x1674),f27(x1673,x1672,x1674))
% 0.57/1.05 [168]~E(x1681,x1682)+E(f27(x1683,x1684,x1681),f27(x1683,x1684,x1682))
% 0.57/1.05 [169]~E(x1691,x1692)+E(f66(x1691,x1693),f66(x1692,x1693))
% 0.57/1.05 [170]~E(x1701,x1702)+E(f66(x1703,x1701),f66(x1703,x1702))
% 0.57/1.05 [171]~E(x1711,x1712)+E(f65(x1711,x1713),f65(x1712,x1713))
% 0.57/1.05 [172]~E(x1721,x1722)+E(f65(x1723,x1721),f65(x1723,x1722))
% 0.57/1.05 [173]~E(x1731,x1732)+E(f14(x1731,x1733,x1734,x1735,x1736),f14(x1732,x1733,x1734,x1735,x1736))
% 0.57/1.05 [174]~E(x1741,x1742)+E(f14(x1743,x1741,x1744,x1745,x1746),f14(x1743,x1742,x1744,x1745,x1746))
% 0.57/1.05 [175]~E(x1751,x1752)+E(f14(x1753,x1754,x1751,x1755,x1756),f14(x1753,x1754,x1752,x1755,x1756))
% 0.57/1.05 [176]~E(x1761,x1762)+E(f14(x1763,x1764,x1765,x1761,x1766),f14(x1763,x1764,x1765,x1762,x1766))
% 0.57/1.05 [177]~E(x1771,x1772)+E(f14(x1773,x1774,x1775,x1776,x1771),f14(x1773,x1774,x1775,x1776,x1772))
% 0.57/1.05 [178]~E(x1781,x1782)+E(f42(x1781,x1783,x1784,x1785),f42(x1782,x1783,x1784,x1785))
% 0.57/1.05 [179]~E(x1791,x1792)+E(f42(x1793,x1791,x1794,x1795),f42(x1793,x1792,x1794,x1795))
% 0.57/1.05 [180]~E(x1801,x1802)+E(f42(x1803,x1804,x1801,x1805),f42(x1803,x1804,x1802,x1805))
% 0.57/1.05 [181]~E(x1811,x1812)+E(f42(x1813,x1814,x1815,x1811),f42(x1813,x1814,x1815,x1812))
% 0.57/1.05 [182]~E(x1821,x1822)+E(f36(x1821,x1823),f36(x1822,x1823))
% 0.57/1.05 [183]~E(x1831,x1832)+E(f36(x1833,x1831),f36(x1833,x1832))
% 0.57/1.05 [184]~E(x1841,x1842)+E(f5(x1841,x1843),f5(x1842,x1843))
% 0.57/1.05 [185]~E(x1851,x1852)+E(f5(x1853,x1851),f5(x1853,x1852))
% 0.57/1.05 [186]~E(x1861,x1862)+E(f26(x1861,x1863,x1864),f26(x1862,x1863,x1864))
% 0.57/1.05 [187]~E(x1871,x1872)+E(f26(x1873,x1871,x1874),f26(x1873,x1872,x1874))
% 0.57/1.05 [188]~E(x1881,x1882)+E(f26(x1883,x1884,x1881),f26(x1883,x1884,x1882))
% 0.57/1.05 [189]~E(x1891,x1892)+E(f39(x1891,x1893,x1894,x1895),f39(x1892,x1893,x1894,x1895))
% 0.57/1.05 [190]~E(x1901,x1902)+E(f39(x1903,x1901,x1904,x1905),f39(x1903,x1902,x1904,x1905))
% 0.57/1.05 [191]~E(x1911,x1912)+E(f39(x1913,x1914,x1911,x1915),f39(x1913,x1914,x1912,x1915))
% 0.57/1.05 [192]~E(x1921,x1922)+E(f39(x1923,x1924,x1925,x1921),f39(x1923,x1924,x1925,x1922))
% 0.57/1.05 [193]~E(x1931,x1932)+E(f69(x1931,x1933),f69(x1932,x1933))
% 0.57/1.05 [194]~E(x1941,x1942)+E(f69(x1943,x1941),f69(x1943,x1942))
% 0.57/1.05 [195]~E(x1951,x1952)+E(f79(x1951,x1953,x1954),f79(x1952,x1953,x1954))
% 0.57/1.05 [196]~E(x1961,x1962)+E(f79(x1963,x1961,x1964),f79(x1963,x1962,x1964))
% 0.57/1.05 [197]~E(x1971,x1972)+E(f79(x1973,x1974,x1971),f79(x1973,x1974,x1972))
% 0.57/1.05 [198]~E(x1981,x1982)+E(f25(x1981,x1983,x1984),f25(x1982,x1983,x1984))
% 0.57/1.05 [199]~E(x1991,x1992)+E(f25(x1993,x1991,x1994),f25(x1993,x1992,x1994))
% 0.57/1.05 [200]~E(x2001,x2002)+E(f25(x2003,x2004,x2001),f25(x2003,x2004,x2002))
% 0.57/1.05 [201]~E(x2011,x2012)+E(f80(x2011,x2013,x2014),f80(x2012,x2013,x2014))
% 0.57/1.05 [202]~E(x2021,x2022)+E(f80(x2023,x2021,x2024),f80(x2023,x2022,x2024))
% 0.57/1.05 [203]~E(x2031,x2032)+E(f80(x2033,x2034,x2031),f80(x2033,x2034,x2032))
% 0.57/1.05 [204]~E(x2041,x2042)+E(f78(x2041,x2043),f78(x2042,x2043))
% 0.57/1.05 [205]~E(x2051,x2052)+E(f78(x2053,x2051),f78(x2053,x2052))
% 0.57/1.05 [206]~E(x2061,x2062)+E(f11(x2061,x2063,x2064,x2065),f11(x2062,x2063,x2064,x2065))
% 0.57/1.05 [207]~E(x2071,x2072)+E(f11(x2073,x2071,x2074,x2075),f11(x2073,x2072,x2074,x2075))
% 0.57/1.05 [208]~E(x2081,x2082)+E(f11(x2083,x2084,x2081,x2085),f11(x2083,x2084,x2082,x2085))
% 0.57/1.05 [209]~E(x2091,x2092)+E(f11(x2093,x2094,x2095,x2091),f11(x2093,x2094,x2095,x2092))
% 0.57/1.05 [210]~E(x2101,x2102)+E(f72(x2101,x2103),f72(x2102,x2103))
% 0.57/1.05 [211]~E(x2111,x2112)+E(f72(x2113,x2111),f72(x2113,x2112))
% 0.57/1.05 [212]~E(x2121,x2122)+E(f10(x2121,x2123,x2124,x2125),f10(x2122,x2123,x2124,x2125))
% 0.57/1.05 [213]~E(x2131,x2132)+E(f10(x2133,x2131,x2134,x2135),f10(x2133,x2132,x2134,x2135))
% 0.57/1.05 [214]~E(x2141,x2142)+E(f10(x2143,x2144,x2141,x2145),f10(x2143,x2144,x2142,x2145))
% 0.57/1.05 [215]~E(x2151,x2152)+E(f10(x2153,x2154,x2155,x2151),f10(x2153,x2154,x2155,x2152))
% 0.57/1.05 [216]~E(x2161,x2162)+E(f71(x2161,x2163),f71(x2162,x2163))
% 0.57/1.05 [217]~E(x2171,x2172)+E(f71(x2173,x2171),f71(x2173,x2172))
% 0.57/1.05 [218]~E(x2181,x2182)+E(f8(x2181,x2183,x2184,x2185),f8(x2182,x2183,x2184,x2185))
% 0.57/1.05 [219]~E(x2191,x2192)+E(f8(x2193,x2191,x2194,x2195),f8(x2193,x2192,x2194,x2195))
% 0.57/1.05 [220]~E(x2201,x2202)+E(f8(x2203,x2204,x2201,x2205),f8(x2203,x2204,x2202,x2205))
% 0.57/1.05 [221]~E(x2211,x2212)+E(f8(x2213,x2214,x2215,x2211),f8(x2213,x2214,x2215,x2212))
% 0.57/1.05 [222]~E(x2221,x2222)+E(f7(x2221,x2223,x2224,x2225),f7(x2222,x2223,x2224,x2225))
% 0.57/1.05 [223]~E(x2231,x2232)+E(f7(x2233,x2231,x2234,x2235),f7(x2233,x2232,x2234,x2235))
% 0.57/1.05 [224]~E(x2241,x2242)+E(f7(x2243,x2244,x2241,x2245),f7(x2243,x2244,x2242,x2245))
% 0.57/1.05 [225]~E(x2251,x2252)+E(f7(x2253,x2254,x2255,x2251),f7(x2253,x2254,x2255,x2252))
% 0.57/1.05 [226]~E(x2261,x2262)+E(f12(x2261,x2263,x2264,x2265),f12(x2262,x2263,x2264,x2265))
% 0.57/1.05 [227]~E(x2271,x2272)+E(f12(x2273,x2271,x2274,x2275),f12(x2273,x2272,x2274,x2275))
% 0.57/1.05 [228]~E(x2281,x2282)+E(f12(x2283,x2284,x2281,x2285),f12(x2283,x2284,x2282,x2285))
% 0.57/1.06 [229]~E(x2291,x2292)+E(f12(x2293,x2294,x2295,x2291),f12(x2293,x2294,x2295,x2292))
% 0.57/1.06 [230]~E(x2301,x2302)+E(f75(x2301,x2303),f75(x2302,x2303))
% 0.57/1.06 [231]~E(x2311,x2312)+E(f75(x2313,x2311),f75(x2313,x2312))
% 0.57/1.06 [232]~E(x2321,x2322)+E(f76(x2321,x2323),f76(x2322,x2323))
% 0.57/1.06 [233]~E(x2331,x2332)+E(f76(x2333,x2331),f76(x2333,x2332))
% 0.57/1.06 [234]~E(x2341,x2342)+E(f77(x2341,x2343),f77(x2342,x2343))
% 0.57/1.06 [235]~E(x2351,x2352)+E(f77(x2353,x2351),f77(x2353,x2352))
% 0.57/1.06 [236]~E(x2361,x2362)+E(f9(x2361,x2363,x2364,x2365),f9(x2362,x2363,x2364,x2365))
% 0.57/1.06 [237]~E(x2371,x2372)+E(f9(x2373,x2371,x2374,x2375),f9(x2373,x2372,x2374,x2375))
% 0.57/1.06 [238]~E(x2381,x2382)+E(f9(x2383,x2384,x2381,x2385),f9(x2383,x2384,x2382,x2385))
% 0.57/1.06 [239]~E(x2391,x2392)+E(f9(x2393,x2394,x2395,x2391),f9(x2393,x2394,x2395,x2392))
% 0.57/1.06 [240]~E(x2401,x2402)+E(f13(x2401,x2403,x2404,x2405,x2406),f13(x2402,x2403,x2404,x2405,x2406))
% 0.57/1.06 [241]~E(x2411,x2412)+E(f13(x2413,x2411,x2414,x2415,x2416),f13(x2413,x2412,x2414,x2415,x2416))
% 0.57/1.06 [242]~E(x2421,x2422)+E(f13(x2423,x2424,x2421,x2425,x2426),f13(x2423,x2424,x2422,x2425,x2426))
% 0.57/1.06 [243]~E(x2431,x2432)+E(f13(x2433,x2434,x2435,x2431,x2436),f13(x2433,x2434,x2435,x2432,x2436))
% 0.57/1.06 [244]~E(x2441,x2442)+E(f13(x2443,x2444,x2445,x2446,x2441),f13(x2443,x2444,x2445,x2446,x2442))
% 0.57/1.06 [245]~E(x2451,x2452)+E(f17(x2451,x2453,x2454,x2455),f17(x2452,x2453,x2454,x2455))
% 0.57/1.06 [246]~E(x2461,x2462)+E(f17(x2463,x2461,x2464,x2465),f17(x2463,x2462,x2464,x2465))
% 0.57/1.06 [247]~E(x2471,x2472)+E(f17(x2473,x2474,x2471,x2475),f17(x2473,x2474,x2472,x2475))
% 0.57/1.06 [248]~E(x2481,x2482)+E(f17(x2483,x2484,x2485,x2481),f17(x2483,x2484,x2485,x2482))
% 0.57/1.06 [249]~E(x2491,x2492)+E(f16(x2491,x2493,x2494,x2495),f16(x2492,x2493,x2494,x2495))
% 0.57/1.06 [250]~E(x2501,x2502)+E(f16(x2503,x2501,x2504,x2505),f16(x2503,x2502,x2504,x2505))
% 0.57/1.06 [251]~E(x2511,x2512)+E(f16(x2513,x2514,x2511,x2515),f16(x2513,x2514,x2512,x2515))
% 0.57/1.06 [252]~E(x2521,x2522)+E(f16(x2523,x2524,x2525,x2521),f16(x2523,x2524,x2525,x2522))
% 0.57/1.06 [253]~E(x2531,x2532)+E(f15(x2531,x2533,x2534,x2535,x2536),f15(x2532,x2533,x2534,x2535,x2536))
% 0.57/1.06 [254]~E(x2541,x2542)+E(f15(x2543,x2541,x2544,x2545,x2546),f15(x2543,x2542,x2544,x2545,x2546))
% 0.57/1.06 [255]~E(x2551,x2552)+E(f15(x2553,x2554,x2551,x2555,x2556),f15(x2553,x2554,x2552,x2555,x2556))
% 0.57/1.06 [256]~E(x2561,x2562)+E(f15(x2563,x2564,x2565,x2561,x2566),f15(x2563,x2564,x2565,x2562,x2566))
% 0.57/1.06 [257]~E(x2571,x2572)+E(f15(x2573,x2574,x2575,x2576,x2571),f15(x2573,x2574,x2575,x2576,x2572))
% 0.57/1.06 [258]P1(x2582,x2583,x2584)+~E(x2581,x2582)+~P1(x2581,x2583,x2584)
% 0.57/1.06 [259]P1(x2593,x2592,x2594)+~E(x2591,x2592)+~P1(x2593,x2591,x2594)
% 0.57/1.06 [260]P1(x2603,x2604,x2602)+~E(x2601,x2602)+~P1(x2603,x2604,x2601)
% 0.57/1.06 [261]~P2(x2611)+P2(x2612)+~E(x2611,x2612)
% 0.57/1.06 [262]~P3(x2621)+P3(x2622)+~E(x2621,x2622)
% 0.57/1.06 [263]~P4(x2631)+P4(x2632)+~E(x2631,x2632)
% 0.57/1.06 [264]P7(x2642,x2643,x2644,x2645)+~E(x2641,x2642)+~P7(x2641,x2643,x2644,x2645)
% 0.57/1.06 [265]P7(x2653,x2652,x2654,x2655)+~E(x2651,x2652)+~P7(x2653,x2651,x2654,x2655)
% 0.57/1.06 [266]P7(x2663,x2664,x2662,x2665)+~E(x2661,x2662)+~P7(x2663,x2664,x2661,x2665)
% 0.57/1.06 [267]P7(x2673,x2674,x2675,x2672)+~E(x2671,x2672)+~P7(x2673,x2674,x2675,x2671)
% 0.57/1.06 [268]P8(x2682,x2683,x2684,x2685)+~E(x2681,x2682)+~P8(x2681,x2683,x2684,x2685)
% 0.57/1.06 [269]P8(x2693,x2692,x2694,x2695)+~E(x2691,x2692)+~P8(x2693,x2691,x2694,x2695)
% 0.57/1.06 [270]P8(x2703,x2704,x2702,x2705)+~E(x2701,x2702)+~P8(x2703,x2704,x2701,x2705)
% 0.57/1.06 [271]P8(x2713,x2714,x2715,x2712)+~E(x2711,x2712)+~P8(x2713,x2714,x2715,x2711)
% 0.57/1.06 [272]P9(x2722,x2723)+~E(x2721,x2722)+~P9(x2721,x2723)
% 0.57/1.06 [273]P9(x2733,x2732)+~E(x2731,x2732)+~P9(x2733,x2731)
% 0.57/1.06 [274]P5(x2742,x2743)+~E(x2741,x2742)+~P5(x2741,x2743)
% 0.57/1.06 [275]P5(x2753,x2752)+~E(x2751,x2752)+~P5(x2753,x2751)
% 0.57/1.06 [276]P6(x2762,x2763)+~E(x2761,x2762)+~P6(x2761,x2763)
% 0.57/1.06 [277]P6(x2773,x2772)+~E(x2771,x2772)+~P6(x2773,x2771)
% 0.57/1.06
% 0.57/1.06 %-------------------------------------------
% 0.57/1.06 cnf(707,plain,
% 0.57/1.06 (P2(f31(x7071,x7072,x7073))),
% 0.57/1.06 inference(equality_inference,[],[319])).
% 0.57/1.06 cnf(756,plain,
% 0.57/1.06 ($false),
% 0.57/1.06 inference(scs_inference,[],[285,707]),
% 0.57/1.06 ['proof']).
% 0.57/1.06 % SZS output end Proof
% 0.57/1.06 % Total time :0.130000s
%------------------------------------------------------------------------------