%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL644+1.020 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 11:21:17 AM UTC 2026
% Result : Theorem 0.62s 0.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL644+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.35 % Computer : n019.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 5 09:55:23 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.24/0.47 start to proof:theBenchmark.p
% 0.62/0.62 % Version : CSI_E---1.1
% 0.62/0.62 % Problem : theBenchmark.p
% 0.62/0.62 % Proof found!
% 0.62/0.62 % SZS status Theorem for theBenchmark.p
% 0.62/0.62 % SZS output start Proof
% 0.62/0.62 fof(main, conjecture, ~(?[X1]:(~((~((![X2]:((~(r1(X1,X2))|~((p21(X2)&![X1]:((~(r1(X2,X1))|p21(X1)))))|p20(X2)))|![X2]:((~(r1(X1,X2))|p21(X2)|~(((p20(X2)&![X1]:((~(r1(X2,X1))|p20(X1))))&p20(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p21(X1)&![X2]:((~(r1(X1,X2))|p21(X2)))))|p20(X1)))|p21(X2)|~(((p20(X2)&![X1]:((~(r1(X2,X1))|p20(X1))))&p20(X2)))))&![X2]:((~(r1(X1,X2))|~((p21(X2)&![X1]:((~(r1(X2,X1))|p21(X1)))))|p20(X2)|![X1]:((~(r1(X2,X1))|p21(X1)|~(((p20(X1)&![X2]:((~(r1(X1,X2))|p20(X2))))&p20(X1))))))))&![X2]:((~(r1(X1,X2))|~((p21(X2)&![X1]:((~(r1(X2,X1))|p21(X1)))))|p20(X2)|p21(X2)|~(((p20(X2)&![X1]:((~(r1(X2,X1))|p20(X1))))&p20(X2)))))))))|~((![X2]:((~(r1(X1,X2))|~((p20(X2)&![X1]:((~(r1(X2,X1))|p20(X1)))))|p19(X2)))|![X2]:((~(r1(X1,X2))|p20(X2)|~(((p19(X2)&![X1]:((~(r1(X2,X1))|p19(X1))))&p19(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p20(X1)&![X2]:((~(r1(X1,X2))|p20(X2)))))|p19(X1)))|p20(X2)|~(((p19(X2)&![X1]:((~(r1(X2,X1))|p19(X1))))&p19(X2)))))&![X2]:((~(r1(X1,X2))|~((p20(X2)&![X1]:((~(r1(X2,X1))|p20(X1)))))|p19(X2)|![X1]:((~(r1(X2,X1))|p20(X1)|~(((p19(X1)&![X2]:((~(r1(X1,X2))|p19(X2))))&p19(X1))))))))&![X2]:((~(r1(X1,X2))|~((p20(X2)&![X1]:((~(r1(X2,X1))|p20(X1)))))|p19(X2)|p20(X2)|~(((p19(X2)&![X1]:((~(r1(X2,X1))|p19(X1))))&p19(X2)))))))))|~((![X2]:((~(r1(X1,X2))|~((p19(X2)&![X1]:((~(r1(X2,X1))|p19(X1)))))|p18(X2)))|![X2]:((~(r1(X1,X2))|p19(X2)|~(((p18(X2)&![X1]:((~(r1(X2,X1))|p18(X1))))&p18(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p19(X1)&![X2]:((~(r1(X1,X2))|p19(X2)))))|p18(X1)))|p19(X2)|~(((p18(X2)&![X1]:((~(r1(X2,X1))|p18(X1))))&p18(X2)))))&![X2]:((~(r1(X1,X2))|~((p19(X2)&![X1]:((~(r1(X2,X1))|p19(X1)))))|p18(X2)|![X1]:((~(r1(X2,X1))|p19(X1)|~(((p18(X1)&![X2]:((~(r1(X1,X2))|p18(X2))))&p18(X1))))))))&![X2]:((~(r1(X1,X2))|~((p19(X2)&![X1]:((~(r1(X2,X1))|p19(X1)))))|p18(X2)|p19(X2)|~(((p18(X2)&![X1]:((~(r1(X2,X1))|p18(X1))))&p18(X2)))))))))|~((![X2]:((~(r1(X1,X2))|~((p18(X2)&![X1]:((~(r1(X2,X1))|p18(X1)))))|p17(X2)))|![X2]:((~(r1(X1,X2))|p18(X2)|~(((p17(X2)&![X1]:((~(r1(X2,X1))|p17(X1))))&p17(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p18(X1)&![X2]:((~(r1(X1,X2))|p18(X2)))))|p17(X1)))|p18(X2)|~(((p17(X2)&![X1]:((~(r1(X2,X1))|p17(X1))))&p17(X2)))))&![X2]:((~(r1(X1,X2))|~((p18(X2)&![X1]:((~(r1(X2,X1))|p18(X1)))))|p17(X2)|![X1]:((~(r1(X2,X1))|p18(X1)|~(((p17(X1)&![X2]:((~(r1(X1,X2))|p17(X2))))&p17(X1))))))))&![X2]:((~(r1(X1,X2))|~((p18(X2)&![X1]:((~(r1(X2,X1))|p18(X1)))))|p17(X2)|p18(X2)|~(((p17(X2)&![X1]:((~(r1(X2,X1))|p17(X1))))&p17(X2)))))))))|~((![X2]:((~(r1(X1,X2))|~((p17(X2)&![X1]:((~(r1(X2,X1))|p17(X1)))))|p16(X2)))|![X2]:((~(r1(X1,X2))|p17(X2)|~(((p16(X2)&![X1]:((~(r1(X2,X1))|p16(X1))))&p16(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p17(X1)&![X2]:((~(r1(X1,X2))|p17(X2)))))|p16(X1)))|p17(X2)|~(((p16(X2)&![X1]:((~(r1(X2,X1))|p16(X1))))&p16(X2)))))&![X2]:((~(r1(X1,X2))|~((p17(X2)&![X1]:((~(r1(X2,X1))|p17(X1)))))|p16(X2)|![X1]:((~(r1(X2,X1))|p17(X1)|~(((p16(X1)&![X2]:((~(r1(X1,X2))|p16(X2))))&p16(X1))))))))&![X2]:((~(r1(X1,X2))|~((p17(X2)&![X1]:((~(r1(X2,X1))|p17(X1)))))|p16(X2)|p17(X2)|~(((p16(X2)&![X1]:((~(r1(X2,X1))|p16(X1))))&p16(X2)))))))))|~((![X2]:((~(r1(X1,X2))|~((p16(X2)&![X1]:((~(r1(X2,X1))|p16(X1)))))|p15(X2)))|![X2]:((~(r1(X1,X2))|p16(X2)|~(((p15(X2)&![X1]:((~(r1(X2,X1))|p15(X1))))&p15(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p16(X1)&![X2]:((~(r1(X1,X2))|p16(X2)))))|p15(X1)))|p16(X2)|~(((p15(X2)&![X1]:((~(r1(X2,X1))|p15(X1))))&p15(X2)))))&![X2]:((~(r1(X1,X2))|~((p16(X2)&![X1]:((~(r1(X2,X1))|p16(X1)))))|p15(X2)|![X1]:((~(r1(X2,X1))|p16(X1)|~(((p15(X1)&![X2]:((~(r1(X1,X2))|p15(X2))))&p15(X1))))))))&![X2]:((~(r1(X1,X2))|~((p16(X2)&![X1]:((~(r1(X2,X1))|p16(X1)))))|p15(X2)|p16(X2)|~(((p15(X2)&![X1]:((~(r1(X2,X1))|p15(X1))))&p15(X2)))))))))|~((![X2]:((~(r1(X1,X2))|~((p15(X2)&![X1]:((~(r1(X2,X1))|p15(X1)))))|p14(X2)))|![X2]:((~(r1(X1,X2))|p15(X2)|~(((p14(X2)&![X1]:((~(r1(X2,X1))|p14(X1))))&p14(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p15(X1)&![X2]:((~(r1(X1,X2))|p15(X2)))))|p14(X1)))|p15(X2)|~(((p14(X2)&![X1]:((~(r1(X2,X1))|p14(X1))))&p14(X2)))))&![X2]:((~(r1(X1,X2))|~((p15(X2)&![X1]:((~(r1(X2,X1))|p15(X1)))))|p14(X2)|![X1]:((~(r1(X2,X1))|p15(X1)|~(((p14(X1)&![X2]:((~(r1(X1,X2))|p14(X2))))&p14(X1))))))))&![X2]:((~(r1(X1,X2))|~((p15(X2)&![X1]:((~(r1(X2,X1))|p15(X1)))))|p14(X2)|p15(X2)|~(((p14(X2)&![X1]:((~(r1(X2,X1))|p14(X1))))&p14(X2)))))))))|~((![X2]:((~(r1(X1,X2))|~((p14(X2)&![X1]:((~(r1(X2,X1))|p14(X1)))))|p13(X2)))|![X2]:((~(r1(X1,X2))|p14(X2)|~(((p13(X2)&![X1]:((~(r1(X2,X1))|p13(X1))))&p13(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p14(X1)&![X2]:((~(r1(X1,X2))|p14(X2)))))|p13(X1)))|p14(X2)|~(((p13(X2)&![X1]:((~(r1(X2,X1))|p13(X1))))&p13(X2)))))&![X2]:((~(r1(X1,X2))|~((p14(X2)&![X1]:((~(r1(X2,X1))|p14(X1)))))|p13(X2)|![X1]:((~(r1(X2,X1))|p14(X1)|~(((p13(X1)&![X2]:((~(r1(X1,X2))|p13(X2))))&p13(X1))))))))&![X2]:((~(r1(X1,X2))|~((p14(X2)&![X1]:((~(r1(X2,X1))|p14(X1)))))|p13(X2)|p14(X2)|~(((p13(X2)&![X1]:((~(r1(X2,X1))|p13(X1))))&p13(X2)))))))))|~((![X2]:((~(r1(X1,X2))|~((p13(X2)&![X1]:((~(r1(X2,X1))|p13(X1)))))|p12(X2)))|![X2]:((~(r1(X1,X2))|p13(X2)|~(((p12(X2)&![X1]:((~(r1(X2,X1))|p12(X1))))&p12(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p13(X1)&![X2]:((~(r1(X1,X2))|p13(X2)))))|p12(X1)))|p13(X2)|~(((p12(X2)&![X1]:((~(r1(X2,X1))|p12(X1))))&p12(X2)))))&![X2]:((~(r1(X1,X2))|~((p13(X2)&![X1]:((~(r1(X2,X1))|p13(X1)))))|p12(X2)|![X1]:((~(r1(X2,X1))|p13(X1)|~(((p12(X1)&![X2]:((~(r1(X1,X2))|p12(X2))))&p12(X1))))))))&![X2]:((~(r1(X1,X2))|~((p13(X2)&![X1]:((~(r1(X2,X1))|p13(X1)))))|p12(X2)|p13(X2)|~(((p12(X2)&![X1]:((~(r1(X2,X1))|p12(X1))))&p12(X2)))))))))|~((![X2]:((~(r1(X1,X2))|~((p12(X2)&![X1]:((~(r1(X2,X1))|p12(X1)))))|p11(X2)))|![X2]:((~(r1(X1,X2))|p12(X2)|~(((p11(X2)&![X1]:((~(r1(X2,X1))|p11(X1))))&p11(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p12(X1)&![X2]:((~(r1(X1,X2))|p12(X2)))))|p11(X1)))|p12(X2)|~(((p11(X2)&![X1]:((~(r1(X2,X1))|p11(X1))))&p11(X2)))))&![X2]:((~(r1(X1,X2))|~((p12(X2)&![X1]:((~(r1(X2,X1))|p12(X1)))))|p11(X2)|![X1]:((~(r1(X2,X1))|p12(X1)|~(((p11(X1)&![X2]:((~(r1(X1,X2))|p11(X2))))&p11(X1))))))))&![X2]:((~(r1(X1,X2))|~((p12(X2)&![X1]:((~(r1(X2,X1))|p12(X1)))))|p11(X2)|p12(X2)|~(((p11(X2)&![X1]:((~(r1(X2,X1))|p11(X1))))&p11(X2)))))))))|~((![X2]:((~(r1(X1,X2))|~((p11(X2)&![X1]:((~(r1(X2,X1))|p11(X1)))))|p10(X2)))|![X2]:((~(r1(X1,X2))|p11(X2)|~(((p10(X2)&![X1]:((~(r1(X2,X1))|p10(X1))))&p10(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p11(X1)&![X2]:((~(r1(X1,X2))|p11(X2)))))|p10(X1)))|p11(X2)|~(((p10(X2)&![X1]:((~(r1(X2,X1))|p10(X1))))&p10(X2)))))&![X2]:((~(r1(X1,X2))|~((p11(X2)&![X1]:((~(r1(X2,X1))|p11(X1)))))|p10(X2)|![X1]:((~(r1(X2,X1))|p11(X1)|~(((p10(X1)&![X2]:((~(r1(X1,X2))|p10(X2))))&p10(X1))))))))&![X2]:((~(r1(X1,X2))|~((p11(X2)&![X1]:((~(r1(X2,X1))|p11(X1)))))|p10(X2)|p11(X2)|~(((p10(X2)&![X1]:((~(r1(X2,X1))|p10(X1))))&p10(X2)))))))))|~((![X2]:((~(r1(X1,X2))|~((p10(X2)&![X1]:((~(r1(X2,X1))|p10(X1)))))|p9(X2)))|![X2]:((~(r1(X1,X2))|p10(X2)|~(((p9(X2)&![X1]:((~(r1(X2,X1))|p9(X1))))&p9(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p10(X1)&![X2]:((~(r1(X1,X2))|p10(X2)))))|p9(X1)))|p10(X2)|~(((p9(X2)&![X1]:((~(r1(X2,X1))|p9(X1))))&p9(X2)))))&![X2]:((~(r1(X1,X2))|~((p10(X2)&![X1]:((~(r1(X2,X1))|p10(X1)))))|p9(X2)|![X1]:((~(r1(X2,X1))|p10(X1)|~(((p9(X1)&![X2]:((~(r1(X1,X2))|p9(X2))))&p9(X1))))))))&![X2]:((~(r1(X1,X2))|~((p10(X2)&![X1]:((~(r1(X2,X1))|p10(X1)))))|p9(X2)|p10(X2)|~(((p9(X2)&![X1]:((~(r1(X2,X1))|p9(X1))))&p9(X2)))))))))|~((![X2]:((~(r1(X1,X2))|~((p9(X2)&![X1]:((~(r1(X2,X1))|p9(X1)))))|p8(X2)))|![X2]:((~(r1(X1,X2))|p9(X2)|~(((p8(X2)&![X1]:((~(r1(X2,X1))|p8(X1))))&p8(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p9(X1)&![X2]:((~(r1(X1,X2))|p9(X2)))))|p8(X1)))|p9(X2)|~(((p8(X2)&![X1]:((~(r1(X2,X1))|p8(X1))))&p8(X2)))))&![X2]:((~(r1(X1,X2))|~((p9(X2)&![X1]:((~(r1(X2,X1))|p9(X1)))))|p8(X2)|![X1]:((~(r1(X2,X1))|p9(X1)|~(((p8(X1)&![X2]:((~(r1(X1,X2))|p8(X2))))&p8(X1))))))))&![X2]:((~(r1(X1,X2))|~((p9(X2)&![X1]:((~(r1(X2,X1))|p9(X1)))))|p8(X2)|p9(X2)|~(((p8(X2)&![X1]:((~(r1(X2,X1))|p8(X1))))&p8(X2)))))))))|~((![X2]:((~(r1(X1,X2))|~((p8(X2)&![X1]:((~(r1(X2,X1))|p8(X1)))))|p7(X2)))|![X2]:((~(r1(X1,X2))|p8(X2)|~(((p7(X2)&![X1]:((~(r1(X2,X1))|p7(X1))))&p7(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p8(X1)&![X2]:((~(r1(X1,X2))|p8(X2)))))|p7(X1)))|p8(X2)|~(((p7(X2)&![X1]:((~(r1(X2,X1))|p7(X1))))&p7(X2)))))&![X2]:((~(r1(X1,X2))|~((p8(X2)&![X1]:((~(r1(X2,X1))|p8(X1)))))|p7(X2)|![X1]:((~(r1(X2,X1))|p8(X1)|~(((p7(X1)&![X2]:((~(r1(X1,X2))|p7(X2))))&p7(X1))))))))&![X2]:((~(r1(X1,X2))|~((p8(X2)&![X1]:((~(r1(X2,X1))|p8(X1)))))|p7(X2)|p8(X2)|~(((p7(X2)&![X1]:((~(r1(X2,X1))|p7(X1))))&p7(X2)))))))))|![X2]:((~(r1(X1,X2))|p20(X2)|~((![X1]:((~(r1(X2,X1))|p20(X1)))&p20(X2)))))|![X2]:((~(r1(X1,X2))|p20(X2)|~((![X1]:((~(r1(X2,X1))|p20(X1)))&p20(X2)))))|~((![X2]:((~(r1(X1,X2))|~((p7(X2)&![X1]:((~(r1(X2,X1))|p7(X1)))))|p6(X2)))|![X2]:((~(r1(X1,X2))|p7(X2)|~(((p6(X2)&![X1]:((~(r1(X2,X1))|p6(X1))))&p6(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p7(X1)&![X2]:((~(r1(X1,X2))|p7(X2)))))|p6(X1)))|p7(X2)|~(((p6(X2)&![X1]:((~(r1(X2,X1))|p6(X1))))&p6(X2)))))&![X2]:((~(r1(X1,X2))|~((p7(X2)&![X1]:((~(r1(X2,X1))|p7(X1)))))|p6(X2)|![X1]:((~(r1(X2,X1))|p7(X1)|~(((p6(X1)&![X2]:((~(r1(X1,X2))|p6(X2))))&p6(X1))))))))&![X2]:((~(r1(X1,X2))|~((p7(X2)&![X1]:((~(r1(X2,X1))|p7(X1)))))|p6(X2)|p7(X2)|~(((p6(X2)&![X1]:((~(r1(X2,X1))|p6(X1))))&p6(X2)))))))))|~((![X2]:((~(r1(X1,X2))|~((p6(X2)&![X1]:((~(r1(X2,X1))|p6(X1)))))|p5(X2)))|![X2]:((~(r1(X1,X2))|p6(X2)|~(((p5(X2)&![X1]:((~(r1(X2,X1))|p5(X1))))&p5(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p6(X1)&![X2]:((~(r1(X1,X2))|p6(X2)))))|p5(X1)))|p6(X2)|~(((p5(X2)&![X1]:((~(r1(X2,X1))|p5(X1))))&p5(X2)))))&![X2]:((~(r1(X1,X2))|~((p6(X2)&![X1]:((~(r1(X2,X1))|p6(X1)))))|p5(X2)|![X1]:((~(r1(X2,X1))|p6(X1)|~(((p5(X1)&![X2]:((~(r1(X1,X2))|p5(X2))))&p5(X1))))))))&![X2]:((~(r1(X1,X2))|~((p6(X2)&![X1]:((~(r1(X2,X1))|p6(X1)))))|p5(X2)|p6(X2)|~(((p5(X2)&![X1]:((~(r1(X2,X1))|p5(X1))))&p5(X2)))))))))|~((![X2]:((~(r1(X1,X2))|~((p5(X2)&![X1]:((~(r1(X2,X1))|p5(X1)))))|p4(X2)))|![X2]:((~(r1(X1,X2))|p5(X2)|~(((p4(X2)&![X1]:((~(r1(X2,X1))|p4(X1))))&p4(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p5(X1)&![X2]:((~(r1(X1,X2))|p5(X2)))))|p4(X1)))|p5(X2)|~(((p4(X2)&![X1]:((~(r1(X2,X1))|p4(X1))))&p4(X2)))))&![X2]:((~(r1(X1,X2))|~((p5(X2)&![X1]:((~(r1(X2,X1))|p5(X1)))))|p4(X2)|![X1]:((~(r1(X2,X1))|p5(X1)|~(((p4(X1)&![X2]:((~(r1(X1,X2))|p4(X2))))&p4(X1))))))))&![X2]:((~(r1(X1,X2))|~((p5(X2)&![X1]:((~(r1(X2,X1))|p5(X1)))))|p4(X2)|p5(X2)|~(((p4(X2)&![X1]:((~(r1(X2,X1))|p4(X1))))&p4(X2)))))))))|~((![X2]:((~(r1(X1,X2))|~((p4(X2)&![X1]:((~(r1(X2,X1))|p4(X1)))))|p3(X2)))|![X2]:((~(r1(X1,X2))|p4(X2)|~(((p3(X2)&![X1]:((~(r1(X2,X1))|p3(X1))))&p3(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p4(X1)&![X2]:((~(r1(X1,X2))|p4(X2)))))|p3(X1)))|p4(X2)|~(((p3(X2)&![X1]:((~(r1(X2,X1))|p3(X1))))&p3(X2)))))&![X2]:((~(r1(X1,X2))|~((p4(X2)&![X1]:((~(r1(X2,X1))|p4(X1)))))|p3(X2)|![X1]:((~(r1(X2,X1))|p4(X1)|~(((p3(X1)&![X2]:((~(r1(X1,X2))|p3(X2))))&p3(X1))))))))&![X2]:((~(r1(X1,X2))|~((p4(X2)&![X1]:((~(r1(X2,X1))|p4(X1)))))|p3(X2)|p4(X2)|~(((p3(X2)&![X1]:((~(r1(X2,X1))|p3(X1))))&p3(X2)))))))))|~((![X2]:((~(r1(X1,X2))|~((p3(X2)&![X1]:((~(r1(X2,X1))|p3(X1)))))|p2(X2)))|![X2]:((~(r1(X1,X2))|p3(X2)|~(((p2(X2)&![X1]:((~(r1(X2,X1))|p2(X1))))&p2(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p3(X1)&![X2]:((~(r1(X1,X2))|p3(X2)))))|p2(X1)))|p3(X2)|~(((p2(X2)&![X1]:((~(r1(X2,X1))|p2(X1))))&p2(X2)))))&![X2]:((~(r1(X1,X2))|~((p3(X2)&![X1]:((~(r1(X2,X1))|p3(X1)))))|p2(X2)|![X1]:((~(r1(X2,X1))|p3(X1)|~(((p2(X1)&![X2]:((~(r1(X1,X2))|p2(X2))))&p2(X1))))))))&![X2]:((~(r1(X1,X2))|~((p3(X2)&![X1]:((~(r1(X2,X1))|p3(X1)))))|p2(X2)|p3(X2)|~(((p2(X2)&![X1]:((~(r1(X2,X1))|p2(X1))))&p2(X2)))))))))|~((![X2]:((~(r1(X1,X2))|~((p2(X2)&![X1]:((~(r1(X2,X1))|p2(X1)))))|p1(X2)))|![X2]:((~(r1(X1,X2))|p2(X2)|~(((p1(X2)&![X1]:((~(r1(X2,X1))|p1(X1))))&p1(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p2(X1)&![X2]:((~(r1(X1,X2))|p2(X2)))))|p1(X1)))|p2(X2)|~(((p1(X2)&![X1]:((~(r1(X2,X1))|p1(X1))))&p1(X2)))))&![X2]:((~(r1(X1,X2))|~((p2(X2)&![X1]:((~(r1(X2,X1))|p2(X1)))))|p1(X2)|![X1]:((~(r1(X2,X1))|p2(X1)|~(((p1(X1)&![X2]:((~(r1(X1,X2))|p1(X2))))&p1(X1))))))))&![X2]:((~(r1(X1,X2))|~((p2(X2)&![X1]:((~(r1(X2,X1))|p2(X1)))))|p1(X2)|p2(X2)|~(((p1(X2)&![X1]:((~(r1(X2,X1))|p1(X1))))&p1(X2))))))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', main)).
% 0.62/0.62 fof(c_0_1, plain, ![X1]:((epred1_1(X1)<=>(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((p21(X1)&![X2]:((~r1(X1,X2)|p21(X2)))))|p20(X1)))|p21(X2)|~(((p20(X2)&![X1]:((~r1(X2,X1)|p20(X1))))&p20(X2)))))&![X2]:((~r1(X1,X2)|~((p21(X2)&![X1]:((~r1(X2,X1)|p21(X1)))))|p20(X2)|![X1]:((~r1(X2,X1)|p21(X1)|~(((p20(X1)&![X2]:((~r1(X1,X2)|p20(X2))))&p20(X1)))))))))), introduced(definition)).
% 0.62/0.62 fof(c_0_2, plain, ![X1]:((epred2_1(X1)<=>(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((p20(X1)&![X2]:((~r1(X1,X2)|p20(X2)))))|p19(X1)))|p20(X2)|~(((p19(X2)&![X1]:((~r1(X2,X1)|p19(X1))))&p19(X2)))))&![X2]:((~r1(X1,X2)|~((p20(X2)&![X1]:((~r1(X2,X1)|p20(X1)))))|p19(X2)|![X1]:((~r1(X2,X1)|p20(X1)|~(((p19(X1)&![X2]:((~r1(X1,X2)|p19(X2))))&p19(X1)))))))))), introduced(definition)).
% 0.62/0.62 fof(c_0_3, plain, ![X1]:((epred3_1(X1)<=>(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((p19(X1)&![X2]:((~r1(X1,X2)|p19(X2)))))|p18(X1)))|p19(X2)|~(((p18(X2)&![X1]:((~r1(X2,X1)|p18(X1))))&p18(X2)))))&![X2]:((~r1(X1,X2)|~((p19(X2)&![X1]:((~r1(X2,X1)|p19(X1)))))|p18(X2)|![X1]:((~r1(X2,X1)|p19(X1)|~(((p18(X1)&![X2]:((~r1(X1,X2)|p18(X2))))&p18(X1)))))))))), introduced(definition)).
% 0.62/0.62 fof(c_0_4, plain, ![X1]:((epred4_1(X1)<=>(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((p18(X1)&![X2]:((~r1(X1,X2)|p18(X2)))))|p17(X1)))|p18(X2)|~(((p17(X2)&![X1]:((~r1(X2,X1)|p17(X1))))&p17(X2)))))&![X2]:((~r1(X1,X2)|~((p18(X2)&![X1]:((~r1(X2,X1)|p18(X1)))))|p17(X2)|![X1]:((~r1(X2,X1)|p18(X1)|~(((p17(X1)&![X2]:((~r1(X1,X2)|p17(X2))))&p17(X1)))))))))), introduced(definition)).
% 0.62/0.62 fof(c_0_5, plain, ![X1]:((epred5_1(X1)<=>(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((p17(X1)&![X2]:((~r1(X1,X2)|p17(X2)))))|p16(X1)))|p17(X2)|~(((p16(X2)&![X1]:((~r1(X2,X1)|p16(X1))))&p16(X2)))))&![X2]:((~r1(X1,X2)|~((p17(X2)&![X1]:((~r1(X2,X1)|p17(X1)))))|p16(X2)|![X1]:((~r1(X2,X1)|p17(X1)|~(((p16(X1)&![X2]:((~r1(X1,X2)|p16(X2))))&p16(X1)))))))))), introduced(definition)).
% 0.62/0.62 fof(c_0_6, plain, ![X1]:((epred6_1(X1)<=>(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((p16(X1)&![X2]:((~r1(X1,X2)|p16(X2)))))|p15(X1)))|p16(X2)|~(((p15(X2)&![X1]:((~r1(X2,X1)|p15(X1))))&p15(X2)))))&![X2]:((~r1(X1,X2)|~((p16(X2)&![X1]:((~r1(X2,X1)|p16(X1)))))|p15(X2)|![X1]:((~r1(X2,X1)|p16(X1)|~(((p15(X1)&![X2]:((~r1(X1,X2)|p15(X2))))&p15(X1)))))))))), introduced(definition)).
% 0.62/0.62 fof(c_0_7, plain, ![X1]:((epred7_1(X1)<=>(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((p15(X1)&![X2]:((~r1(X1,X2)|p15(X2)))))|p14(X1)))|p15(X2)|~(((p14(X2)&![X1]:((~r1(X2,X1)|p14(X1))))&p14(X2)))))&![X2]:((~r1(X1,X2)|~((p15(X2)&![X1]:((~r1(X2,X1)|p15(X1)))))|p14(X2)|![X1]:((~r1(X2,X1)|p15(X1)|~(((p14(X1)&![X2]:((~r1(X1,X2)|p14(X2))))&p14(X1)))))))))), introduced(definition)).
% 0.62/0.62 fof(c_0_8, plain, ![X1]:((epred8_1(X1)<=>(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((p14(X1)&![X2]:((~r1(X1,X2)|p14(X2)))))|p13(X1)))|p14(X2)|~(((p13(X2)&![X1]:((~r1(X2,X1)|p13(X1))))&p13(X2)))))&![X2]:((~r1(X1,X2)|~((p14(X2)&![X1]:((~r1(X2,X1)|p14(X1)))))|p13(X2)|![X1]:((~r1(X2,X1)|p14(X1)|~(((p13(X1)&![X2]:((~r1(X1,X2)|p13(X2))))&p13(X1)))))))))), introduced(definition)).
% 0.62/0.62 fof(c_0_9, plain, ![X1]:((epred9_1(X1)<=>(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((p13(X1)&![X2]:((~r1(X1,X2)|p13(X2)))))|p12(X1)))|p13(X2)|~(((p12(X2)&![X1]:((~r1(X2,X1)|p12(X1))))&p12(X2)))))&![X2]:((~r1(X1,X2)|~((p13(X2)&![X1]:((~r1(X2,X1)|p13(X1)))))|p12(X2)|![X1]:((~r1(X2,X1)|p13(X1)|~(((p12(X1)&![X2]:((~r1(X1,X2)|p12(X2))))&p12(X1)))))))))), introduced(definition)).
% 0.62/0.62 fof(c_0_10, plain, ![X1]:((epred10_1(X1)<=>(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((p12(X1)&![X2]:((~r1(X1,X2)|p12(X2)))))|p11(X1)))|p12(X2)|~(((p11(X2)&![X1]:((~r1(X2,X1)|p11(X1))))&p11(X2)))))&![X2]:((~r1(X1,X2)|~((p12(X2)&![X1]:((~r1(X2,X1)|p12(X1)))))|p11(X2)|![X1]:((~r1(X2,X1)|p12(X1)|~(((p11(X1)&![X2]:((~r1(X1,X2)|p11(X2))))&p11(X1)))))))))), introduced(definition)).
% 0.62/0.62 fof(c_0_11, plain, ![X1]:((epred11_1(X1)<=>(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((p11(X1)&![X2]:((~r1(X1,X2)|p11(X2)))))|p10(X1)))|p11(X2)|~(((p10(X2)&![X1]:((~r1(X2,X1)|p10(X1))))&p10(X2)))))&![X2]:((~r1(X1,X2)|~((p11(X2)&![X1]:((~r1(X2,X1)|p11(X1)))))|p10(X2)|![X1]:((~r1(X2,X1)|p11(X1)|~(((p10(X1)&![X2]:((~r1(X1,X2)|p10(X2))))&p10(X1)))))))))), introduced(definition)).
% 0.62/0.62 fof(c_0_12, plain, ![X1]:((epred12_1(X1)<=>(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((p10(X1)&![X2]:((~r1(X1,X2)|p10(X2)))))|p9(X1)))|p10(X2)|~(((p9(X2)&![X1]:((~r1(X2,X1)|p9(X1))))&p9(X2)))))&![X2]:((~r1(X1,X2)|~((p10(X2)&![X1]:((~r1(X2,X1)|p10(X1)))))|p9(X2)|![X1]:((~r1(X2,X1)|p10(X1)|~(((p9(X1)&![X2]:((~r1(X1,X2)|p9(X2))))&p9(X1)))))))))), introduced(definition)).
% 0.62/0.62 fof(c_0_13, plain, ![X1]:((epred13_1(X1)<=>(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((p9(X1)&![X2]:((~r1(X1,X2)|p9(X2)))))|p8(X1)))|p9(X2)|~(((p8(X2)&![X1]:((~r1(X2,X1)|p8(X1))))&p8(X2)))))&![X2]:((~r1(X1,X2)|~((p9(X2)&![X1]:((~r1(X2,X1)|p9(X1)))))|p8(X2)|![X1]:((~r1(X2,X1)|p9(X1)|~(((p8(X1)&![X2]:((~r1(X1,X2)|p8(X2))))&p8(X1)))))))))), introduced(definition)).
% 0.62/0.62 fof(c_0_14, plain, ![X1]:((epred14_1(X1)<=>(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((p8(X1)&![X2]:((~r1(X1,X2)|p8(X2)))))|p7(X1)))|p8(X2)|~(((p7(X2)&![X1]:((~r1(X2,X1)|p7(X1))))&p7(X2)))))&![X2]:((~r1(X1,X2)|~((p8(X2)&![X1]:((~r1(X2,X1)|p8(X1)))))|p7(X2)|![X1]:((~r1(X2,X1)|p8(X1)|~(((p7(X1)&![X2]:((~r1(X1,X2)|p7(X2))))&p7(X1)))))))))), introduced(definition)).
% 0.62/0.62 fof(c_0_15, plain, ![X1]:((epred15_1(X1)<=>(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((p7(X1)&![X2]:((~r1(X1,X2)|p7(X2)))))|p6(X1)))|p7(X2)|~(((p6(X2)&![X1]:((~r1(X2,X1)|p6(X1))))&p6(X2)))))&![X2]:((~r1(X1,X2)|~((p7(X2)&![X1]:((~r1(X2,X1)|p7(X1)))))|p6(X2)|![X1]:((~r1(X2,X1)|p7(X1)|~(((p6(X1)&![X2]:((~r1(X1,X2)|p6(X2))))&p6(X1)))))))))), introduced(definition)).
% 0.62/0.62 fof(c_0_16, plain, ![X1]:((epred16_1(X1)<=>(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((p6(X1)&![X2]:((~r1(X1,X2)|p6(X2)))))|p5(X1)))|p6(X2)|~(((p5(X2)&![X1]:((~r1(X2,X1)|p5(X1))))&p5(X2)))))&![X2]:((~r1(X1,X2)|~((p6(X2)&![X1]:((~r1(X2,X1)|p6(X1)))))|p5(X2)|![X1]:((~r1(X2,X1)|p6(X1)|~(((p5(X1)&![X2]:((~r1(X1,X2)|p5(X2))))&p5(X1)))))))))), introduced(definition)).
% 0.62/0.62 fof(c_0_17, plain, ![X1]:((epred17_1(X1)<=>(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((p5(X1)&![X2]:((~r1(X1,X2)|p5(X2)))))|p4(X1)))|p5(X2)|~(((p4(X2)&![X1]:((~r1(X2,X1)|p4(X1))))&p4(X2)))))&![X2]:((~r1(X1,X2)|~((p5(X2)&![X1]:((~r1(X2,X1)|p5(X1)))))|p4(X2)|![X1]:((~r1(X2,X1)|p5(X1)|~(((p4(X1)&![X2]:((~r1(X1,X2)|p4(X2))))&p4(X1)))))))))), introduced(definition)).
% 0.62/0.62 fof(c_0_18, plain, ![X1]:((epred18_1(X1)<=>(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((p4(X1)&![X2]:((~r1(X1,X2)|p4(X2)))))|p3(X1)))|p4(X2)|~(((p3(X2)&![X1]:((~r1(X2,X1)|p3(X1))))&p3(X2)))))&![X2]:((~r1(X1,X2)|~((p4(X2)&![X1]:((~r1(X2,X1)|p4(X1)))))|p3(X2)|![X1]:((~r1(X2,X1)|p4(X1)|~(((p3(X1)&![X2]:((~r1(X1,X2)|p3(X2))))&p3(X1)))))))))), introduced(definition)).
% 0.62/0.62 fof(c_0_19, plain, ![X1]:((epred19_1(X1)<=>(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((p3(X1)&![X2]:((~r1(X1,X2)|p3(X2)))))|p2(X1)))|p3(X2)|~(((p2(X2)&![X1]:((~r1(X2,X1)|p2(X1))))&p2(X2)))))&![X2]:((~r1(X1,X2)|~((p3(X2)&![X1]:((~r1(X2,X1)|p3(X1)))))|p2(X2)|![X1]:((~r1(X2,X1)|p3(X1)|~(((p2(X1)&![X2]:((~r1(X1,X2)|p2(X2))))&p2(X1)))))))))), introduced(definition)).
% 0.62/0.62 fof(c_0_20, plain, ![X1]:((epred20_1(X1)<=>(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((p2(X1)&![X2]:((~r1(X1,X2)|p2(X2)))))|p1(X1)))|p2(X2)|~(((p1(X2)&![X1]:((~r1(X2,X1)|p1(X1))))&p1(X2)))))&![X2]:((~r1(X1,X2)|~((p2(X2)&![X1]:((~r1(X2,X1)|p2(X1)))))|p1(X2)|![X1]:((~r1(X2,X1)|p2(X1)|~(((p1(X1)&![X2]:((~r1(X1,X2)|p1(X2))))&p1(X1)))))))))), introduced(definition)).
% 0.62/0.62 fof(c_0_21, negated_conjecture, ~(~(?[X1]:(~((~((![X2]:((~r1(X1,X2)|~((p21(X2)&![X1]:((~r1(X2,X1)|p21(X1)))))|p20(X2)))|![X2]:((~r1(X1,X2)|p21(X2)|~(((p20(X2)&![X1]:((~r1(X2,X1)|p20(X1))))&p20(X2)))))|~((epred1_1(X1)&![X2]:((~r1(X1,X2)|~((p21(X2)&![X1]:((~r1(X2,X1)|p21(X1)))))|p20(X2)|p21(X2)|~(((p20(X2)&![X1]:((~r1(X2,X1)|p20(X1))))&p20(X2)))))))))|~((![X2]:((~r1(X1,X2)|~((p20(X2)&![X1]:((~r1(X2,X1)|p20(X1)))))|p19(X2)))|![X2]:((~r1(X1,X2)|p20(X2)|~(((p19(X2)&![X1]:((~r1(X2,X1)|p19(X1))))&p19(X2)))))|~((epred2_1(X1)&![X2]:((~r1(X1,X2)|~((p20(X2)&![X1]:((~r1(X2,X1)|p20(X1)))))|p19(X2)|p20(X2)|~(((p19(X2)&![X1]:((~r1(X2,X1)|p19(X1))))&p19(X2)))))))))|~((![X2]:((~r1(X1,X2)|~((p19(X2)&![X1]:((~r1(X2,X1)|p19(X1)))))|p18(X2)))|![X2]:((~r1(X1,X2)|p19(X2)|~(((p18(X2)&![X1]:((~r1(X2,X1)|p18(X1))))&p18(X2)))))|~((epred3_1(X1)&![X2]:((~r1(X1,X2)|~((p19(X2)&![X1]:((~r1(X2,X1)|p19(X1)))))|p18(X2)|p19(X2)|~(((p18(X2)&![X1]:((~r1(X2,X1)|p18(X1))))&p18(X2)))))))))|~((![X2]:((~r1(X1,X2)|~((p18(X2)&![X1]:((~r1(X2,X1)|p18(X1)))))|p17(X2)))|![X2]:((~r1(X1,X2)|p18(X2)|~(((p17(X2)&![X1]:((~r1(X2,X1)|p17(X1))))&p17(X2)))))|~((epred4_1(X1)&![X2]:((~r1(X1,X2)|~((p18(X2)&![X1]:((~r1(X2,X1)|p18(X1)))))|p17(X2)|p18(X2)|~(((p17(X2)&![X1]:((~r1(X2,X1)|p17(X1))))&p17(X2)))))))))|~((![X2]:((~r1(X1,X2)|~((p17(X2)&![X1]:((~r1(X2,X1)|p17(X1)))))|p16(X2)))|![X2]:((~r1(X1,X2)|p17(X2)|~(((p16(X2)&![X1]:((~r1(X2,X1)|p16(X1))))&p16(X2)))))|~((epred5_1(X1)&![X2]:((~r1(X1,X2)|~((p17(X2)&![X1]:((~r1(X2,X1)|p17(X1)))))|p16(X2)|p17(X2)|~(((p16(X2)&![X1]:((~r1(X2,X1)|p16(X1))))&p16(X2)))))))))|~((![X2]:((~r1(X1,X2)|~((p16(X2)&![X1]:((~r1(X2,X1)|p16(X1)))))|p15(X2)))|![X2]:((~r1(X1,X2)|p16(X2)|~(((p15(X2)&![X1]:((~r1(X2,X1)|p15(X1))))&p15(X2)))))|~((epred6_1(X1)&![X2]:((~r1(X1,X2)|~((p16(X2)&![X1]:((~r1(X2,X1)|p16(X1)))))|p15(X2)|p16(X2)|~(((p15(X2)&![X1]:((~r1(X2,X1)|p15(X1))))&p15(X2)))))))))|~((![X2]:((~r1(X1,X2)|~((p15(X2)&![X1]:((~r1(X2,X1)|p15(X1)))))|p14(X2)))|![X2]:((~r1(X1,X2)|p15(X2)|~(((p14(X2)&![X1]:((~r1(X2,X1)|p14(X1))))&p14(X2)))))|~((epred7_1(X1)&![X2]:((~r1(X1,X2)|~((p15(X2)&![X1]:((~r1(X2,X1)|p15(X1)))))|p14(X2)|p15(X2)|~(((p14(X2)&![X1]:((~r1(X2,X1)|p14(X1))))&p14(X2)))))))))|~((![X2]:((~r1(X1,X2)|~((p14(X2)&![X1]:((~r1(X2,X1)|p14(X1)))))|p13(X2)))|![X2]:((~r1(X1,X2)|p14(X2)|~(((p13(X2)&![X1]:((~r1(X2,X1)|p13(X1))))&p13(X2)))))|~((epred8_1(X1)&![X2]:((~r1(X1,X2)|~((p14(X2)&![X1]:((~r1(X2,X1)|p14(X1)))))|p13(X2)|p14(X2)|~(((p13(X2)&![X1]:((~r1(X2,X1)|p13(X1))))&p13(X2)))))))))|~((![X2]:((~r1(X1,X2)|~((p13(X2)&![X1]:((~r1(X2,X1)|p13(X1)))))|p12(X2)))|![X2]:((~r1(X1,X2)|p13(X2)|~(((p12(X2)&![X1]:((~r1(X2,X1)|p12(X1))))&p12(X2)))))|~((epred9_1(X1)&![X2]:((~r1(X1,X2)|~((p13(X2)&![X1]:((~r1(X2,X1)|p13(X1)))))|p12(X2)|p13(X2)|~(((p12(X2)&![X1]:((~r1(X2,X1)|p12(X1))))&p12(X2)))))))))|~((![X2]:((~r1(X1,X2)|~((p12(X2)&![X1]:((~r1(X2,X1)|p12(X1)))))|p11(X2)))|![X2]:((~r1(X1,X2)|p12(X2)|~(((p11(X2)&![X1]:((~r1(X2,X1)|p11(X1))))&p11(X2)))))|~((epred10_1(X1)&![X2]:((~r1(X1,X2)|~((p12(X2)&![X1]:((~r1(X2,X1)|p12(X1)))))|p11(X2)|p12(X2)|~(((p11(X2)&![X1]:((~r1(X2,X1)|p11(X1))))&p11(X2)))))))))|~((![X2]:((~r1(X1,X2)|~((p11(X2)&![X1]:((~r1(X2,X1)|p11(X1)))))|p10(X2)))|![X2]:((~r1(X1,X2)|p11(X2)|~(((p10(X2)&![X1]:((~r1(X2,X1)|p10(X1))))&p10(X2)))))|~((epred11_1(X1)&![X2]:((~r1(X1,X2)|~((p11(X2)&![X1]:((~r1(X2,X1)|p11(X1)))))|p10(X2)|p11(X2)|~(((p10(X2)&![X1]:((~r1(X2,X1)|p10(X1))))&p10(X2)))))))))|~((![X2]:((~r1(X1,X2)|~((p10(X2)&![X1]:((~r1(X2,X1)|p10(X1)))))|p9(X2)))|![X2]:((~r1(X1,X2)|p10(X2)|~(((p9(X2)&![X1]:((~r1(X2,X1)|p9(X1))))&p9(X2)))))|~((epred12_1(X1)&![X2]:((~r1(X1,X2)|~((p10(X2)&![X1]:((~r1(X2,X1)|p10(X1)))))|p9(X2)|p10(X2)|~(((p9(X2)&![X1]:((~r1(X2,X1)|p9(X1))))&p9(X2)))))))))|~((![X2]:((~r1(X1,X2)|~((p9(X2)&![X1]:((~r1(X2,X1)|p9(X1)))))|p8(X2)))|![X2]:((~r1(X1,X2)|p9(X2)|~(((p8(X2)&![X1]:((~r1(X2,X1)|p8(X1))))&p8(X2)))))|~((epred13_1(X1)&![X2]:((~r1(X1,X2)|~((p9(X2)&![X1]:((~r1(X2,X1)|p9(X1)))))|p8(X2)|p9(X2)|~(((p8(X2)&![X1]:((~r1(X2,X1)|p8(X1))))&p8(X2)))))))))|~((![X2]:((~r1(X1,X2)|~((p8(X2)&![X1]:((~r1(X2,X1)|p8(X1)))))|p7(X2)))|![X2]:((~r1(X1,X2)|p8(X2)|~(((p7(X2)&![X1]:((~r1(X2,X1)|p7(X1))))&p7(X2)))))|~((epred14_1(X1)&![X2]:((~r1(X1,X2)|~((p8(X2)&![X1]:((~r1(X2,X1)|p8(X1)))))|p7(X2)|p8(X2)|~(((p7(X2)&![X1]:((~r1(X2,X1)|p7(X1))))&p7(X2)))))))))|![X2]:((~r1(X1,X2)|p20(X2)|~((![X1]:((~r1(X2,X1)|p20(X1)))&p20(X2)))))|![X2]:((~r1(X1,X2)|p20(X2)|~((![X1]:((~r1(X2,X1)|p20(X1)))&p20(X2)))))|~((![X2]:((~r1(X1,X2)|~((p7(X2)&![X1]:((~r1(X2,X1)|p7(X1)))))|p6(X2)))|![X2]:((~r1(X1,X2)|p7(X2)|~(((p6(X2)&![X1]:((~r1(X2,X1)|p6(X1))))&p6(X2)))))|~((epred15_1(X1)&![X2]:((~r1(X1,X2)|~((p7(X2)&![X1]:((~r1(X2,X1)|p7(X1)))))|p6(X2)|p7(X2)|~(((p6(X2)&![X1]:((~r1(X2,X1)|p6(X1))))&p6(X2)))))))))|~((![X2]:((~r1(X1,X2)|~((p6(X2)&![X1]:((~r1(X2,X1)|p6(X1)))))|p5(X2)))|![X2]:((~r1(X1,X2)|p6(X2)|~(((p5(X2)&![X1]:((~r1(X2,X1)|p5(X1))))&p5(X2)))))|~((epred16_1(X1)&![X2]:((~r1(X1,X2)|~((p6(X2)&![X1]:((~r1(X2,X1)|p6(X1)))))|p5(X2)|p6(X2)|~(((p5(X2)&![X1]:((~r1(X2,X1)|p5(X1))))&p5(X2)))))))))|~((![X2]:((~r1(X1,X2)|~((p5(X2)&![X1]:((~r1(X2,X1)|p5(X1)))))|p4(X2)))|![X2]:((~r1(X1,X2)|p5(X2)|~(((p4(X2)&![X1]:((~r1(X2,X1)|p4(X1))))&p4(X2)))))|~((epred17_1(X1)&![X2]:((~r1(X1,X2)|~((p5(X2)&![X1]:((~r1(X2,X1)|p5(X1)))))|p4(X2)|p5(X2)|~(((p4(X2)&![X1]:((~r1(X2,X1)|p4(X1))))&p4(X2)))))))))|~((![X2]:((~r1(X1,X2)|~((p4(X2)&![X1]:((~r1(X2,X1)|p4(X1)))))|p3(X2)))|![X2]:((~r1(X1,X2)|p4(X2)|~(((p3(X2)&![X1]:((~r1(X2,X1)|p3(X1))))&p3(X2)))))|~((epred18_1(X1)&![X2]:((~r1(X1,X2)|~((p4(X2)&![X1]:((~r1(X2,X1)|p4(X1)))))|p3(X2)|p4(X2)|~(((p3(X2)&![X1]:((~r1(X2,X1)|p3(X1))))&p3(X2)))))))))|~((![X2]:((~r1(X1,X2)|~((p3(X2)&![X1]:((~r1(X2,X1)|p3(X1)))))|p2(X2)))|![X2]:((~r1(X1,X2)|p3(X2)|~(((p2(X2)&![X1]:((~r1(X2,X1)|p2(X1))))&p2(X2)))))|~((epred19_1(X1)&![X2]:((~r1(X1,X2)|~((p3(X2)&![X1]:((~r1(X2,X1)|p3(X1)))))|p2(X2)|p3(X2)|~(((p2(X2)&![X1]:((~r1(X2,X1)|p2(X1))))&p2(X2)))))))))|~((![X2]:((~r1(X1,X2)|~((p2(X2)&![X1]:((~r1(X2,X1)|p2(X1)))))|p1(X2)))|![X2]:((~r1(X1,X2)|p2(X2)|~(((p1(X2)&![X1]:((~r1(X2,X1)|p1(X1))))&p1(X2)))))|~((epred20_1(X1)&![X2]:((~r1(X1,X2)|~((p2(X2)&![X1]:((~r1(X2,X1)|p2(X1)))))|p1(X2)|p2(X2)|~(((p1(X2)&![X1]:((~r1(X2,X1)|p1(X1))))&p1(X2)))))))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])]), c_0_1]), c_0_2]), c_0_3]), c_0_4]), c_0_5]), c_0_6]), c_0_7]), c_0_8]), c_0_9]), c_0_10]), c_0_11]), c_0_12]), c_0_13]), c_0_14]), c_0_15]), c_0_16]), c_0_17]), c_0_18]), c_0_19]), c_0_20])).
% 0.62/0.62 fof(c_0_22, negated_conjecture, ![X4, X6, X9, X10, X11, X13, X16, X17, X18, X20, X23, X24, X25, X27, X30, X31, X32, X34, X37, X38, X39, X41, X44, X45, X46, X48, X51, X52, X53, X55, X58, X59, X60, X62, X65, X66, X67, X69, X72, X73, X74, X76, X79, X80, X81, X83, X86, X87, X88, X90, X93, X94, X95, X97, X100, X101, X103, X105, X106, X108, X111, X112, X113, X115, X118, X119, X120, X122, X125, X126, X127, X129, X132, X133, X134, X136, X139, X140, X141, X143, X146, X147]:(((((((((((((((((((((((((((((r1(esk1_0,esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(r1(X4,esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4))))&((p21(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(r1(X4,esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4))))&(~r1(esk4_0,X9)|p21(X9)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(r1(X4,esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4))))))&(~p20(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(r1(X4,esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4)))))&(~p21(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(r1(X4,esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4)))))&(((p20(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(r1(X4,esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4))))&(~r1(esk4_0,X10)|p20(X10)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(r1(X4,esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4)))))&(p20(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(r1(X4,esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4))))))&(((((r1(esk1_0,esk4_0)|~epred1_1(esk1_0)|(~p20(esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(r1(X4,esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4))))&((p21(esk4_0)|~epred1_1(esk1_0)|(~p20(esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(r1(X4,esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4))))&(~r1(esk4_0,X9)|p21(X9)|~epred1_1(esk1_0)|(~p20(esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(r1(X4,esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4))))))&(~p20(esk4_0)|~epred1_1(esk1_0)|(~p20(esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(r1(X4,esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4)))))&(~p21(esk4_0)|~epred1_1(esk1_0)|(~p20(esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(r1(X4,esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4)))))&(((p20(esk4_0)|~epred1_1(esk1_0)|(~p20(esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(r1(X4,esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4))))&(~r1(esk4_0,X10)|p20(X10)|~epred1_1(esk1_0)|(~p20(esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(r1(X4,esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4)))))&(p20(esk4_0)|~epred1_1(esk1_0)|(~p20(esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(r1(X4,esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4)))))))&((((((r1(esk1_0,esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(~p21(esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4))))&((p21(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(~p21(esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4))))&(~r1(esk4_0,X9)|p21(X9)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(~p21(esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4))))))&(~p20(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(~p21(esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4)))))&(~p21(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(~p21(esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4)))))&(((p20(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(~p21(esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4))))&(~r1(esk4_0,X10)|p20(X10)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(~p21(esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4)))))&(p20(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(~p21(esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4))))))&(((((r1(esk1_0,esk4_0)|~epred1_1(esk1_0)|(~p20(esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(~p21(esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4))))&((p21(esk4_0)|~epred1_1(esk1_0)|(~p20(esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(~p21(esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4))))&(~r1(esk4_0,X9)|p21(X9)|~epred1_1(esk1_0)|(~p20(esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(~p21(esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4))))))&(~p20(esk4_0)|~epred1_1(esk1_0)|(~p20(esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(~p21(esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4)))))&(~p21(esk4_0)|~epred1_1(esk1_0)|(~p20(esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(~p21(esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4)))))&(((p20(esk4_0)|~epred1_1(esk1_0)|(~p20(esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(~p21(esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4))))&(~r1(esk4_0,X10)|p20(X10)|~epred1_1(esk1_0)|(~p20(esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(~p21(esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4)))))&(p20(esk4_0)|~epred1_1(esk1_0)|(~p20(esk3_1(X6))|~p20(X6)|~p20(X6)|(~r1(esk1_0,X6)|p21(X6))|(~p21(esk2_1(X4))|~p21(X4)|~r1(esk1_0,X4)|p20(X4))))))))&(((((((r1(esk1_0,esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(r1(X11,esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11))))&((p20(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(r1(X11,esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11))))&(~r1(esk7_0,X16)|p20(X16)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(r1(X11,esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11))))))&(~p19(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(r1(X11,esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11)))))&(~p20(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(r1(X11,esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11)))))&(((p19(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(r1(X11,esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11))))&(~r1(esk7_0,X17)|p19(X17)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(r1(X11,esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11)))))&(p19(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(r1(X11,esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11))))))&(((((r1(esk1_0,esk7_0)|~epred2_1(esk1_0)|(~p19(esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(r1(X11,esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11))))&((p20(esk7_0)|~epred2_1(esk1_0)|(~p19(esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(r1(X11,esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11))))&(~r1(esk7_0,X16)|p20(X16)|~epred2_1(esk1_0)|(~p19(esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(r1(X11,esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11))))))&(~p19(esk7_0)|~epred2_1(esk1_0)|(~p19(esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(r1(X11,esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11)))))&(~p20(esk7_0)|~epred2_1(esk1_0)|(~p19(esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(r1(X11,esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11)))))&(((p19(esk7_0)|~epred2_1(esk1_0)|(~p19(esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(r1(X11,esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11))))&(~r1(esk7_0,X17)|p19(X17)|~epred2_1(esk1_0)|(~p19(esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(r1(X11,esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11)))))&(p19(esk7_0)|~epred2_1(esk1_0)|(~p19(esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(r1(X11,esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11)))))))&((((((r1(esk1_0,esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(~p20(esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11))))&((p20(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(~p20(esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11))))&(~r1(esk7_0,X16)|p20(X16)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(~p20(esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11))))))&(~p19(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(~p20(esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11)))))&(~p20(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(~p20(esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11)))))&(((p19(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(~p20(esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11))))&(~r1(esk7_0,X17)|p19(X17)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(~p20(esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11)))))&(p19(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(~p20(esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11))))))&(((((r1(esk1_0,esk7_0)|~epred2_1(esk1_0)|(~p19(esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(~p20(esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11))))&((p20(esk7_0)|~epred2_1(esk1_0)|(~p19(esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(~p20(esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11))))&(~r1(esk7_0,X16)|p20(X16)|~epred2_1(esk1_0)|(~p19(esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(~p20(esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11))))))&(~p19(esk7_0)|~epred2_1(esk1_0)|(~p19(esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(~p20(esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11)))))&(~p20(esk7_0)|~epred2_1(esk1_0)|(~p19(esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(~p20(esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11)))))&(((p19(esk7_0)|~epred2_1(esk1_0)|(~p19(esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(~p20(esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11))))&(~r1(esk7_0,X17)|p19(X17)|~epred2_1(esk1_0)|(~p19(esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(~p20(esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11)))))&(p19(esk7_0)|~epred2_1(esk1_0)|(~p19(esk6_1(X13))|~p19(X13)|~p19(X13)|(~r1(esk1_0,X13)|p20(X13))|(~p20(esk5_1(X11))|~p20(X11)|~r1(esk1_0,X11)|p19(X11)))))))))&(((((((r1(esk1_0,esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(r1(X18,esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18))))&((p19(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(r1(X18,esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18))))&(~r1(esk10_0,X23)|p19(X23)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(r1(X18,esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18))))))&(~p18(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(r1(X18,esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18)))))&(~p19(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(r1(X18,esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18)))))&(((p18(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(r1(X18,esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18))))&(~r1(esk10_0,X24)|p18(X24)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(r1(X18,esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18)))))&(p18(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(r1(X18,esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18))))))&(((((r1(esk1_0,esk10_0)|~epred3_1(esk1_0)|(~p18(esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(r1(X18,esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18))))&((p19(esk10_0)|~epred3_1(esk1_0)|(~p18(esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(r1(X18,esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18))))&(~r1(esk10_0,X23)|p19(X23)|~epred3_1(esk1_0)|(~p18(esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(r1(X18,esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18))))))&(~p18(esk10_0)|~epred3_1(esk1_0)|(~p18(esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(r1(X18,esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18)))))&(~p19(esk10_0)|~epred3_1(esk1_0)|(~p18(esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(r1(X18,esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18)))))&(((p18(esk10_0)|~epred3_1(esk1_0)|(~p18(esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(r1(X18,esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18))))&(~r1(esk10_0,X24)|p18(X24)|~epred3_1(esk1_0)|(~p18(esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(r1(X18,esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18)))))&(p18(esk10_0)|~epred3_1(esk1_0)|(~p18(esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(r1(X18,esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18)))))))&((((((r1(esk1_0,esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(~p19(esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18))))&((p19(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(~p19(esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18))))&(~r1(esk10_0,X23)|p19(X23)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(~p19(esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18))))))&(~p18(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(~p19(esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18)))))&(~p19(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(~p19(esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18)))))&(((p18(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(~p19(esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18))))&(~r1(esk10_0,X24)|p18(X24)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(~p19(esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18)))))&(p18(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(~p19(esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18))))))&(((((r1(esk1_0,esk10_0)|~epred3_1(esk1_0)|(~p18(esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(~p19(esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18))))&((p19(esk10_0)|~epred3_1(esk1_0)|(~p18(esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(~p19(esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18))))&(~r1(esk10_0,X23)|p19(X23)|~epred3_1(esk1_0)|(~p18(esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(~p19(esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18))))))&(~p18(esk10_0)|~epred3_1(esk1_0)|(~p18(esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(~p19(esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18)))))&(~p19(esk10_0)|~epred3_1(esk1_0)|(~p18(esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(~p19(esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18)))))&(((p18(esk10_0)|~epred3_1(esk1_0)|(~p18(esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(~p19(esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18))))&(~r1(esk10_0,X24)|p18(X24)|~epred3_1(esk1_0)|(~p18(esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(~p19(esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18)))))&(p18(esk10_0)|~epred3_1(esk1_0)|(~p18(esk9_1(X20))|~p18(X20)|~p18(X20)|(~r1(esk1_0,X20)|p19(X20))|(~p19(esk8_1(X18))|~p19(X18)|~r1(esk1_0,X18)|p18(X18)))))))))&(((((((r1(esk1_0,esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(r1(X25,esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25))))&((p18(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(r1(X25,esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25))))&(~r1(esk13_0,X30)|p18(X30)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(r1(X25,esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25))))))&(~p17(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(r1(X25,esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25)))))&(~p18(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(r1(X25,esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25)))))&(((p17(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(r1(X25,esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25))))&(~r1(esk13_0,X31)|p17(X31)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(r1(X25,esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25)))))&(p17(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(r1(X25,esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25))))))&(((((r1(esk1_0,esk13_0)|~epred4_1(esk1_0)|(~p17(esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(r1(X25,esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25))))&((p18(esk13_0)|~epred4_1(esk1_0)|(~p17(esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(r1(X25,esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25))))&(~r1(esk13_0,X30)|p18(X30)|~epred4_1(esk1_0)|(~p17(esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(r1(X25,esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25))))))&(~p17(esk13_0)|~epred4_1(esk1_0)|(~p17(esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(r1(X25,esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25)))))&(~p18(esk13_0)|~epred4_1(esk1_0)|(~p17(esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(r1(X25,esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25)))))&(((p17(esk13_0)|~epred4_1(esk1_0)|(~p17(esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(r1(X25,esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25))))&(~r1(esk13_0,X31)|p17(X31)|~epred4_1(esk1_0)|(~p17(esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(r1(X25,esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25)))))&(p17(esk13_0)|~epred4_1(esk1_0)|(~p17(esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(r1(X25,esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25)))))))&((((((r1(esk1_0,esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(~p18(esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25))))&((p18(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(~p18(esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25))))&(~r1(esk13_0,X30)|p18(X30)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(~p18(esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25))))))&(~p17(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(~p18(esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25)))))&(~p18(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(~p18(esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25)))))&(((p17(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(~p18(esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25))))&(~r1(esk13_0,X31)|p17(X31)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(~p18(esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25)))))&(p17(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(~p18(esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25))))))&(((((r1(esk1_0,esk13_0)|~epred4_1(esk1_0)|(~p17(esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(~p18(esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25))))&((p18(esk13_0)|~epred4_1(esk1_0)|(~p17(esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(~p18(esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25))))&(~r1(esk13_0,X30)|p18(X30)|~epred4_1(esk1_0)|(~p17(esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(~p18(esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25))))))&(~p17(esk13_0)|~epred4_1(esk1_0)|(~p17(esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(~p18(esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25)))))&(~p18(esk13_0)|~epred4_1(esk1_0)|(~p17(esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(~p18(esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25)))))&(((p17(esk13_0)|~epred4_1(esk1_0)|(~p17(esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(~p18(esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25))))&(~r1(esk13_0,X31)|p17(X31)|~epred4_1(esk1_0)|(~p17(esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(~p18(esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25)))))&(p17(esk13_0)|~epred4_1(esk1_0)|(~p17(esk12_1(X27))|~p17(X27)|~p17(X27)|(~r1(esk1_0,X27)|p18(X27))|(~p18(esk11_1(X25))|~p18(X25)|~r1(esk1_0,X25)|p17(X25)))))))))&(((((((r1(esk1_0,esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(r1(X32,esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32))))&((p17(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(r1(X32,esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32))))&(~r1(esk16_0,X37)|p17(X37)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(r1(X32,esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32))))))&(~p16(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(r1(X32,esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32)))))&(~p17(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(r1(X32,esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32)))))&(((p16(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(r1(X32,esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32))))&(~r1(esk16_0,X38)|p16(X38)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(r1(X32,esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32)))))&(p16(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(r1(X32,esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32))))))&(((((r1(esk1_0,esk16_0)|~epred5_1(esk1_0)|(~p16(esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(r1(X32,esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32))))&((p17(esk16_0)|~epred5_1(esk1_0)|(~p16(esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(r1(X32,esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32))))&(~r1(esk16_0,X37)|p17(X37)|~epred5_1(esk1_0)|(~p16(esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(r1(X32,esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32))))))&(~p16(esk16_0)|~epred5_1(esk1_0)|(~p16(esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(r1(X32,esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32)))))&(~p17(esk16_0)|~epred5_1(esk1_0)|(~p16(esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(r1(X32,esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32)))))&(((p16(esk16_0)|~epred5_1(esk1_0)|(~p16(esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(r1(X32,esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32))))&(~r1(esk16_0,X38)|p16(X38)|~epred5_1(esk1_0)|(~p16(esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(r1(X32,esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32)))))&(p16(esk16_0)|~epred5_1(esk1_0)|(~p16(esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(r1(X32,esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32)))))))&((((((r1(esk1_0,esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(~p17(esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32))))&((p17(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(~p17(esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32))))&(~r1(esk16_0,X37)|p17(X37)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(~p17(esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32))))))&(~p16(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(~p17(esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32)))))&(~p17(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(~p17(esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32)))))&(((p16(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(~p17(esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32))))&(~r1(esk16_0,X38)|p16(X38)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(~p17(esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32)))))&(p16(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(~p17(esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32))))))&(((((r1(esk1_0,esk16_0)|~epred5_1(esk1_0)|(~p16(esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(~p17(esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32))))&((p17(esk16_0)|~epred5_1(esk1_0)|(~p16(esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(~p17(esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32))))&(~r1(esk16_0,X37)|p17(X37)|~epred5_1(esk1_0)|(~p16(esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(~p17(esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32))))))&(~p16(esk16_0)|~epred5_1(esk1_0)|(~p16(esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(~p17(esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32)))))&(~p17(esk16_0)|~epred5_1(esk1_0)|(~p16(esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(~p17(esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32)))))&(((p16(esk16_0)|~epred5_1(esk1_0)|(~p16(esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(~p17(esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32))))&(~r1(esk16_0,X38)|p16(X38)|~epred5_1(esk1_0)|(~p16(esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(~p17(esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32)))))&(p16(esk16_0)|~epred5_1(esk1_0)|(~p16(esk15_1(X34))|~p16(X34)|~p16(X34)|(~r1(esk1_0,X34)|p17(X34))|(~p17(esk14_1(X32))|~p17(X32)|~r1(esk1_0,X32)|p16(X32)))))))))&(((((((r1(esk1_0,esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(r1(X39,esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39))))&((p16(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(r1(X39,esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39))))&(~r1(esk19_0,X44)|p16(X44)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(r1(X39,esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39))))))&(~p15(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(r1(X39,esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39)))))&(~p16(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(r1(X39,esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39)))))&(((p15(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(r1(X39,esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39))))&(~r1(esk19_0,X45)|p15(X45)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(r1(X39,esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39)))))&(p15(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(r1(X39,esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39))))))&(((((r1(esk1_0,esk19_0)|~epred6_1(esk1_0)|(~p15(esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(r1(X39,esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39))))&((p16(esk19_0)|~epred6_1(esk1_0)|(~p15(esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(r1(X39,esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39))))&(~r1(esk19_0,X44)|p16(X44)|~epred6_1(esk1_0)|(~p15(esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(r1(X39,esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39))))))&(~p15(esk19_0)|~epred6_1(esk1_0)|(~p15(esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(r1(X39,esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39)))))&(~p16(esk19_0)|~epred6_1(esk1_0)|(~p15(esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(r1(X39,esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39)))))&(((p15(esk19_0)|~epred6_1(esk1_0)|(~p15(esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(r1(X39,esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39))))&(~r1(esk19_0,X45)|p15(X45)|~epred6_1(esk1_0)|(~p15(esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(r1(X39,esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39)))))&(p15(esk19_0)|~epred6_1(esk1_0)|(~p15(esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(r1(X39,esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39)))))))&((((((r1(esk1_0,esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(~p16(esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39))))&((p16(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(~p16(esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39))))&(~r1(esk19_0,X44)|p16(X44)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(~p16(esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39))))))&(~p15(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(~p16(esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39)))))&(~p16(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(~p16(esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39)))))&(((p15(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(~p16(esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39))))&(~r1(esk19_0,X45)|p15(X45)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(~p16(esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39)))))&(p15(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(~p16(esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39))))))&(((((r1(esk1_0,esk19_0)|~epred6_1(esk1_0)|(~p15(esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(~p16(esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39))))&((p16(esk19_0)|~epred6_1(esk1_0)|(~p15(esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(~p16(esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39))))&(~r1(esk19_0,X44)|p16(X44)|~epred6_1(esk1_0)|(~p15(esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(~p16(esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39))))))&(~p15(esk19_0)|~epred6_1(esk1_0)|(~p15(esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(~p16(esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39)))))&(~p16(esk19_0)|~epred6_1(esk1_0)|(~p15(esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(~p16(esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39)))))&(((p15(esk19_0)|~epred6_1(esk1_0)|(~p15(esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(~p16(esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39))))&(~r1(esk19_0,X45)|p15(X45)|~epred6_1(esk1_0)|(~p15(esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(~p16(esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39)))))&(p15(esk19_0)|~epred6_1(esk1_0)|(~p15(esk18_1(X41))|~p15(X41)|~p15(X41)|(~r1(esk1_0,X41)|p16(X41))|(~p16(esk17_1(X39))|~p16(X39)|~r1(esk1_0,X39)|p15(X39)))))))))&(((((((r1(esk1_0,esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(r1(X46,esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46))))&((p15(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(r1(X46,esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46))))&(~r1(esk22_0,X51)|p15(X51)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(r1(X46,esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46))))))&(~p14(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(r1(X46,esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46)))))&(~p15(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(r1(X46,esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46)))))&(((p14(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(r1(X46,esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46))))&(~r1(esk22_0,X52)|p14(X52)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(r1(X46,esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46)))))&(p14(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(r1(X46,esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46))))))&(((((r1(esk1_0,esk22_0)|~epred7_1(esk1_0)|(~p14(esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(r1(X46,esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46))))&((p15(esk22_0)|~epred7_1(esk1_0)|(~p14(esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(r1(X46,esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46))))&(~r1(esk22_0,X51)|p15(X51)|~epred7_1(esk1_0)|(~p14(esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(r1(X46,esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46))))))&(~p14(esk22_0)|~epred7_1(esk1_0)|(~p14(esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(r1(X46,esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46)))))&(~p15(esk22_0)|~epred7_1(esk1_0)|(~p14(esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(r1(X46,esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46)))))&(((p14(esk22_0)|~epred7_1(esk1_0)|(~p14(esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(r1(X46,esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46))))&(~r1(esk22_0,X52)|p14(X52)|~epred7_1(esk1_0)|(~p14(esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(r1(X46,esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46)))))&(p14(esk22_0)|~epred7_1(esk1_0)|(~p14(esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(r1(X46,esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46)))))))&((((((r1(esk1_0,esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(~p15(esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46))))&((p15(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(~p15(esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46))))&(~r1(esk22_0,X51)|p15(X51)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(~p15(esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46))))))&(~p14(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(~p15(esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46)))))&(~p15(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(~p15(esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46)))))&(((p14(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(~p15(esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46))))&(~r1(esk22_0,X52)|p14(X52)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(~p15(esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46)))))&(p14(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(~p15(esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46))))))&(((((r1(esk1_0,esk22_0)|~epred7_1(esk1_0)|(~p14(esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(~p15(esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46))))&((p15(esk22_0)|~epred7_1(esk1_0)|(~p14(esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(~p15(esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46))))&(~r1(esk22_0,X51)|p15(X51)|~epred7_1(esk1_0)|(~p14(esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(~p15(esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46))))))&(~p14(esk22_0)|~epred7_1(esk1_0)|(~p14(esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(~p15(esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46)))))&(~p15(esk22_0)|~epred7_1(esk1_0)|(~p14(esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(~p15(esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46)))))&(((p14(esk22_0)|~epred7_1(esk1_0)|(~p14(esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(~p15(esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46))))&(~r1(esk22_0,X52)|p14(X52)|~epred7_1(esk1_0)|(~p14(esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(~p15(esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46)))))&(p14(esk22_0)|~epred7_1(esk1_0)|(~p14(esk21_1(X48))|~p14(X48)|~p14(X48)|(~r1(esk1_0,X48)|p15(X48))|(~p15(esk20_1(X46))|~p15(X46)|~r1(esk1_0,X46)|p14(X46)))))))))&(((((((r1(esk1_0,esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(r1(X53,esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53))))&((p14(esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(r1(X53,esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53))))&(~r1(esk25_0,X58)|p14(X58)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(r1(X53,esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53))))))&(~p13(esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(r1(X53,esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53)))))&(~p14(esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(r1(X53,esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53)))))&(((p13(esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(r1(X53,esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53))))&(~r1(esk25_0,X59)|p13(X59)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(r1(X53,esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53)))))&(p13(esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(r1(X53,esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53))))))&(((((r1(esk1_0,esk25_0)|~epred8_1(esk1_0)|(~p13(esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(r1(X53,esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53))))&((p14(esk25_0)|~epred8_1(esk1_0)|(~p13(esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(r1(X53,esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53))))&(~r1(esk25_0,X58)|p14(X58)|~epred8_1(esk1_0)|(~p13(esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(r1(X53,esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53))))))&(~p13(esk25_0)|~epred8_1(esk1_0)|(~p13(esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(r1(X53,esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53)))))&(~p14(esk25_0)|~epred8_1(esk1_0)|(~p13(esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(r1(X53,esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53)))))&(((p13(esk25_0)|~epred8_1(esk1_0)|(~p13(esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(r1(X53,esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53))))&(~r1(esk25_0,X59)|p13(X59)|~epred8_1(esk1_0)|(~p13(esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(r1(X53,esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53)))))&(p13(esk25_0)|~epred8_1(esk1_0)|(~p13(esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(r1(X53,esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53)))))))&((((((r1(esk1_0,esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(~p14(esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53))))&((p14(esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(~p14(esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53))))&(~r1(esk25_0,X58)|p14(X58)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(~p14(esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53))))))&(~p13(esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(~p14(esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53)))))&(~p14(esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(~p14(esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53)))))&(((p13(esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(~p14(esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53))))&(~r1(esk25_0,X59)|p13(X59)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(~p14(esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53)))))&(p13(esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(~p14(esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53))))))&(((((r1(esk1_0,esk25_0)|~epred8_1(esk1_0)|(~p13(esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(~p14(esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53))))&((p14(esk25_0)|~epred8_1(esk1_0)|(~p13(esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(~p14(esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53))))&(~r1(esk25_0,X58)|p14(X58)|~epred8_1(esk1_0)|(~p13(esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(~p14(esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53))))))&(~p13(esk25_0)|~epred8_1(esk1_0)|(~p13(esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(~p14(esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53)))))&(~p14(esk25_0)|~epred8_1(esk1_0)|(~p13(esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(~p14(esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53)))))&(((p13(esk25_0)|~epred8_1(esk1_0)|(~p13(esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(~p14(esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53))))&(~r1(esk25_0,X59)|p13(X59)|~epred8_1(esk1_0)|(~p13(esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(~p14(esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53)))))&(p13(esk25_0)|~epred8_1(esk1_0)|(~p13(esk24_1(X55))|~p13(X55)|~p13(X55)|(~r1(esk1_0,X55)|p14(X55))|(~p14(esk23_1(X53))|~p14(X53)|~r1(esk1_0,X53)|p13(X53)))))))))&(((((((r1(esk1_0,esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(r1(X60,esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60))))&((p13(esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(r1(X60,esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60))))&(~r1(esk28_0,X65)|p13(X65)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(r1(X60,esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60))))))&(~p12(esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(r1(X60,esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60)))))&(~p13(esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(r1(X60,esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60)))))&(((p12(esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(r1(X60,esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60))))&(~r1(esk28_0,X66)|p12(X66)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(r1(X60,esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60)))))&(p12(esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(r1(X60,esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60))))))&(((((r1(esk1_0,esk28_0)|~epred9_1(esk1_0)|(~p12(esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(r1(X60,esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60))))&((p13(esk28_0)|~epred9_1(esk1_0)|(~p12(esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(r1(X60,esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60))))&(~r1(esk28_0,X65)|p13(X65)|~epred9_1(esk1_0)|(~p12(esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(r1(X60,esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60))))))&(~p12(esk28_0)|~epred9_1(esk1_0)|(~p12(esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(r1(X60,esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60)))))&(~p13(esk28_0)|~epred9_1(esk1_0)|(~p12(esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(r1(X60,esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60)))))&(((p12(esk28_0)|~epred9_1(esk1_0)|(~p12(esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(r1(X60,esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60))))&(~r1(esk28_0,X66)|p12(X66)|~epred9_1(esk1_0)|(~p12(esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(r1(X60,esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60)))))&(p12(esk28_0)|~epred9_1(esk1_0)|(~p12(esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(r1(X60,esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60)))))))&((((((r1(esk1_0,esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(~p13(esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60))))&((p13(esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(~p13(esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60))))&(~r1(esk28_0,X65)|p13(X65)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(~p13(esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60))))))&(~p12(esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(~p13(esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60)))))&(~p13(esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(~p13(esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60)))))&(((p12(esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(~p13(esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60))))&(~r1(esk28_0,X66)|p12(X66)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(~p13(esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60)))))&(p12(esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(~p13(esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60))))))&(((((r1(esk1_0,esk28_0)|~epred9_1(esk1_0)|(~p12(esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(~p13(esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60))))&((p13(esk28_0)|~epred9_1(esk1_0)|(~p12(esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(~p13(esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60))))&(~r1(esk28_0,X65)|p13(X65)|~epred9_1(esk1_0)|(~p12(esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(~p13(esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60))))))&(~p12(esk28_0)|~epred9_1(esk1_0)|(~p12(esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(~p13(esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60)))))&(~p13(esk28_0)|~epred9_1(esk1_0)|(~p12(esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(~p13(esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60)))))&(((p12(esk28_0)|~epred9_1(esk1_0)|(~p12(esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(~p13(esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60))))&(~r1(esk28_0,X66)|p12(X66)|~epred9_1(esk1_0)|(~p12(esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(~p13(esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60)))))&(p12(esk28_0)|~epred9_1(esk1_0)|(~p12(esk27_1(X62))|~p12(X62)|~p12(X62)|(~r1(esk1_0,X62)|p13(X62))|(~p13(esk26_1(X60))|~p13(X60)|~r1(esk1_0,X60)|p12(X60)))))))))&(((((((r1(esk1_0,esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(r1(X67,esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67))))&((p12(esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(r1(X67,esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67))))&(~r1(esk31_0,X72)|p12(X72)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(r1(X67,esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67))))))&(~p11(esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(r1(X67,esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67)))))&(~p12(esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(r1(X67,esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67)))))&(((p11(esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(r1(X67,esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67))))&(~r1(esk31_0,X73)|p11(X73)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(r1(X67,esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67)))))&(p11(esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(r1(X67,esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67))))))&(((((r1(esk1_0,esk31_0)|~epred10_1(esk1_0)|(~p11(esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(r1(X67,esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67))))&((p12(esk31_0)|~epred10_1(esk1_0)|(~p11(esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(r1(X67,esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67))))&(~r1(esk31_0,X72)|p12(X72)|~epred10_1(esk1_0)|(~p11(esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(r1(X67,esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67))))))&(~p11(esk31_0)|~epred10_1(esk1_0)|(~p11(esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(r1(X67,esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67)))))&(~p12(esk31_0)|~epred10_1(esk1_0)|(~p11(esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(r1(X67,esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67)))))&(((p11(esk31_0)|~epred10_1(esk1_0)|(~p11(esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(r1(X67,esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67))))&(~r1(esk31_0,X73)|p11(X73)|~epred10_1(esk1_0)|(~p11(esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(r1(X67,esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67)))))&(p11(esk31_0)|~epred10_1(esk1_0)|(~p11(esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(r1(X67,esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67)))))))&((((((r1(esk1_0,esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(~p12(esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67))))&((p12(esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(~p12(esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67))))&(~r1(esk31_0,X72)|p12(X72)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(~p12(esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67))))))&(~p11(esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(~p12(esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67)))))&(~p12(esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(~p12(esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67)))))&(((p11(esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(~p12(esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67))))&(~r1(esk31_0,X73)|p11(X73)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(~p12(esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67)))))&(p11(esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(~p12(esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67))))))&(((((r1(esk1_0,esk31_0)|~epred10_1(esk1_0)|(~p11(esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(~p12(esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67))))&((p12(esk31_0)|~epred10_1(esk1_0)|(~p11(esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(~p12(esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67))))&(~r1(esk31_0,X72)|p12(X72)|~epred10_1(esk1_0)|(~p11(esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(~p12(esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67))))))&(~p11(esk31_0)|~epred10_1(esk1_0)|(~p11(esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(~p12(esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67)))))&(~p12(esk31_0)|~epred10_1(esk1_0)|(~p11(esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(~p12(esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67)))))&(((p11(esk31_0)|~epred10_1(esk1_0)|(~p11(esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(~p12(esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67))))&(~r1(esk31_0,X73)|p11(X73)|~epred10_1(esk1_0)|(~p11(esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(~p12(esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67)))))&(p11(esk31_0)|~epred10_1(esk1_0)|(~p11(esk30_1(X69))|~p11(X69)|~p11(X69)|(~r1(esk1_0,X69)|p12(X69))|(~p12(esk29_1(X67))|~p12(X67)|~r1(esk1_0,X67)|p11(X67)))))))))&(((((((r1(esk1_0,esk34_0)|~epred11_1(esk1_0)|(r1(X76,esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(r1(X74,esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74))))&((p11(esk34_0)|~epred11_1(esk1_0)|(r1(X76,esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(r1(X74,esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74))))&(~r1(esk34_0,X79)|p11(X79)|~epred11_1(esk1_0)|(r1(X76,esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(r1(X74,esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74))))))&(~p10(esk34_0)|~epred11_1(esk1_0)|(r1(X76,esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(r1(X74,esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74)))))&(~p11(esk34_0)|~epred11_1(esk1_0)|(r1(X76,esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(r1(X74,esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74)))))&(((p10(esk34_0)|~epred11_1(esk1_0)|(r1(X76,esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(r1(X74,esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74))))&(~r1(esk34_0,X80)|p10(X80)|~epred11_1(esk1_0)|(r1(X76,esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(r1(X74,esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74)))))&(p10(esk34_0)|~epred11_1(esk1_0)|(r1(X76,esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(r1(X74,esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74))))))&(((((r1(esk1_0,esk34_0)|~epred11_1(esk1_0)|(~p10(esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(r1(X74,esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74))))&((p11(esk34_0)|~epred11_1(esk1_0)|(~p10(esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(r1(X74,esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74))))&(~r1(esk34_0,X79)|p11(X79)|~epred11_1(esk1_0)|(~p10(esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(r1(X74,esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74))))))&(~p10(esk34_0)|~epred11_1(esk1_0)|(~p10(esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(r1(X74,esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74)))))&(~p11(esk34_0)|~epred11_1(esk1_0)|(~p10(esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(r1(X74,esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74)))))&(((p10(esk34_0)|~epred11_1(esk1_0)|(~p10(esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(r1(X74,esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74))))&(~r1(esk34_0,X80)|p10(X80)|~epred11_1(esk1_0)|(~p10(esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(r1(X74,esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74)))))&(p10(esk34_0)|~epred11_1(esk1_0)|(~p10(esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(r1(X74,esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74)))))))&((((((r1(esk1_0,esk34_0)|~epred11_1(esk1_0)|(r1(X76,esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(~p11(esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74))))&((p11(esk34_0)|~epred11_1(esk1_0)|(r1(X76,esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(~p11(esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74))))&(~r1(esk34_0,X79)|p11(X79)|~epred11_1(esk1_0)|(r1(X76,esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(~p11(esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74))))))&(~p10(esk34_0)|~epred11_1(esk1_0)|(r1(X76,esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(~p11(esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74)))))&(~p11(esk34_0)|~epred11_1(esk1_0)|(r1(X76,esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(~p11(esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74)))))&(((p10(esk34_0)|~epred11_1(esk1_0)|(r1(X76,esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(~p11(esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74))))&(~r1(esk34_0,X80)|p10(X80)|~epred11_1(esk1_0)|(r1(X76,esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(~p11(esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74)))))&(p10(esk34_0)|~epred11_1(esk1_0)|(r1(X76,esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(~p11(esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74))))))&(((((r1(esk1_0,esk34_0)|~epred11_1(esk1_0)|(~p10(esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(~p11(esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74))))&((p11(esk34_0)|~epred11_1(esk1_0)|(~p10(esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(~p11(esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74))))&(~r1(esk34_0,X79)|p11(X79)|~epred11_1(esk1_0)|(~p10(esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(~p11(esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74))))))&(~p10(esk34_0)|~epred11_1(esk1_0)|(~p10(esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(~p11(esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74)))))&(~p11(esk34_0)|~epred11_1(esk1_0)|(~p10(esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(~p11(esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74)))))&(((p10(esk34_0)|~epred11_1(esk1_0)|(~p10(esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(~p11(esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74))))&(~r1(esk34_0,X80)|p10(X80)|~epred11_1(esk1_0)|(~p10(esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(~p11(esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74)))))&(p10(esk34_0)|~epred11_1(esk1_0)|(~p10(esk33_1(X76))|~p10(X76)|~p10(X76)|(~r1(esk1_0,X76)|p11(X76))|(~p11(esk32_1(X74))|~p11(X74)|~r1(esk1_0,X74)|p10(X74)))))))))&(((((((r1(esk1_0,esk37_0)|~epred12_1(esk1_0)|(r1(X83,esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(r1(X81,esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81))))&((p10(esk37_0)|~epred12_1(esk1_0)|(r1(X83,esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(r1(X81,esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81))))&(~r1(esk37_0,X86)|p10(X86)|~epred12_1(esk1_0)|(r1(X83,esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(r1(X81,esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81))))))&(~p9(esk37_0)|~epred12_1(esk1_0)|(r1(X83,esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(r1(X81,esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81)))))&(~p10(esk37_0)|~epred12_1(esk1_0)|(r1(X83,esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(r1(X81,esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81)))))&(((p9(esk37_0)|~epred12_1(esk1_0)|(r1(X83,esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(r1(X81,esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81))))&(~r1(esk37_0,X87)|p9(X87)|~epred12_1(esk1_0)|(r1(X83,esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(r1(X81,esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81)))))&(p9(esk37_0)|~epred12_1(esk1_0)|(r1(X83,esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(r1(X81,esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81))))))&(((((r1(esk1_0,esk37_0)|~epred12_1(esk1_0)|(~p9(esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(r1(X81,esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81))))&((p10(esk37_0)|~epred12_1(esk1_0)|(~p9(esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(r1(X81,esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81))))&(~r1(esk37_0,X86)|p10(X86)|~epred12_1(esk1_0)|(~p9(esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(r1(X81,esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81))))))&(~p9(esk37_0)|~epred12_1(esk1_0)|(~p9(esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(r1(X81,esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81)))))&(~p10(esk37_0)|~epred12_1(esk1_0)|(~p9(esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(r1(X81,esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81)))))&(((p9(esk37_0)|~epred12_1(esk1_0)|(~p9(esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(r1(X81,esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81))))&(~r1(esk37_0,X87)|p9(X87)|~epred12_1(esk1_0)|(~p9(esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(r1(X81,esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81)))))&(p9(esk37_0)|~epred12_1(esk1_0)|(~p9(esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(r1(X81,esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81)))))))&((((((r1(esk1_0,esk37_0)|~epred12_1(esk1_0)|(r1(X83,esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(~p10(esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81))))&((p10(esk37_0)|~epred12_1(esk1_0)|(r1(X83,esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(~p10(esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81))))&(~r1(esk37_0,X86)|p10(X86)|~epred12_1(esk1_0)|(r1(X83,esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(~p10(esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81))))))&(~p9(esk37_0)|~epred12_1(esk1_0)|(r1(X83,esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(~p10(esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81)))))&(~p10(esk37_0)|~epred12_1(esk1_0)|(r1(X83,esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(~p10(esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81)))))&(((p9(esk37_0)|~epred12_1(esk1_0)|(r1(X83,esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(~p10(esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81))))&(~r1(esk37_0,X87)|p9(X87)|~epred12_1(esk1_0)|(r1(X83,esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(~p10(esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81)))))&(p9(esk37_0)|~epred12_1(esk1_0)|(r1(X83,esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(~p10(esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81))))))&(((((r1(esk1_0,esk37_0)|~epred12_1(esk1_0)|(~p9(esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(~p10(esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81))))&((p10(esk37_0)|~epred12_1(esk1_0)|(~p9(esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(~p10(esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81))))&(~r1(esk37_0,X86)|p10(X86)|~epred12_1(esk1_0)|(~p9(esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(~p10(esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81))))))&(~p9(esk37_0)|~epred12_1(esk1_0)|(~p9(esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(~p10(esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81)))))&(~p10(esk37_0)|~epred12_1(esk1_0)|(~p9(esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(~p10(esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81)))))&(((p9(esk37_0)|~epred12_1(esk1_0)|(~p9(esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(~p10(esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81))))&(~r1(esk37_0,X87)|p9(X87)|~epred12_1(esk1_0)|(~p9(esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(~p10(esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81)))))&(p9(esk37_0)|~epred12_1(esk1_0)|(~p9(esk36_1(X83))|~p9(X83)|~p9(X83)|(~r1(esk1_0,X83)|p10(X83))|(~p10(esk35_1(X81))|~p10(X81)|~r1(esk1_0,X81)|p9(X81)))))))))&(((((((r1(esk1_0,esk40_0)|~epred13_1(esk1_0)|(r1(X90,esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(r1(X88,esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88))))&((p9(esk40_0)|~epred13_1(esk1_0)|(r1(X90,esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(r1(X88,esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88))))&(~r1(esk40_0,X93)|p9(X93)|~epred13_1(esk1_0)|(r1(X90,esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(r1(X88,esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88))))))&(~p8(esk40_0)|~epred13_1(esk1_0)|(r1(X90,esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(r1(X88,esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88)))))&(~p9(esk40_0)|~epred13_1(esk1_0)|(r1(X90,esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(r1(X88,esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88)))))&(((p8(esk40_0)|~epred13_1(esk1_0)|(r1(X90,esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(r1(X88,esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88))))&(~r1(esk40_0,X94)|p8(X94)|~epred13_1(esk1_0)|(r1(X90,esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(r1(X88,esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88)))))&(p8(esk40_0)|~epred13_1(esk1_0)|(r1(X90,esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(r1(X88,esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88))))))&(((((r1(esk1_0,esk40_0)|~epred13_1(esk1_0)|(~p8(esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(r1(X88,esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88))))&((p9(esk40_0)|~epred13_1(esk1_0)|(~p8(esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(r1(X88,esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88))))&(~r1(esk40_0,X93)|p9(X93)|~epred13_1(esk1_0)|(~p8(esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(r1(X88,esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88))))))&(~p8(esk40_0)|~epred13_1(esk1_0)|(~p8(esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(r1(X88,esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88)))))&(~p9(esk40_0)|~epred13_1(esk1_0)|(~p8(esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(r1(X88,esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88)))))&(((p8(esk40_0)|~epred13_1(esk1_0)|(~p8(esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(r1(X88,esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88))))&(~r1(esk40_0,X94)|p8(X94)|~epred13_1(esk1_0)|(~p8(esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(r1(X88,esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88)))))&(p8(esk40_0)|~epred13_1(esk1_0)|(~p8(esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(r1(X88,esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88)))))))&((((((r1(esk1_0,esk40_0)|~epred13_1(esk1_0)|(r1(X90,esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(~p9(esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88))))&((p9(esk40_0)|~epred13_1(esk1_0)|(r1(X90,esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(~p9(esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88))))&(~r1(esk40_0,X93)|p9(X93)|~epred13_1(esk1_0)|(r1(X90,esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(~p9(esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88))))))&(~p8(esk40_0)|~epred13_1(esk1_0)|(r1(X90,esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(~p9(esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88)))))&(~p9(esk40_0)|~epred13_1(esk1_0)|(r1(X90,esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(~p9(esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88)))))&(((p8(esk40_0)|~epred13_1(esk1_0)|(r1(X90,esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(~p9(esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88))))&(~r1(esk40_0,X94)|p8(X94)|~epred13_1(esk1_0)|(r1(X90,esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(~p9(esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88)))))&(p8(esk40_0)|~epred13_1(esk1_0)|(r1(X90,esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(~p9(esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88))))))&(((((r1(esk1_0,esk40_0)|~epred13_1(esk1_0)|(~p8(esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(~p9(esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88))))&((p9(esk40_0)|~epred13_1(esk1_0)|(~p8(esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(~p9(esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88))))&(~r1(esk40_0,X93)|p9(X93)|~epred13_1(esk1_0)|(~p8(esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(~p9(esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88))))))&(~p8(esk40_0)|~epred13_1(esk1_0)|(~p8(esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(~p9(esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88)))))&(~p9(esk40_0)|~epred13_1(esk1_0)|(~p8(esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(~p9(esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88)))))&(((p8(esk40_0)|~epred13_1(esk1_0)|(~p8(esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(~p9(esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88))))&(~r1(esk40_0,X94)|p8(X94)|~epred13_1(esk1_0)|(~p8(esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(~p9(esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88)))))&(p8(esk40_0)|~epred13_1(esk1_0)|(~p8(esk39_1(X90))|~p8(X90)|~p8(X90)|(~r1(esk1_0,X90)|p9(X90))|(~p9(esk38_1(X88))|~p9(X88)|~r1(esk1_0,X88)|p8(X88)))))))))&(((((((r1(esk1_0,esk43_0)|~epred14_1(esk1_0)|(r1(X97,esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(r1(X95,esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95))))&((p8(esk43_0)|~epred14_1(esk1_0)|(r1(X97,esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(r1(X95,esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95))))&(~r1(esk43_0,X100)|p8(X100)|~epred14_1(esk1_0)|(r1(X97,esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(r1(X95,esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95))))))&(~p7(esk43_0)|~epred14_1(esk1_0)|(r1(X97,esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(r1(X95,esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95)))))&(~p8(esk43_0)|~epred14_1(esk1_0)|(r1(X97,esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(r1(X95,esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95)))))&(((p7(esk43_0)|~epred14_1(esk1_0)|(r1(X97,esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(r1(X95,esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95))))&(~r1(esk43_0,X101)|p7(X101)|~epred14_1(esk1_0)|(r1(X97,esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(r1(X95,esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95)))))&(p7(esk43_0)|~epred14_1(esk1_0)|(r1(X97,esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(r1(X95,esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95))))))&(((((r1(esk1_0,esk43_0)|~epred14_1(esk1_0)|(~p7(esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(r1(X95,esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95))))&((p8(esk43_0)|~epred14_1(esk1_0)|(~p7(esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(r1(X95,esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95))))&(~r1(esk43_0,X100)|p8(X100)|~epred14_1(esk1_0)|(~p7(esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(r1(X95,esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95))))))&(~p7(esk43_0)|~epred14_1(esk1_0)|(~p7(esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(r1(X95,esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95)))))&(~p8(esk43_0)|~epred14_1(esk1_0)|(~p7(esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(r1(X95,esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95)))))&(((p7(esk43_0)|~epred14_1(esk1_0)|(~p7(esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(r1(X95,esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95))))&(~r1(esk43_0,X101)|p7(X101)|~epred14_1(esk1_0)|(~p7(esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(r1(X95,esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95)))))&(p7(esk43_0)|~epred14_1(esk1_0)|(~p7(esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(r1(X95,esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95)))))))&((((((r1(esk1_0,esk43_0)|~epred14_1(esk1_0)|(r1(X97,esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(~p8(esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95))))&((p8(esk43_0)|~epred14_1(esk1_0)|(r1(X97,esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(~p8(esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95))))&(~r1(esk43_0,X100)|p8(X100)|~epred14_1(esk1_0)|(r1(X97,esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(~p8(esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95))))))&(~p7(esk43_0)|~epred14_1(esk1_0)|(r1(X97,esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(~p8(esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95)))))&(~p8(esk43_0)|~epred14_1(esk1_0)|(r1(X97,esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(~p8(esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95)))))&(((p7(esk43_0)|~epred14_1(esk1_0)|(r1(X97,esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(~p8(esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95))))&(~r1(esk43_0,X101)|p7(X101)|~epred14_1(esk1_0)|(r1(X97,esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(~p8(esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95)))))&(p7(esk43_0)|~epred14_1(esk1_0)|(r1(X97,esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(~p8(esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95))))))&(((((r1(esk1_0,esk43_0)|~epred14_1(esk1_0)|(~p7(esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(~p8(esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95))))&((p8(esk43_0)|~epred14_1(esk1_0)|(~p7(esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(~p8(esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95))))&(~r1(esk43_0,X100)|p8(X100)|~epred14_1(esk1_0)|(~p7(esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(~p8(esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95))))))&(~p7(esk43_0)|~epred14_1(esk1_0)|(~p7(esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(~p8(esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95)))))&(~p8(esk43_0)|~epred14_1(esk1_0)|(~p7(esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(~p8(esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95)))))&(((p7(esk43_0)|~epred14_1(esk1_0)|(~p7(esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(~p8(esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95))))&(~r1(esk43_0,X101)|p7(X101)|~epred14_1(esk1_0)|(~p7(esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(~p8(esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95)))))&(p7(esk43_0)|~epred14_1(esk1_0)|(~p7(esk42_1(X97))|~p7(X97)|~p7(X97)|(~r1(esk1_0,X97)|p8(X97))|(~p8(esk41_1(X95))|~p8(X95)|~r1(esk1_0,X95)|p7(X95)))))))))&((r1(esk1_0,esk44_0)&~p20(esk44_0))&((~r1(esk44_0,X103)|p20(X103))&p20(esk44_0))))&((r1(esk1_0,esk45_0)&~p20(esk45_0))&((~r1(esk45_0,X105)|p20(X105))&p20(esk45_0))))&(((((((r1(esk1_0,esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(r1(X106,esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106))))&((p7(esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(r1(X106,esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106))))&(~r1(esk48_0,X111)|p7(X111)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(r1(X106,esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106))))))&(~p6(esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(r1(X106,esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106)))))&(~p7(esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(r1(X106,esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106)))))&(((p6(esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(r1(X106,esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106))))&(~r1(esk48_0,X112)|p6(X112)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(r1(X106,esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106)))))&(p6(esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(r1(X106,esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106))))))&(((((r1(esk1_0,esk48_0)|~epred15_1(esk1_0)|(~p6(esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(r1(X106,esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106))))&((p7(esk48_0)|~epred15_1(esk1_0)|(~p6(esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(r1(X106,esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106))))&(~r1(esk48_0,X111)|p7(X111)|~epred15_1(esk1_0)|(~p6(esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(r1(X106,esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106))))))&(~p6(esk48_0)|~epred15_1(esk1_0)|(~p6(esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(r1(X106,esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106)))))&(~p7(esk48_0)|~epred15_1(esk1_0)|(~p6(esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(r1(X106,esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106)))))&(((p6(esk48_0)|~epred15_1(esk1_0)|(~p6(esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(r1(X106,esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106))))&(~r1(esk48_0,X112)|p6(X112)|~epred15_1(esk1_0)|(~p6(esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(r1(X106,esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106)))))&(p6(esk48_0)|~epred15_1(esk1_0)|(~p6(esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(r1(X106,esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106)))))))&((((((r1(esk1_0,esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(~p7(esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106))))&((p7(esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(~p7(esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106))))&(~r1(esk48_0,X111)|p7(X111)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(~p7(esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106))))))&(~p6(esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(~p7(esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106)))))&(~p7(esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(~p7(esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106)))))&(((p6(esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(~p7(esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106))))&(~r1(esk48_0,X112)|p6(X112)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(~p7(esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106)))))&(p6(esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(~p7(esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106))))))&(((((r1(esk1_0,esk48_0)|~epred15_1(esk1_0)|(~p6(esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(~p7(esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106))))&((p7(esk48_0)|~epred15_1(esk1_0)|(~p6(esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(~p7(esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106))))&(~r1(esk48_0,X111)|p7(X111)|~epred15_1(esk1_0)|(~p6(esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(~p7(esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106))))))&(~p6(esk48_0)|~epred15_1(esk1_0)|(~p6(esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(~p7(esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106)))))&(~p7(esk48_0)|~epred15_1(esk1_0)|(~p6(esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(~p7(esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106)))))&(((p6(esk48_0)|~epred15_1(esk1_0)|(~p6(esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(~p7(esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106))))&(~r1(esk48_0,X112)|p6(X112)|~epred15_1(esk1_0)|(~p6(esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(~p7(esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106)))))&(p6(esk48_0)|~epred15_1(esk1_0)|(~p6(esk47_1(X108))|~p6(X108)|~p6(X108)|(~r1(esk1_0,X108)|p7(X108))|(~p7(esk46_1(X106))|~p7(X106)|~r1(esk1_0,X106)|p6(X106)))))))))&(((((((r1(esk1_0,esk51_0)|~epred16_1(esk1_0)|(r1(X115,esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(r1(X113,esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113))))&((p6(esk51_0)|~epred16_1(esk1_0)|(r1(X115,esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(r1(X113,esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113))))&(~r1(esk51_0,X118)|p6(X118)|~epred16_1(esk1_0)|(r1(X115,esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(r1(X113,esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113))))))&(~p5(esk51_0)|~epred16_1(esk1_0)|(r1(X115,esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(r1(X113,esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113)))))&(~p6(esk51_0)|~epred16_1(esk1_0)|(r1(X115,esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(r1(X113,esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113)))))&(((p5(esk51_0)|~epred16_1(esk1_0)|(r1(X115,esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(r1(X113,esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113))))&(~r1(esk51_0,X119)|p5(X119)|~epred16_1(esk1_0)|(r1(X115,esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(r1(X113,esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113)))))&(p5(esk51_0)|~epred16_1(esk1_0)|(r1(X115,esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(r1(X113,esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113))))))&(((((r1(esk1_0,esk51_0)|~epred16_1(esk1_0)|(~p5(esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(r1(X113,esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113))))&((p6(esk51_0)|~epred16_1(esk1_0)|(~p5(esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(r1(X113,esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113))))&(~r1(esk51_0,X118)|p6(X118)|~epred16_1(esk1_0)|(~p5(esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(r1(X113,esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113))))))&(~p5(esk51_0)|~epred16_1(esk1_0)|(~p5(esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(r1(X113,esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113)))))&(~p6(esk51_0)|~epred16_1(esk1_0)|(~p5(esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(r1(X113,esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113)))))&(((p5(esk51_0)|~epred16_1(esk1_0)|(~p5(esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(r1(X113,esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113))))&(~r1(esk51_0,X119)|p5(X119)|~epred16_1(esk1_0)|(~p5(esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(r1(X113,esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113)))))&(p5(esk51_0)|~epred16_1(esk1_0)|(~p5(esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(r1(X113,esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113)))))))&((((((r1(esk1_0,esk51_0)|~epred16_1(esk1_0)|(r1(X115,esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(~p6(esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113))))&((p6(esk51_0)|~epred16_1(esk1_0)|(r1(X115,esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(~p6(esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113))))&(~r1(esk51_0,X118)|p6(X118)|~epred16_1(esk1_0)|(r1(X115,esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(~p6(esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113))))))&(~p5(esk51_0)|~epred16_1(esk1_0)|(r1(X115,esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(~p6(esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113)))))&(~p6(esk51_0)|~epred16_1(esk1_0)|(r1(X115,esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(~p6(esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113)))))&(((p5(esk51_0)|~epred16_1(esk1_0)|(r1(X115,esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(~p6(esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113))))&(~r1(esk51_0,X119)|p5(X119)|~epred16_1(esk1_0)|(r1(X115,esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(~p6(esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113)))))&(p5(esk51_0)|~epred16_1(esk1_0)|(r1(X115,esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(~p6(esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113))))))&(((((r1(esk1_0,esk51_0)|~epred16_1(esk1_0)|(~p5(esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(~p6(esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113))))&((p6(esk51_0)|~epred16_1(esk1_0)|(~p5(esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(~p6(esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113))))&(~r1(esk51_0,X118)|p6(X118)|~epred16_1(esk1_0)|(~p5(esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(~p6(esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113))))))&(~p5(esk51_0)|~epred16_1(esk1_0)|(~p5(esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(~p6(esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113)))))&(~p6(esk51_0)|~epred16_1(esk1_0)|(~p5(esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(~p6(esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113)))))&(((p5(esk51_0)|~epred16_1(esk1_0)|(~p5(esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(~p6(esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113))))&(~r1(esk51_0,X119)|p5(X119)|~epred16_1(esk1_0)|(~p5(esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(~p6(esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113)))))&(p5(esk51_0)|~epred16_1(esk1_0)|(~p5(esk50_1(X115))|~p5(X115)|~p5(X115)|(~r1(esk1_0,X115)|p6(X115))|(~p6(esk49_1(X113))|~p6(X113)|~r1(esk1_0,X113)|p5(X113)))))))))&(((((((r1(esk1_0,esk54_0)|~epred17_1(esk1_0)|(r1(X122,esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(r1(X120,esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120))))&((p5(esk54_0)|~epred17_1(esk1_0)|(r1(X122,esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(r1(X120,esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120))))&(~r1(esk54_0,X125)|p5(X125)|~epred17_1(esk1_0)|(r1(X122,esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(r1(X120,esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120))))))&(~p4(esk54_0)|~epred17_1(esk1_0)|(r1(X122,esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(r1(X120,esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120)))))&(~p5(esk54_0)|~epred17_1(esk1_0)|(r1(X122,esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(r1(X120,esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120)))))&(((p4(esk54_0)|~epred17_1(esk1_0)|(r1(X122,esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(r1(X120,esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120))))&(~r1(esk54_0,X126)|p4(X126)|~epred17_1(esk1_0)|(r1(X122,esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(r1(X120,esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120)))))&(p4(esk54_0)|~epred17_1(esk1_0)|(r1(X122,esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(r1(X120,esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120))))))&(((((r1(esk1_0,esk54_0)|~epred17_1(esk1_0)|(~p4(esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(r1(X120,esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120))))&((p5(esk54_0)|~epred17_1(esk1_0)|(~p4(esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(r1(X120,esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120))))&(~r1(esk54_0,X125)|p5(X125)|~epred17_1(esk1_0)|(~p4(esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(r1(X120,esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120))))))&(~p4(esk54_0)|~epred17_1(esk1_0)|(~p4(esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(r1(X120,esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120)))))&(~p5(esk54_0)|~epred17_1(esk1_0)|(~p4(esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(r1(X120,esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120)))))&(((p4(esk54_0)|~epred17_1(esk1_0)|(~p4(esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(r1(X120,esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120))))&(~r1(esk54_0,X126)|p4(X126)|~epred17_1(esk1_0)|(~p4(esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(r1(X120,esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120)))))&(p4(esk54_0)|~epred17_1(esk1_0)|(~p4(esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(r1(X120,esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120)))))))&((((((r1(esk1_0,esk54_0)|~epred17_1(esk1_0)|(r1(X122,esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(~p5(esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120))))&((p5(esk54_0)|~epred17_1(esk1_0)|(r1(X122,esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(~p5(esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120))))&(~r1(esk54_0,X125)|p5(X125)|~epred17_1(esk1_0)|(r1(X122,esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(~p5(esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120))))))&(~p4(esk54_0)|~epred17_1(esk1_0)|(r1(X122,esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(~p5(esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120)))))&(~p5(esk54_0)|~epred17_1(esk1_0)|(r1(X122,esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(~p5(esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120)))))&(((p4(esk54_0)|~epred17_1(esk1_0)|(r1(X122,esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(~p5(esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120))))&(~r1(esk54_0,X126)|p4(X126)|~epred17_1(esk1_0)|(r1(X122,esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(~p5(esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120)))))&(p4(esk54_0)|~epred17_1(esk1_0)|(r1(X122,esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(~p5(esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120))))))&(((((r1(esk1_0,esk54_0)|~epred17_1(esk1_0)|(~p4(esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(~p5(esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120))))&((p5(esk54_0)|~epred17_1(esk1_0)|(~p4(esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(~p5(esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120))))&(~r1(esk54_0,X125)|p5(X125)|~epred17_1(esk1_0)|(~p4(esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(~p5(esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120))))))&(~p4(esk54_0)|~epred17_1(esk1_0)|(~p4(esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(~p5(esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120)))))&(~p5(esk54_0)|~epred17_1(esk1_0)|(~p4(esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(~p5(esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120)))))&(((p4(esk54_0)|~epred17_1(esk1_0)|(~p4(esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(~p5(esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120))))&(~r1(esk54_0,X126)|p4(X126)|~epred17_1(esk1_0)|(~p4(esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(~p5(esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120)))))&(p4(esk54_0)|~epred17_1(esk1_0)|(~p4(esk53_1(X122))|~p4(X122)|~p4(X122)|(~r1(esk1_0,X122)|p5(X122))|(~p5(esk52_1(X120))|~p5(X120)|~r1(esk1_0,X120)|p4(X120)))))))))&(((((((r1(esk1_0,esk57_0)|~epred18_1(esk1_0)|(r1(X129,esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(r1(X127,esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127))))&((p4(esk57_0)|~epred18_1(esk1_0)|(r1(X129,esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(r1(X127,esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127))))&(~r1(esk57_0,X132)|p4(X132)|~epred18_1(esk1_0)|(r1(X129,esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(r1(X127,esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127))))))&(~p3(esk57_0)|~epred18_1(esk1_0)|(r1(X129,esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(r1(X127,esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127)))))&(~p4(esk57_0)|~epred18_1(esk1_0)|(r1(X129,esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(r1(X127,esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127)))))&(((p3(esk57_0)|~epred18_1(esk1_0)|(r1(X129,esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(r1(X127,esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127))))&(~r1(esk57_0,X133)|p3(X133)|~epred18_1(esk1_0)|(r1(X129,esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(r1(X127,esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127)))))&(p3(esk57_0)|~epred18_1(esk1_0)|(r1(X129,esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(r1(X127,esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127))))))&(((((r1(esk1_0,esk57_0)|~epred18_1(esk1_0)|(~p3(esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(r1(X127,esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127))))&((p4(esk57_0)|~epred18_1(esk1_0)|(~p3(esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(r1(X127,esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127))))&(~r1(esk57_0,X132)|p4(X132)|~epred18_1(esk1_0)|(~p3(esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(r1(X127,esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127))))))&(~p3(esk57_0)|~epred18_1(esk1_0)|(~p3(esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(r1(X127,esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127)))))&(~p4(esk57_0)|~epred18_1(esk1_0)|(~p3(esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(r1(X127,esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127)))))&(((p3(esk57_0)|~epred18_1(esk1_0)|(~p3(esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(r1(X127,esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127))))&(~r1(esk57_0,X133)|p3(X133)|~epred18_1(esk1_0)|(~p3(esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(r1(X127,esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127)))))&(p3(esk57_0)|~epred18_1(esk1_0)|(~p3(esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(r1(X127,esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127)))))))&((((((r1(esk1_0,esk57_0)|~epred18_1(esk1_0)|(r1(X129,esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(~p4(esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127))))&((p4(esk57_0)|~epred18_1(esk1_0)|(r1(X129,esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(~p4(esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127))))&(~r1(esk57_0,X132)|p4(X132)|~epred18_1(esk1_0)|(r1(X129,esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(~p4(esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127))))))&(~p3(esk57_0)|~epred18_1(esk1_0)|(r1(X129,esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(~p4(esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127)))))&(~p4(esk57_0)|~epred18_1(esk1_0)|(r1(X129,esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(~p4(esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127)))))&(((p3(esk57_0)|~epred18_1(esk1_0)|(r1(X129,esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(~p4(esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127))))&(~r1(esk57_0,X133)|p3(X133)|~epred18_1(esk1_0)|(r1(X129,esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(~p4(esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127)))))&(p3(esk57_0)|~epred18_1(esk1_0)|(r1(X129,esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(~p4(esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127))))))&(((((r1(esk1_0,esk57_0)|~epred18_1(esk1_0)|(~p3(esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(~p4(esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127))))&((p4(esk57_0)|~epred18_1(esk1_0)|(~p3(esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(~p4(esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127))))&(~r1(esk57_0,X132)|p4(X132)|~epred18_1(esk1_0)|(~p3(esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(~p4(esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127))))))&(~p3(esk57_0)|~epred18_1(esk1_0)|(~p3(esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(~p4(esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127)))))&(~p4(esk57_0)|~epred18_1(esk1_0)|(~p3(esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(~p4(esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127)))))&(((p3(esk57_0)|~epred18_1(esk1_0)|(~p3(esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(~p4(esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127))))&(~r1(esk57_0,X133)|p3(X133)|~epred18_1(esk1_0)|(~p3(esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(~p4(esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127)))))&(p3(esk57_0)|~epred18_1(esk1_0)|(~p3(esk56_1(X129))|~p3(X129)|~p3(X129)|(~r1(esk1_0,X129)|p4(X129))|(~p4(esk55_1(X127))|~p4(X127)|~r1(esk1_0,X127)|p3(X127)))))))))&(((((((r1(esk1_0,esk60_0)|~epred19_1(esk1_0)|(r1(X136,esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(r1(X134,esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134))))&((p3(esk60_0)|~epred19_1(esk1_0)|(r1(X136,esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(r1(X134,esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134))))&(~r1(esk60_0,X139)|p3(X139)|~epred19_1(esk1_0)|(r1(X136,esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(r1(X134,esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134))))))&(~p2(esk60_0)|~epred19_1(esk1_0)|(r1(X136,esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(r1(X134,esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134)))))&(~p3(esk60_0)|~epred19_1(esk1_0)|(r1(X136,esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(r1(X134,esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134)))))&(((p2(esk60_0)|~epred19_1(esk1_0)|(r1(X136,esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(r1(X134,esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134))))&(~r1(esk60_0,X140)|p2(X140)|~epred19_1(esk1_0)|(r1(X136,esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(r1(X134,esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134)))))&(p2(esk60_0)|~epred19_1(esk1_0)|(r1(X136,esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(r1(X134,esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134))))))&(((((r1(esk1_0,esk60_0)|~epred19_1(esk1_0)|(~p2(esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(r1(X134,esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134))))&((p3(esk60_0)|~epred19_1(esk1_0)|(~p2(esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(r1(X134,esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134))))&(~r1(esk60_0,X139)|p3(X139)|~epred19_1(esk1_0)|(~p2(esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(r1(X134,esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134))))))&(~p2(esk60_0)|~epred19_1(esk1_0)|(~p2(esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(r1(X134,esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134)))))&(~p3(esk60_0)|~epred19_1(esk1_0)|(~p2(esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(r1(X134,esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134)))))&(((p2(esk60_0)|~epred19_1(esk1_0)|(~p2(esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(r1(X134,esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134))))&(~r1(esk60_0,X140)|p2(X140)|~epred19_1(esk1_0)|(~p2(esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(r1(X134,esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134)))))&(p2(esk60_0)|~epred19_1(esk1_0)|(~p2(esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(r1(X134,esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134)))))))&((((((r1(esk1_0,esk60_0)|~epred19_1(esk1_0)|(r1(X136,esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(~p3(esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134))))&((p3(esk60_0)|~epred19_1(esk1_0)|(r1(X136,esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(~p3(esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134))))&(~r1(esk60_0,X139)|p3(X139)|~epred19_1(esk1_0)|(r1(X136,esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(~p3(esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134))))))&(~p2(esk60_0)|~epred19_1(esk1_0)|(r1(X136,esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(~p3(esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134)))))&(~p3(esk60_0)|~epred19_1(esk1_0)|(r1(X136,esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(~p3(esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134)))))&(((p2(esk60_0)|~epred19_1(esk1_0)|(r1(X136,esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(~p3(esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134))))&(~r1(esk60_0,X140)|p2(X140)|~epred19_1(esk1_0)|(r1(X136,esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(~p3(esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134)))))&(p2(esk60_0)|~epred19_1(esk1_0)|(r1(X136,esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(~p3(esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134))))))&(((((r1(esk1_0,esk60_0)|~epred19_1(esk1_0)|(~p2(esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(~p3(esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134))))&((p3(esk60_0)|~epred19_1(esk1_0)|(~p2(esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(~p3(esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134))))&(~r1(esk60_0,X139)|p3(X139)|~epred19_1(esk1_0)|(~p2(esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(~p3(esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134))))))&(~p2(esk60_0)|~epred19_1(esk1_0)|(~p2(esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(~p3(esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134)))))&(~p3(esk60_0)|~epred19_1(esk1_0)|(~p2(esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(~p3(esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134)))))&(((p2(esk60_0)|~epred19_1(esk1_0)|(~p2(esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(~p3(esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134))))&(~r1(esk60_0,X140)|p2(X140)|~epred19_1(esk1_0)|(~p2(esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(~p3(esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134)))))&(p2(esk60_0)|~epred19_1(esk1_0)|(~p2(esk59_1(X136))|~p2(X136)|~p2(X136)|(~r1(esk1_0,X136)|p3(X136))|(~p3(esk58_1(X134))|~p3(X134)|~r1(esk1_0,X134)|p2(X134)))))))))&(((((((r1(esk1_0,esk63_0)|~epred20_1(esk1_0)|(r1(X143,esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(r1(X141,esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141))))&((p2(esk63_0)|~epred20_1(esk1_0)|(r1(X143,esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(r1(X141,esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141))))&(~r1(esk63_0,X146)|p2(X146)|~epred20_1(esk1_0)|(r1(X143,esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(r1(X141,esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141))))))&(~p1(esk63_0)|~epred20_1(esk1_0)|(r1(X143,esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(r1(X141,esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141)))))&(~p2(esk63_0)|~epred20_1(esk1_0)|(r1(X143,esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(r1(X141,esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141)))))&(((p1(esk63_0)|~epred20_1(esk1_0)|(r1(X143,esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(r1(X141,esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141))))&(~r1(esk63_0,X147)|p1(X147)|~epred20_1(esk1_0)|(r1(X143,esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(r1(X141,esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141)))))&(p1(esk63_0)|~epred20_1(esk1_0)|(r1(X143,esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(r1(X141,esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141))))))&(((((r1(esk1_0,esk63_0)|~epred20_1(esk1_0)|(~p1(esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(r1(X141,esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141))))&((p2(esk63_0)|~epred20_1(esk1_0)|(~p1(esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(r1(X141,esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141))))&(~r1(esk63_0,X146)|p2(X146)|~epred20_1(esk1_0)|(~p1(esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(r1(X141,esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141))))))&(~p1(esk63_0)|~epred20_1(esk1_0)|(~p1(esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(r1(X141,esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141)))))&(~p2(esk63_0)|~epred20_1(esk1_0)|(~p1(esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(r1(X141,esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141)))))&(((p1(esk63_0)|~epred20_1(esk1_0)|(~p1(esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(r1(X141,esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141))))&(~r1(esk63_0,X147)|p1(X147)|~epred20_1(esk1_0)|(~p1(esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(r1(X141,esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141)))))&(p1(esk63_0)|~epred20_1(esk1_0)|(~p1(esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(r1(X141,esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141)))))))&((((((r1(esk1_0,esk63_0)|~epred20_1(esk1_0)|(r1(X143,esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(~p2(esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141))))&((p2(esk63_0)|~epred20_1(esk1_0)|(r1(X143,esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(~p2(esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141))))&(~r1(esk63_0,X146)|p2(X146)|~epred20_1(esk1_0)|(r1(X143,esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(~p2(esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141))))))&(~p1(esk63_0)|~epred20_1(esk1_0)|(r1(X143,esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(~p2(esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141)))))&(~p2(esk63_0)|~epred20_1(esk1_0)|(r1(X143,esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(~p2(esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141)))))&(((p1(esk63_0)|~epred20_1(esk1_0)|(r1(X143,esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(~p2(esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141))))&(~r1(esk63_0,X147)|p1(X147)|~epred20_1(esk1_0)|(r1(X143,esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(~p2(esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141)))))&(p1(esk63_0)|~epred20_1(esk1_0)|(r1(X143,esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(~p2(esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141))))))&(((((r1(esk1_0,esk63_0)|~epred20_1(esk1_0)|(~p1(esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(~p2(esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141))))&((p2(esk63_0)|~epred20_1(esk1_0)|(~p1(esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(~p2(esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141))))&(~r1(esk63_0,X146)|p2(X146)|~epred20_1(esk1_0)|(~p1(esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(~p2(esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141))))))&(~p1(esk63_0)|~epred20_1(esk1_0)|(~p1(esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(~p2(esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141)))))&(~p2(esk63_0)|~epred20_1(esk1_0)|(~p1(esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(~p2(esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141)))))&(((p1(esk63_0)|~epred20_1(esk1_0)|(~p1(esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(~p2(esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141))))&(~r1(esk63_0,X147)|p1(X147)|~epred20_1(esk1_0)|(~p1(esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(~p2(esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141)))))&(p1(esk63_0)|~epred20_1(esk1_0)|(~p1(esk62_1(X143))|~p1(X143)|~p1(X143)|(~r1(esk1_0,X143)|p2(X143))|(~p2(esk61_1(X141))|~p2(X141)|~r1(esk1_0,X141)|p1(X141)))))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_21])])])])])])).
% 0.62/0.62 cnf(c_0_23, negated_conjecture, (~p20(esk44_0)), inference(split_conjunct,[status(thm)],[c_0_22])).
% 0.62/0.62 cnf(c_0_24, negated_conjecture, (p20(esk44_0)), inference(split_conjunct,[status(thm)],[c_0_22])).
% 0.62/0.62 cnf(c_0_25, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_23, c_0_24])]), ['proof']).
% 0.62/0.62 % SZS output end Proof
% 0.62/0.62 % User time : 0.057 s
% 0.62/0.62 % System time : 0.008 s
% 0.62/0.62 % Total time : 0.065 s
% 0.62/0.62 % User time : 0.062 s
% 0.62/0.62 % System time : 0.013 s
% 0.62/0.62 % Total time : 0.075 s
% 0.62/0.62
%------------------------------------------------------------------------------