%------------------------------------------------------------------------------
% File : Etableau---0.67
% Problem : LCL644+1.020 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s
% Computer : n015.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 12:01:33 PM UTC 2026
% Result : Theorem 0.21s 0.49s
% 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.04 % Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s
% 0.09/0.36 % Computer : n015.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 5 09:56:57 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.21/0.49 # No SInE strategy applied
% 0.21/0.49 # Auto-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S5PRR_RG_S04AN
% 0.21/0.49 # and selection function SelectComplexExceptUniqMaxHorn.
% 0.21/0.49 #
% 0.21/0.49 # Presaturation interreduction done
% 0.21/0.49
% 0.21/0.49 # Proof found!
% 0.21/0.49 # SZS status Theorem
% 0.21/0.49 # SZS output start CNFRefutation
% 0.21/0.49 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/sandbox/benchmark/theBenchmark.p', main)).
% 0.21/0.49 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.21/0.49 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.21/0.49 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.21/0.49 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.21/0.49 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.21/0.49 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.21/0.49 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.21/0.49 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.21/0.49 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.21/0.49 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.21/0.49 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.21/0.49 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.21/0.49 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.21/0.49 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.21/0.49 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.21/0.49 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.21/0.49 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.21/0.49 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.21/0.49 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.21/0.49 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.21/0.49 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(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.21/0.49 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(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_21])])])])])])).
% 0.21/0.50 cnf(c_0_23, negated_conjecture, (~p20(esk44_0)), inference(split_conjunct,[status(thm)],[c_0_22])).
% 0.21/0.50 cnf(c_0_24, negated_conjecture, (p20(esk44_0)), inference(split_conjunct,[status(thm)],[c_0_22])).
% 0.21/0.50 cnf(c_0_25, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_23, c_0_24])]), ['proof']).
% 0.21/0.50 # SZS output end CNFRefutation
% 0.21/0.50 # Training examples: 0 positive, 0 negative
%------------------------------------------------------------------------------