%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL644+1.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 11:21:17 AM UTC 2026
% Result : Theorem 0.75s 0.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL644+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : java -jar mcs_scs.jar %d %s
% 0.06/0.34 % Computer : n001.cluster.edu
% 0.06/0.34 % Model : x86_64 x86_64
% 0.06/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.34 % Memory : 8046.5625MB
% 0.06/0.34 % OS : Linux 6.8.0-71-generic
% 0.06/0.34 % CPULimit : 300
% 0.06/0.34 % WCLimit : 300
% 0.06/0.34 % DateTime : Sat Sep 5 23:09:17 UTC 2026
% 0.06/0.34 % CPUTime :
% 0.24/0.46 start to proof:theBenchmark.p
% 0.75/0.57 % Version : CSI_E---1.1
% 0.75/0.57 % Problem : theBenchmark.p
% 0.75/0.57 % Proof found!
% 0.75/0.57 % SZS status Theorem for theBenchmark.p
% 0.75/0.57 % SZS output start Proof
% 0.75/0.57 fof(main, conjecture, ~(?[X1]:(~((~((![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))|~((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))|p15(X2)|~((![X1]:((~(r1(X2,X1))|p15(X1)))&p15(X2)))))|![X2]:((~(r1(X1,X2))|p15(X2)|~((![X1]:((~(r1(X2,X1))|p15(X1)))&p15(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.75/0.57 fof(c_0_1, plain, ![X1]:((epred1_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.75/0.57 fof(c_0_2, plain, ![X1]:((epred2_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.75/0.57 fof(c_0_3, plain, ![X1]:((epred3_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.75/0.57 fof(c_0_4, plain, ![X1]:((epred4_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.75/0.57 fof(c_0_5, plain, ![X1]:((epred5_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.75/0.57 fof(c_0_6, plain, ![X1]:((epred6_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.75/0.57 fof(c_0_7, plain, ![X1]:((epred7_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.75/0.57 fof(c_0_8, plain, ![X1]:((epred8_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.75/0.57 fof(c_0_9, plain, ![X1]:((epred9_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.75/0.57 fof(c_0_10, plain, ![X1]:((epred10_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.75/0.57 fof(c_0_11, plain, ![X1]:((epred11_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.75/0.57 fof(c_0_12, plain, ![X1]:((epred12_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.75/0.57 fof(c_0_13, plain, ![X1]:((epred13_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.75/0.57 fof(c_0_14, plain, ![X1]:((epred14_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.75/0.57 fof(c_0_15, plain, ![X1]:((epred15_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.75/0.57 fof(c_0_16, negated_conjecture, ~(~(?[X1]:(~((~((![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)))))|~((epred1_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)))))|~((epred2_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)))))|~((epred3_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)))))|~((epred4_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)))))|~((epred5_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)))))|~((epred6_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)))))|~((epred7_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)))))|~((epred8_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)))))|~((epred9_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)|~((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)))))|~((epred10_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)|p15(X2)|~((![X1]:((~r1(X2,X1)|p15(X1)))&p15(X2)))))|![X2]:((~r1(X1,X2)|p15(X2)|~((![X1]:((~r1(X2,X1)|p15(X1)))&p15(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)))))|~((epred11_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)))))|~((epred12_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)))))|~((epred13_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)))))|~((epred14_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)))))|~((epred15_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(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])]), c_0_1]), c_0_2]), c_0_3]), c_0_4]), c_0_5]), c_0_6]), c_0_7]), c_0_8]), c_0_9]), c_0_10]), c_0_11]), c_0_12]), c_0_13]), c_0_14]), c_0_15])).
% 0.75/0.57 fof(c_0_17, 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, X75, X77, X78, X80, X83, X84, X85, X87, X90, X91, X92, X94, X97, X98, X99, X101, X104, X105, X106, X108, X111, X112]:((((((((((((((((((((((((r1(esk1_0,esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(r1(X4,esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4))))&((p16(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(r1(X4,esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4))))&(~r1(esk4_0,X9)|p16(X9)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(r1(X4,esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4))))))&(~p15(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(r1(X4,esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4)))))&(~p16(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(r1(X4,esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4)))))&(((p15(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(r1(X4,esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4))))&(~r1(esk4_0,X10)|p15(X10)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(r1(X4,esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4)))))&(p15(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(r1(X4,esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4))))))&(((((r1(esk1_0,esk4_0)|~epred1_1(esk1_0)|(~p15(esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(r1(X4,esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4))))&((p16(esk4_0)|~epred1_1(esk1_0)|(~p15(esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(r1(X4,esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4))))&(~r1(esk4_0,X9)|p16(X9)|~epred1_1(esk1_0)|(~p15(esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(r1(X4,esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4))))))&(~p15(esk4_0)|~epred1_1(esk1_0)|(~p15(esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(r1(X4,esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4)))))&(~p16(esk4_0)|~epred1_1(esk1_0)|(~p15(esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(r1(X4,esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4)))))&(((p15(esk4_0)|~epred1_1(esk1_0)|(~p15(esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(r1(X4,esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4))))&(~r1(esk4_0,X10)|p15(X10)|~epred1_1(esk1_0)|(~p15(esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(r1(X4,esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4)))))&(p15(esk4_0)|~epred1_1(esk1_0)|(~p15(esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(r1(X4,esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4)))))))&((((((r1(esk1_0,esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(~p16(esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4))))&((p16(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(~p16(esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4))))&(~r1(esk4_0,X9)|p16(X9)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(~p16(esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4))))))&(~p15(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(~p16(esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4)))))&(~p16(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(~p16(esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4)))))&(((p15(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(~p16(esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4))))&(~r1(esk4_0,X10)|p15(X10)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(~p16(esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4)))))&(p15(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(~p16(esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4))))))&(((((r1(esk1_0,esk4_0)|~epred1_1(esk1_0)|(~p15(esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(~p16(esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4))))&((p16(esk4_0)|~epred1_1(esk1_0)|(~p15(esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(~p16(esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4))))&(~r1(esk4_0,X9)|p16(X9)|~epred1_1(esk1_0)|(~p15(esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(~p16(esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4))))))&(~p15(esk4_0)|~epred1_1(esk1_0)|(~p15(esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(~p16(esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4)))))&(~p16(esk4_0)|~epred1_1(esk1_0)|(~p15(esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(~p16(esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4)))))&(((p15(esk4_0)|~epred1_1(esk1_0)|(~p15(esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(~p16(esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4))))&(~r1(esk4_0,X10)|p15(X10)|~epred1_1(esk1_0)|(~p15(esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(~p16(esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4)))))&(p15(esk4_0)|~epred1_1(esk1_0)|(~p15(esk3_1(X6))|~p15(X6)|~p15(X6)|(~r1(esk1_0,X6)|p16(X6))|(~p16(esk2_1(X4))|~p16(X4)|~r1(esk1_0,X4)|p15(X4))))))))&(((((((r1(esk1_0,esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(r1(X11,esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11))))&((p15(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(r1(X11,esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11))))&(~r1(esk7_0,X16)|p15(X16)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(r1(X11,esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11))))))&(~p14(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(r1(X11,esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11)))))&(~p15(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(r1(X11,esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11)))))&(((p14(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(r1(X11,esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11))))&(~r1(esk7_0,X17)|p14(X17)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(r1(X11,esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11)))))&(p14(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(r1(X11,esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11))))))&(((((r1(esk1_0,esk7_0)|~epred2_1(esk1_0)|(~p14(esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(r1(X11,esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11))))&((p15(esk7_0)|~epred2_1(esk1_0)|(~p14(esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(r1(X11,esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11))))&(~r1(esk7_0,X16)|p15(X16)|~epred2_1(esk1_0)|(~p14(esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(r1(X11,esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11))))))&(~p14(esk7_0)|~epred2_1(esk1_0)|(~p14(esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(r1(X11,esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11)))))&(~p15(esk7_0)|~epred2_1(esk1_0)|(~p14(esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(r1(X11,esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11)))))&(((p14(esk7_0)|~epred2_1(esk1_0)|(~p14(esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(r1(X11,esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11))))&(~r1(esk7_0,X17)|p14(X17)|~epred2_1(esk1_0)|(~p14(esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(r1(X11,esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11)))))&(p14(esk7_0)|~epred2_1(esk1_0)|(~p14(esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(r1(X11,esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11)))))))&((((((r1(esk1_0,esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(~p15(esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11))))&((p15(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(~p15(esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11))))&(~r1(esk7_0,X16)|p15(X16)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(~p15(esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11))))))&(~p14(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(~p15(esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11)))))&(~p15(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(~p15(esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11)))))&(((p14(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(~p15(esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11))))&(~r1(esk7_0,X17)|p14(X17)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(~p15(esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11)))))&(p14(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(~p15(esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11))))))&(((((r1(esk1_0,esk7_0)|~epred2_1(esk1_0)|(~p14(esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(~p15(esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11))))&((p15(esk7_0)|~epred2_1(esk1_0)|(~p14(esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(~p15(esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11))))&(~r1(esk7_0,X16)|p15(X16)|~epred2_1(esk1_0)|(~p14(esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(~p15(esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11))))))&(~p14(esk7_0)|~epred2_1(esk1_0)|(~p14(esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(~p15(esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11)))))&(~p15(esk7_0)|~epred2_1(esk1_0)|(~p14(esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(~p15(esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11)))))&(((p14(esk7_0)|~epred2_1(esk1_0)|(~p14(esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(~p15(esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11))))&(~r1(esk7_0,X17)|p14(X17)|~epred2_1(esk1_0)|(~p14(esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(~p15(esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11)))))&(p14(esk7_0)|~epred2_1(esk1_0)|(~p14(esk6_1(X13))|~p14(X13)|~p14(X13)|(~r1(esk1_0,X13)|p15(X13))|(~p15(esk5_1(X11))|~p15(X11)|~r1(esk1_0,X11)|p14(X11)))))))))&(((((((r1(esk1_0,esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(r1(X18,esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18))))&((p14(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(r1(X18,esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18))))&(~r1(esk10_0,X23)|p14(X23)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(r1(X18,esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18))))))&(~p13(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(r1(X18,esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18)))))&(~p14(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(r1(X18,esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18)))))&(((p13(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(r1(X18,esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18))))&(~r1(esk10_0,X24)|p13(X24)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(r1(X18,esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18)))))&(p13(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(r1(X18,esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18))))))&(((((r1(esk1_0,esk10_0)|~epred3_1(esk1_0)|(~p13(esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(r1(X18,esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18))))&((p14(esk10_0)|~epred3_1(esk1_0)|(~p13(esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(r1(X18,esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18))))&(~r1(esk10_0,X23)|p14(X23)|~epred3_1(esk1_0)|(~p13(esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(r1(X18,esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18))))))&(~p13(esk10_0)|~epred3_1(esk1_0)|(~p13(esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(r1(X18,esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18)))))&(~p14(esk10_0)|~epred3_1(esk1_0)|(~p13(esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(r1(X18,esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18)))))&(((p13(esk10_0)|~epred3_1(esk1_0)|(~p13(esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(r1(X18,esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18))))&(~r1(esk10_0,X24)|p13(X24)|~epred3_1(esk1_0)|(~p13(esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(r1(X18,esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18)))))&(p13(esk10_0)|~epred3_1(esk1_0)|(~p13(esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(r1(X18,esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18)))))))&((((((r1(esk1_0,esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(~p14(esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18))))&((p14(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(~p14(esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18))))&(~r1(esk10_0,X23)|p14(X23)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(~p14(esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18))))))&(~p13(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(~p14(esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18)))))&(~p14(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(~p14(esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18)))))&(((p13(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(~p14(esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18))))&(~r1(esk10_0,X24)|p13(X24)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(~p14(esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18)))))&(p13(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(~p14(esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18))))))&(((((r1(esk1_0,esk10_0)|~epred3_1(esk1_0)|(~p13(esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(~p14(esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18))))&((p14(esk10_0)|~epred3_1(esk1_0)|(~p13(esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(~p14(esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18))))&(~r1(esk10_0,X23)|p14(X23)|~epred3_1(esk1_0)|(~p13(esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(~p14(esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18))))))&(~p13(esk10_0)|~epred3_1(esk1_0)|(~p13(esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(~p14(esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18)))))&(~p14(esk10_0)|~epred3_1(esk1_0)|(~p13(esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(~p14(esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18)))))&(((p13(esk10_0)|~epred3_1(esk1_0)|(~p13(esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(~p14(esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18))))&(~r1(esk10_0,X24)|p13(X24)|~epred3_1(esk1_0)|(~p13(esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(~p14(esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18)))))&(p13(esk10_0)|~epred3_1(esk1_0)|(~p13(esk9_1(X20))|~p13(X20)|~p13(X20)|(~r1(esk1_0,X20)|p14(X20))|(~p14(esk8_1(X18))|~p14(X18)|~r1(esk1_0,X18)|p13(X18)))))))))&(((((((r1(esk1_0,esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(r1(X25,esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25))))&((p13(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(r1(X25,esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25))))&(~r1(esk13_0,X30)|p13(X30)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(r1(X25,esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25))))))&(~p12(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(r1(X25,esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25)))))&(~p13(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(r1(X25,esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25)))))&(((p12(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(r1(X25,esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25))))&(~r1(esk13_0,X31)|p12(X31)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(r1(X25,esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25)))))&(p12(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(r1(X25,esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25))))))&(((((r1(esk1_0,esk13_0)|~epred4_1(esk1_0)|(~p12(esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(r1(X25,esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25))))&((p13(esk13_0)|~epred4_1(esk1_0)|(~p12(esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(r1(X25,esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25))))&(~r1(esk13_0,X30)|p13(X30)|~epred4_1(esk1_0)|(~p12(esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(r1(X25,esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25))))))&(~p12(esk13_0)|~epred4_1(esk1_0)|(~p12(esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(r1(X25,esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25)))))&(~p13(esk13_0)|~epred4_1(esk1_0)|(~p12(esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(r1(X25,esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25)))))&(((p12(esk13_0)|~epred4_1(esk1_0)|(~p12(esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(r1(X25,esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25))))&(~r1(esk13_0,X31)|p12(X31)|~epred4_1(esk1_0)|(~p12(esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(r1(X25,esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25)))))&(p12(esk13_0)|~epred4_1(esk1_0)|(~p12(esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(r1(X25,esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25)))))))&((((((r1(esk1_0,esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(~p13(esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25))))&((p13(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(~p13(esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25))))&(~r1(esk13_0,X30)|p13(X30)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(~p13(esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25))))))&(~p12(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(~p13(esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25)))))&(~p13(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(~p13(esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25)))))&(((p12(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(~p13(esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25))))&(~r1(esk13_0,X31)|p12(X31)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(~p13(esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25)))))&(p12(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(~p13(esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25))))))&(((((r1(esk1_0,esk13_0)|~epred4_1(esk1_0)|(~p12(esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(~p13(esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25))))&((p13(esk13_0)|~epred4_1(esk1_0)|(~p12(esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(~p13(esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25))))&(~r1(esk13_0,X30)|p13(X30)|~epred4_1(esk1_0)|(~p12(esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(~p13(esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25))))))&(~p12(esk13_0)|~epred4_1(esk1_0)|(~p12(esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(~p13(esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25)))))&(~p13(esk13_0)|~epred4_1(esk1_0)|(~p12(esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(~p13(esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25)))))&(((p12(esk13_0)|~epred4_1(esk1_0)|(~p12(esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(~p13(esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25))))&(~r1(esk13_0,X31)|p12(X31)|~epred4_1(esk1_0)|(~p12(esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(~p13(esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25)))))&(p12(esk13_0)|~epred4_1(esk1_0)|(~p12(esk12_1(X27))|~p12(X27)|~p12(X27)|(~r1(esk1_0,X27)|p13(X27))|(~p13(esk11_1(X25))|~p13(X25)|~r1(esk1_0,X25)|p12(X25)))))))))&(((((((r1(esk1_0,esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(r1(X32,esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32))))&((p12(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(r1(X32,esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32))))&(~r1(esk16_0,X37)|p12(X37)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(r1(X32,esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32))))))&(~p11(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(r1(X32,esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32)))))&(~p12(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(r1(X32,esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32)))))&(((p11(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(r1(X32,esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32))))&(~r1(esk16_0,X38)|p11(X38)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(r1(X32,esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32)))))&(p11(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(r1(X32,esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32))))))&(((((r1(esk1_0,esk16_0)|~epred5_1(esk1_0)|(~p11(esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(r1(X32,esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32))))&((p12(esk16_0)|~epred5_1(esk1_0)|(~p11(esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(r1(X32,esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32))))&(~r1(esk16_0,X37)|p12(X37)|~epred5_1(esk1_0)|(~p11(esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(r1(X32,esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32))))))&(~p11(esk16_0)|~epred5_1(esk1_0)|(~p11(esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(r1(X32,esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32)))))&(~p12(esk16_0)|~epred5_1(esk1_0)|(~p11(esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(r1(X32,esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32)))))&(((p11(esk16_0)|~epred5_1(esk1_0)|(~p11(esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(r1(X32,esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32))))&(~r1(esk16_0,X38)|p11(X38)|~epred5_1(esk1_0)|(~p11(esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(r1(X32,esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32)))))&(p11(esk16_0)|~epred5_1(esk1_0)|(~p11(esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(r1(X32,esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32)))))))&((((((r1(esk1_0,esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(~p12(esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32))))&((p12(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(~p12(esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32))))&(~r1(esk16_0,X37)|p12(X37)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(~p12(esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32))))))&(~p11(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(~p12(esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32)))))&(~p12(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(~p12(esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32)))))&(((p11(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(~p12(esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32))))&(~r1(esk16_0,X38)|p11(X38)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(~p12(esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32)))))&(p11(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(~p12(esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32))))))&(((((r1(esk1_0,esk16_0)|~epred5_1(esk1_0)|(~p11(esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(~p12(esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32))))&((p12(esk16_0)|~epred5_1(esk1_0)|(~p11(esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(~p12(esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32))))&(~r1(esk16_0,X37)|p12(X37)|~epred5_1(esk1_0)|(~p11(esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(~p12(esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32))))))&(~p11(esk16_0)|~epred5_1(esk1_0)|(~p11(esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(~p12(esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32)))))&(~p12(esk16_0)|~epred5_1(esk1_0)|(~p11(esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(~p12(esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32)))))&(((p11(esk16_0)|~epred5_1(esk1_0)|(~p11(esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(~p12(esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32))))&(~r1(esk16_0,X38)|p11(X38)|~epred5_1(esk1_0)|(~p11(esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(~p12(esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32)))))&(p11(esk16_0)|~epred5_1(esk1_0)|(~p11(esk15_1(X34))|~p11(X34)|~p11(X34)|(~r1(esk1_0,X34)|p12(X34))|(~p12(esk14_1(X32))|~p12(X32)|~r1(esk1_0,X32)|p11(X32)))))))))&(((((((r1(esk1_0,esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(r1(X39,esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39))))&((p11(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(r1(X39,esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39))))&(~r1(esk19_0,X44)|p11(X44)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(r1(X39,esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39))))))&(~p10(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(r1(X39,esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39)))))&(~p11(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(r1(X39,esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39)))))&(((p10(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(r1(X39,esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39))))&(~r1(esk19_0,X45)|p10(X45)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(r1(X39,esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39)))))&(p10(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(r1(X39,esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39))))))&(((((r1(esk1_0,esk19_0)|~epred6_1(esk1_0)|(~p10(esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(r1(X39,esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39))))&((p11(esk19_0)|~epred6_1(esk1_0)|(~p10(esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(r1(X39,esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39))))&(~r1(esk19_0,X44)|p11(X44)|~epred6_1(esk1_0)|(~p10(esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(r1(X39,esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39))))))&(~p10(esk19_0)|~epred6_1(esk1_0)|(~p10(esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(r1(X39,esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39)))))&(~p11(esk19_0)|~epred6_1(esk1_0)|(~p10(esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(r1(X39,esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39)))))&(((p10(esk19_0)|~epred6_1(esk1_0)|(~p10(esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(r1(X39,esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39))))&(~r1(esk19_0,X45)|p10(X45)|~epred6_1(esk1_0)|(~p10(esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(r1(X39,esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39)))))&(p10(esk19_0)|~epred6_1(esk1_0)|(~p10(esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(r1(X39,esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39)))))))&((((((r1(esk1_0,esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(~p11(esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39))))&((p11(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(~p11(esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39))))&(~r1(esk19_0,X44)|p11(X44)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(~p11(esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39))))))&(~p10(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(~p11(esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39)))))&(~p11(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(~p11(esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39)))))&(((p10(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(~p11(esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39))))&(~r1(esk19_0,X45)|p10(X45)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(~p11(esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39)))))&(p10(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(~p11(esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39))))))&(((((r1(esk1_0,esk19_0)|~epred6_1(esk1_0)|(~p10(esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(~p11(esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39))))&((p11(esk19_0)|~epred6_1(esk1_0)|(~p10(esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(~p11(esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39))))&(~r1(esk19_0,X44)|p11(X44)|~epred6_1(esk1_0)|(~p10(esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(~p11(esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39))))))&(~p10(esk19_0)|~epred6_1(esk1_0)|(~p10(esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(~p11(esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39)))))&(~p11(esk19_0)|~epred6_1(esk1_0)|(~p10(esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(~p11(esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39)))))&(((p10(esk19_0)|~epred6_1(esk1_0)|(~p10(esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(~p11(esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39))))&(~r1(esk19_0,X45)|p10(X45)|~epred6_1(esk1_0)|(~p10(esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(~p11(esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39)))))&(p10(esk19_0)|~epred6_1(esk1_0)|(~p10(esk18_1(X41))|~p10(X41)|~p10(X41)|(~r1(esk1_0,X41)|p11(X41))|(~p11(esk17_1(X39))|~p11(X39)|~r1(esk1_0,X39)|p10(X39)))))))))&(((((((r1(esk1_0,esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(r1(X46,esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46))))&((p10(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(r1(X46,esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46))))&(~r1(esk22_0,X51)|p10(X51)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(r1(X46,esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46))))))&(~p9(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(r1(X46,esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46)))))&(~p10(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(r1(X46,esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46)))))&(((p9(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(r1(X46,esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46))))&(~r1(esk22_0,X52)|p9(X52)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(r1(X46,esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46)))))&(p9(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(r1(X46,esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46))))))&(((((r1(esk1_0,esk22_0)|~epred7_1(esk1_0)|(~p9(esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(r1(X46,esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46))))&((p10(esk22_0)|~epred7_1(esk1_0)|(~p9(esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(r1(X46,esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46))))&(~r1(esk22_0,X51)|p10(X51)|~epred7_1(esk1_0)|(~p9(esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(r1(X46,esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46))))))&(~p9(esk22_0)|~epred7_1(esk1_0)|(~p9(esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(r1(X46,esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46)))))&(~p10(esk22_0)|~epred7_1(esk1_0)|(~p9(esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(r1(X46,esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46)))))&(((p9(esk22_0)|~epred7_1(esk1_0)|(~p9(esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(r1(X46,esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46))))&(~r1(esk22_0,X52)|p9(X52)|~epred7_1(esk1_0)|(~p9(esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(r1(X46,esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46)))))&(p9(esk22_0)|~epred7_1(esk1_0)|(~p9(esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(r1(X46,esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46)))))))&((((((r1(esk1_0,esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(~p10(esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46))))&((p10(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(~p10(esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46))))&(~r1(esk22_0,X51)|p10(X51)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(~p10(esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46))))))&(~p9(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(~p10(esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46)))))&(~p10(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(~p10(esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46)))))&(((p9(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(~p10(esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46))))&(~r1(esk22_0,X52)|p9(X52)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(~p10(esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46)))))&(p9(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(~p10(esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46))))))&(((((r1(esk1_0,esk22_0)|~epred7_1(esk1_0)|(~p9(esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(~p10(esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46))))&((p10(esk22_0)|~epred7_1(esk1_0)|(~p9(esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(~p10(esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46))))&(~r1(esk22_0,X51)|p10(X51)|~epred7_1(esk1_0)|(~p9(esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(~p10(esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46))))))&(~p9(esk22_0)|~epred7_1(esk1_0)|(~p9(esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(~p10(esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46)))))&(~p10(esk22_0)|~epred7_1(esk1_0)|(~p9(esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(~p10(esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46)))))&(((p9(esk22_0)|~epred7_1(esk1_0)|(~p9(esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(~p10(esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46))))&(~r1(esk22_0,X52)|p9(X52)|~epred7_1(esk1_0)|(~p9(esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(~p10(esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46)))))&(p9(esk22_0)|~epred7_1(esk1_0)|(~p9(esk21_1(X48))|~p9(X48)|~p9(X48)|(~r1(esk1_0,X48)|p10(X48))|(~p10(esk20_1(X46))|~p10(X46)|~r1(esk1_0,X46)|p9(X46)))))))))&(((((((r1(esk1_0,esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(r1(X53,esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53))))&((p9(esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(r1(X53,esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53))))&(~r1(esk25_0,X58)|p9(X58)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(r1(X53,esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53))))))&(~p8(esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(r1(X53,esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53)))))&(~p9(esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(r1(X53,esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53)))))&(((p8(esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(r1(X53,esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53))))&(~r1(esk25_0,X59)|p8(X59)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(r1(X53,esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53)))))&(p8(esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(r1(X53,esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53))))))&(((((r1(esk1_0,esk25_0)|~epred8_1(esk1_0)|(~p8(esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(r1(X53,esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53))))&((p9(esk25_0)|~epred8_1(esk1_0)|(~p8(esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(r1(X53,esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53))))&(~r1(esk25_0,X58)|p9(X58)|~epred8_1(esk1_0)|(~p8(esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(r1(X53,esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53))))))&(~p8(esk25_0)|~epred8_1(esk1_0)|(~p8(esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(r1(X53,esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53)))))&(~p9(esk25_0)|~epred8_1(esk1_0)|(~p8(esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(r1(X53,esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53)))))&(((p8(esk25_0)|~epred8_1(esk1_0)|(~p8(esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(r1(X53,esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53))))&(~r1(esk25_0,X59)|p8(X59)|~epred8_1(esk1_0)|(~p8(esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(r1(X53,esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53)))))&(p8(esk25_0)|~epred8_1(esk1_0)|(~p8(esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(r1(X53,esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53)))))))&((((((r1(esk1_0,esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(~p9(esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53))))&((p9(esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(~p9(esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53))))&(~r1(esk25_0,X58)|p9(X58)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(~p9(esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53))))))&(~p8(esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(~p9(esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53)))))&(~p9(esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(~p9(esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53)))))&(((p8(esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(~p9(esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53))))&(~r1(esk25_0,X59)|p8(X59)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(~p9(esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53)))))&(p8(esk25_0)|~epred8_1(esk1_0)|(r1(X55,esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(~p9(esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53))))))&(((((r1(esk1_0,esk25_0)|~epred8_1(esk1_0)|(~p8(esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(~p9(esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53))))&((p9(esk25_0)|~epred8_1(esk1_0)|(~p8(esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(~p9(esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53))))&(~r1(esk25_0,X58)|p9(X58)|~epred8_1(esk1_0)|(~p8(esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(~p9(esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53))))))&(~p8(esk25_0)|~epred8_1(esk1_0)|(~p8(esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(~p9(esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53)))))&(~p9(esk25_0)|~epred8_1(esk1_0)|(~p8(esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(~p9(esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53)))))&(((p8(esk25_0)|~epred8_1(esk1_0)|(~p8(esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(~p9(esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53))))&(~r1(esk25_0,X59)|p8(X59)|~epred8_1(esk1_0)|(~p8(esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(~p9(esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53)))))&(p8(esk25_0)|~epred8_1(esk1_0)|(~p8(esk24_1(X55))|~p8(X55)|~p8(X55)|(~r1(esk1_0,X55)|p9(X55))|(~p9(esk23_1(X53))|~p9(X53)|~r1(esk1_0,X53)|p8(X53)))))))))&(((((((r1(esk1_0,esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(r1(X60,esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60))))&((p8(esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(r1(X60,esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60))))&(~r1(esk28_0,X65)|p8(X65)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(r1(X60,esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60))))))&(~p7(esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(r1(X60,esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60)))))&(~p8(esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(r1(X60,esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60)))))&(((p7(esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(r1(X60,esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60))))&(~r1(esk28_0,X66)|p7(X66)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(r1(X60,esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60)))))&(p7(esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(r1(X60,esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60))))))&(((((r1(esk1_0,esk28_0)|~epred9_1(esk1_0)|(~p7(esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(r1(X60,esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60))))&((p8(esk28_0)|~epred9_1(esk1_0)|(~p7(esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(r1(X60,esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60))))&(~r1(esk28_0,X65)|p8(X65)|~epred9_1(esk1_0)|(~p7(esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(r1(X60,esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60))))))&(~p7(esk28_0)|~epred9_1(esk1_0)|(~p7(esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(r1(X60,esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60)))))&(~p8(esk28_0)|~epred9_1(esk1_0)|(~p7(esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(r1(X60,esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60)))))&(((p7(esk28_0)|~epred9_1(esk1_0)|(~p7(esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(r1(X60,esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60))))&(~r1(esk28_0,X66)|p7(X66)|~epred9_1(esk1_0)|(~p7(esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(r1(X60,esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60)))))&(p7(esk28_0)|~epred9_1(esk1_0)|(~p7(esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(r1(X60,esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60)))))))&((((((r1(esk1_0,esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(~p8(esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60))))&((p8(esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(~p8(esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60))))&(~r1(esk28_0,X65)|p8(X65)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(~p8(esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60))))))&(~p7(esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(~p8(esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60)))))&(~p8(esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(~p8(esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60)))))&(((p7(esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(~p8(esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60))))&(~r1(esk28_0,X66)|p7(X66)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(~p8(esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60)))))&(p7(esk28_0)|~epred9_1(esk1_0)|(r1(X62,esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(~p8(esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60))))))&(((((r1(esk1_0,esk28_0)|~epred9_1(esk1_0)|(~p7(esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(~p8(esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60))))&((p8(esk28_0)|~epred9_1(esk1_0)|(~p7(esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(~p8(esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60))))&(~r1(esk28_0,X65)|p8(X65)|~epred9_1(esk1_0)|(~p7(esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(~p8(esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60))))))&(~p7(esk28_0)|~epred9_1(esk1_0)|(~p7(esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(~p8(esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60)))))&(~p8(esk28_0)|~epred9_1(esk1_0)|(~p7(esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(~p8(esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60)))))&(((p7(esk28_0)|~epred9_1(esk1_0)|(~p7(esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(~p8(esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60))))&(~r1(esk28_0,X66)|p7(X66)|~epred9_1(esk1_0)|(~p7(esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(~p8(esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60)))))&(p7(esk28_0)|~epred9_1(esk1_0)|(~p7(esk27_1(X62))|~p7(X62)|~p7(X62)|(~r1(esk1_0,X62)|p8(X62))|(~p8(esk26_1(X60))|~p8(X60)|~r1(esk1_0,X60)|p7(X60)))))))))&(((((((r1(esk1_0,esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(r1(X67,esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67))))&((p7(esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(r1(X67,esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67))))&(~r1(esk31_0,X72)|p7(X72)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(r1(X67,esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67))))))&(~p6(esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(r1(X67,esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67)))))&(~p7(esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(r1(X67,esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67)))))&(((p6(esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(r1(X67,esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67))))&(~r1(esk31_0,X73)|p6(X73)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(r1(X67,esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67)))))&(p6(esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(r1(X67,esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67))))))&(((((r1(esk1_0,esk31_0)|~epred10_1(esk1_0)|(~p6(esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(r1(X67,esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67))))&((p7(esk31_0)|~epred10_1(esk1_0)|(~p6(esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(r1(X67,esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67))))&(~r1(esk31_0,X72)|p7(X72)|~epred10_1(esk1_0)|(~p6(esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(r1(X67,esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67))))))&(~p6(esk31_0)|~epred10_1(esk1_0)|(~p6(esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(r1(X67,esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67)))))&(~p7(esk31_0)|~epred10_1(esk1_0)|(~p6(esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(r1(X67,esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67)))))&(((p6(esk31_0)|~epred10_1(esk1_0)|(~p6(esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(r1(X67,esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67))))&(~r1(esk31_0,X73)|p6(X73)|~epred10_1(esk1_0)|(~p6(esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(r1(X67,esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67)))))&(p6(esk31_0)|~epred10_1(esk1_0)|(~p6(esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(r1(X67,esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67)))))))&((((((r1(esk1_0,esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(~p7(esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67))))&((p7(esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(~p7(esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67))))&(~r1(esk31_0,X72)|p7(X72)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(~p7(esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67))))))&(~p6(esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(~p7(esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67)))))&(~p7(esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(~p7(esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67)))))&(((p6(esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(~p7(esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67))))&(~r1(esk31_0,X73)|p6(X73)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(~p7(esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67)))))&(p6(esk31_0)|~epred10_1(esk1_0)|(r1(X69,esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(~p7(esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67))))))&(((((r1(esk1_0,esk31_0)|~epred10_1(esk1_0)|(~p6(esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(~p7(esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67))))&((p7(esk31_0)|~epred10_1(esk1_0)|(~p6(esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(~p7(esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67))))&(~r1(esk31_0,X72)|p7(X72)|~epred10_1(esk1_0)|(~p6(esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(~p7(esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67))))))&(~p6(esk31_0)|~epred10_1(esk1_0)|(~p6(esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(~p7(esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67)))))&(~p7(esk31_0)|~epred10_1(esk1_0)|(~p6(esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(~p7(esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67)))))&(((p6(esk31_0)|~epred10_1(esk1_0)|(~p6(esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(~p7(esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67))))&(~r1(esk31_0,X73)|p6(X73)|~epred10_1(esk1_0)|(~p6(esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(~p7(esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67)))))&(p6(esk31_0)|~epred10_1(esk1_0)|(~p6(esk30_1(X69))|~p6(X69)|~p6(X69)|(~r1(esk1_0,X69)|p7(X69))|(~p7(esk29_1(X67))|~p7(X67)|~r1(esk1_0,X67)|p6(X67)))))))))&((r1(esk1_0,esk32_0)&~p15(esk32_0))&((~r1(esk32_0,X75)|p15(X75))&p15(esk32_0))))&((r1(esk1_0,esk33_0)&~p15(esk33_0))&((~r1(esk33_0,X77)|p15(X77))&p15(esk33_0))))&(((((((r1(esk1_0,esk36_0)|~epred11_1(esk1_0)|(r1(X80,esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(r1(X78,esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78))))&((p6(esk36_0)|~epred11_1(esk1_0)|(r1(X80,esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(r1(X78,esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78))))&(~r1(esk36_0,X83)|p6(X83)|~epred11_1(esk1_0)|(r1(X80,esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(r1(X78,esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78))))))&(~p5(esk36_0)|~epred11_1(esk1_0)|(r1(X80,esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(r1(X78,esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78)))))&(~p6(esk36_0)|~epred11_1(esk1_0)|(r1(X80,esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(r1(X78,esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78)))))&(((p5(esk36_0)|~epred11_1(esk1_0)|(r1(X80,esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(r1(X78,esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78))))&(~r1(esk36_0,X84)|p5(X84)|~epred11_1(esk1_0)|(r1(X80,esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(r1(X78,esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78)))))&(p5(esk36_0)|~epred11_1(esk1_0)|(r1(X80,esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(r1(X78,esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78))))))&(((((r1(esk1_0,esk36_0)|~epred11_1(esk1_0)|(~p5(esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(r1(X78,esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78))))&((p6(esk36_0)|~epred11_1(esk1_0)|(~p5(esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(r1(X78,esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78))))&(~r1(esk36_0,X83)|p6(X83)|~epred11_1(esk1_0)|(~p5(esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(r1(X78,esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78))))))&(~p5(esk36_0)|~epred11_1(esk1_0)|(~p5(esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(r1(X78,esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78)))))&(~p6(esk36_0)|~epred11_1(esk1_0)|(~p5(esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(r1(X78,esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78)))))&(((p5(esk36_0)|~epred11_1(esk1_0)|(~p5(esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(r1(X78,esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78))))&(~r1(esk36_0,X84)|p5(X84)|~epred11_1(esk1_0)|(~p5(esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(r1(X78,esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78)))))&(p5(esk36_0)|~epred11_1(esk1_0)|(~p5(esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(r1(X78,esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78)))))))&((((((r1(esk1_0,esk36_0)|~epred11_1(esk1_0)|(r1(X80,esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(~p6(esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78))))&((p6(esk36_0)|~epred11_1(esk1_0)|(r1(X80,esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(~p6(esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78))))&(~r1(esk36_0,X83)|p6(X83)|~epred11_1(esk1_0)|(r1(X80,esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(~p6(esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78))))))&(~p5(esk36_0)|~epred11_1(esk1_0)|(r1(X80,esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(~p6(esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78)))))&(~p6(esk36_0)|~epred11_1(esk1_0)|(r1(X80,esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(~p6(esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78)))))&(((p5(esk36_0)|~epred11_1(esk1_0)|(r1(X80,esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(~p6(esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78))))&(~r1(esk36_0,X84)|p5(X84)|~epred11_1(esk1_0)|(r1(X80,esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(~p6(esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78)))))&(p5(esk36_0)|~epred11_1(esk1_0)|(r1(X80,esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(~p6(esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78))))))&(((((r1(esk1_0,esk36_0)|~epred11_1(esk1_0)|(~p5(esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(~p6(esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78))))&((p6(esk36_0)|~epred11_1(esk1_0)|(~p5(esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(~p6(esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78))))&(~r1(esk36_0,X83)|p6(X83)|~epred11_1(esk1_0)|(~p5(esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(~p6(esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78))))))&(~p5(esk36_0)|~epred11_1(esk1_0)|(~p5(esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(~p6(esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78)))))&(~p6(esk36_0)|~epred11_1(esk1_0)|(~p5(esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(~p6(esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78)))))&(((p5(esk36_0)|~epred11_1(esk1_0)|(~p5(esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(~p6(esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78))))&(~r1(esk36_0,X84)|p5(X84)|~epred11_1(esk1_0)|(~p5(esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(~p6(esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78)))))&(p5(esk36_0)|~epred11_1(esk1_0)|(~p5(esk35_1(X80))|~p5(X80)|~p5(X80)|(~r1(esk1_0,X80)|p6(X80))|(~p6(esk34_1(X78))|~p6(X78)|~r1(esk1_0,X78)|p5(X78)))))))))&(((((((r1(esk1_0,esk39_0)|~epred12_1(esk1_0)|(r1(X87,esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(r1(X85,esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85))))&((p5(esk39_0)|~epred12_1(esk1_0)|(r1(X87,esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(r1(X85,esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85))))&(~r1(esk39_0,X90)|p5(X90)|~epred12_1(esk1_0)|(r1(X87,esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(r1(X85,esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85))))))&(~p4(esk39_0)|~epred12_1(esk1_0)|(r1(X87,esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(r1(X85,esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85)))))&(~p5(esk39_0)|~epred12_1(esk1_0)|(r1(X87,esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(r1(X85,esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85)))))&(((p4(esk39_0)|~epred12_1(esk1_0)|(r1(X87,esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(r1(X85,esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85))))&(~r1(esk39_0,X91)|p4(X91)|~epred12_1(esk1_0)|(r1(X87,esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(r1(X85,esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85)))))&(p4(esk39_0)|~epred12_1(esk1_0)|(r1(X87,esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(r1(X85,esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85))))))&(((((r1(esk1_0,esk39_0)|~epred12_1(esk1_0)|(~p4(esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(r1(X85,esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85))))&((p5(esk39_0)|~epred12_1(esk1_0)|(~p4(esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(r1(X85,esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85))))&(~r1(esk39_0,X90)|p5(X90)|~epred12_1(esk1_0)|(~p4(esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(r1(X85,esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85))))))&(~p4(esk39_0)|~epred12_1(esk1_0)|(~p4(esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(r1(X85,esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85)))))&(~p5(esk39_0)|~epred12_1(esk1_0)|(~p4(esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(r1(X85,esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85)))))&(((p4(esk39_0)|~epred12_1(esk1_0)|(~p4(esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(r1(X85,esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85))))&(~r1(esk39_0,X91)|p4(X91)|~epred12_1(esk1_0)|(~p4(esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(r1(X85,esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85)))))&(p4(esk39_0)|~epred12_1(esk1_0)|(~p4(esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(r1(X85,esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85)))))))&((((((r1(esk1_0,esk39_0)|~epred12_1(esk1_0)|(r1(X87,esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(~p5(esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85))))&((p5(esk39_0)|~epred12_1(esk1_0)|(r1(X87,esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(~p5(esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85))))&(~r1(esk39_0,X90)|p5(X90)|~epred12_1(esk1_0)|(r1(X87,esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(~p5(esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85))))))&(~p4(esk39_0)|~epred12_1(esk1_0)|(r1(X87,esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(~p5(esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85)))))&(~p5(esk39_0)|~epred12_1(esk1_0)|(r1(X87,esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(~p5(esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85)))))&(((p4(esk39_0)|~epred12_1(esk1_0)|(r1(X87,esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(~p5(esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85))))&(~r1(esk39_0,X91)|p4(X91)|~epred12_1(esk1_0)|(r1(X87,esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(~p5(esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85)))))&(p4(esk39_0)|~epred12_1(esk1_0)|(r1(X87,esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(~p5(esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85))))))&(((((r1(esk1_0,esk39_0)|~epred12_1(esk1_0)|(~p4(esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(~p5(esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85))))&((p5(esk39_0)|~epred12_1(esk1_0)|(~p4(esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(~p5(esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85))))&(~r1(esk39_0,X90)|p5(X90)|~epred12_1(esk1_0)|(~p4(esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(~p5(esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85))))))&(~p4(esk39_0)|~epred12_1(esk1_0)|(~p4(esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(~p5(esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85)))))&(~p5(esk39_0)|~epred12_1(esk1_0)|(~p4(esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(~p5(esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85)))))&(((p4(esk39_0)|~epred12_1(esk1_0)|(~p4(esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(~p5(esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85))))&(~r1(esk39_0,X91)|p4(X91)|~epred12_1(esk1_0)|(~p4(esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(~p5(esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85)))))&(p4(esk39_0)|~epred12_1(esk1_0)|(~p4(esk38_1(X87))|~p4(X87)|~p4(X87)|(~r1(esk1_0,X87)|p5(X87))|(~p5(esk37_1(X85))|~p5(X85)|~r1(esk1_0,X85)|p4(X85)))))))))&(((((((r1(esk1_0,esk42_0)|~epred13_1(esk1_0)|(r1(X94,esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(r1(X92,esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92))))&((p4(esk42_0)|~epred13_1(esk1_0)|(r1(X94,esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(r1(X92,esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92))))&(~r1(esk42_0,X97)|p4(X97)|~epred13_1(esk1_0)|(r1(X94,esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(r1(X92,esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92))))))&(~p3(esk42_0)|~epred13_1(esk1_0)|(r1(X94,esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(r1(X92,esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92)))))&(~p4(esk42_0)|~epred13_1(esk1_0)|(r1(X94,esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(r1(X92,esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92)))))&(((p3(esk42_0)|~epred13_1(esk1_0)|(r1(X94,esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(r1(X92,esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92))))&(~r1(esk42_0,X98)|p3(X98)|~epred13_1(esk1_0)|(r1(X94,esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(r1(X92,esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92)))))&(p3(esk42_0)|~epred13_1(esk1_0)|(r1(X94,esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(r1(X92,esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92))))))&(((((r1(esk1_0,esk42_0)|~epred13_1(esk1_0)|(~p3(esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(r1(X92,esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92))))&((p4(esk42_0)|~epred13_1(esk1_0)|(~p3(esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(r1(X92,esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92))))&(~r1(esk42_0,X97)|p4(X97)|~epred13_1(esk1_0)|(~p3(esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(r1(X92,esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92))))))&(~p3(esk42_0)|~epred13_1(esk1_0)|(~p3(esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(r1(X92,esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92)))))&(~p4(esk42_0)|~epred13_1(esk1_0)|(~p3(esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(r1(X92,esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92)))))&(((p3(esk42_0)|~epred13_1(esk1_0)|(~p3(esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(r1(X92,esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92))))&(~r1(esk42_0,X98)|p3(X98)|~epred13_1(esk1_0)|(~p3(esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(r1(X92,esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92)))))&(p3(esk42_0)|~epred13_1(esk1_0)|(~p3(esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(r1(X92,esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92)))))))&((((((r1(esk1_0,esk42_0)|~epred13_1(esk1_0)|(r1(X94,esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(~p4(esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92))))&((p4(esk42_0)|~epred13_1(esk1_0)|(r1(X94,esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(~p4(esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92))))&(~r1(esk42_0,X97)|p4(X97)|~epred13_1(esk1_0)|(r1(X94,esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(~p4(esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92))))))&(~p3(esk42_0)|~epred13_1(esk1_0)|(r1(X94,esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(~p4(esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92)))))&(~p4(esk42_0)|~epred13_1(esk1_0)|(r1(X94,esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(~p4(esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92)))))&(((p3(esk42_0)|~epred13_1(esk1_0)|(r1(X94,esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(~p4(esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92))))&(~r1(esk42_0,X98)|p3(X98)|~epred13_1(esk1_0)|(r1(X94,esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(~p4(esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92)))))&(p3(esk42_0)|~epred13_1(esk1_0)|(r1(X94,esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(~p4(esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92))))))&(((((r1(esk1_0,esk42_0)|~epred13_1(esk1_0)|(~p3(esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(~p4(esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92))))&((p4(esk42_0)|~epred13_1(esk1_0)|(~p3(esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(~p4(esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92))))&(~r1(esk42_0,X97)|p4(X97)|~epred13_1(esk1_0)|(~p3(esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(~p4(esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92))))))&(~p3(esk42_0)|~epred13_1(esk1_0)|(~p3(esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(~p4(esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92)))))&(~p4(esk42_0)|~epred13_1(esk1_0)|(~p3(esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(~p4(esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92)))))&(((p3(esk42_0)|~epred13_1(esk1_0)|(~p3(esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(~p4(esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92))))&(~r1(esk42_0,X98)|p3(X98)|~epred13_1(esk1_0)|(~p3(esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(~p4(esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92)))))&(p3(esk42_0)|~epred13_1(esk1_0)|(~p3(esk41_1(X94))|~p3(X94)|~p3(X94)|(~r1(esk1_0,X94)|p4(X94))|(~p4(esk40_1(X92))|~p4(X92)|~r1(esk1_0,X92)|p3(X92)))))))))&(((((((r1(esk1_0,esk45_0)|~epred14_1(esk1_0)|(r1(X101,esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(r1(X99,esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99))))&((p3(esk45_0)|~epred14_1(esk1_0)|(r1(X101,esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(r1(X99,esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99))))&(~r1(esk45_0,X104)|p3(X104)|~epred14_1(esk1_0)|(r1(X101,esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(r1(X99,esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99))))))&(~p2(esk45_0)|~epred14_1(esk1_0)|(r1(X101,esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(r1(X99,esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99)))))&(~p3(esk45_0)|~epred14_1(esk1_0)|(r1(X101,esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(r1(X99,esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99)))))&(((p2(esk45_0)|~epred14_1(esk1_0)|(r1(X101,esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(r1(X99,esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99))))&(~r1(esk45_0,X105)|p2(X105)|~epred14_1(esk1_0)|(r1(X101,esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(r1(X99,esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99)))))&(p2(esk45_0)|~epred14_1(esk1_0)|(r1(X101,esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(r1(X99,esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99))))))&(((((r1(esk1_0,esk45_0)|~epred14_1(esk1_0)|(~p2(esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(r1(X99,esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99))))&((p3(esk45_0)|~epred14_1(esk1_0)|(~p2(esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(r1(X99,esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99))))&(~r1(esk45_0,X104)|p3(X104)|~epred14_1(esk1_0)|(~p2(esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(r1(X99,esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99))))))&(~p2(esk45_0)|~epred14_1(esk1_0)|(~p2(esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(r1(X99,esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99)))))&(~p3(esk45_0)|~epred14_1(esk1_0)|(~p2(esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(r1(X99,esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99)))))&(((p2(esk45_0)|~epred14_1(esk1_0)|(~p2(esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(r1(X99,esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99))))&(~r1(esk45_0,X105)|p2(X105)|~epred14_1(esk1_0)|(~p2(esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(r1(X99,esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99)))))&(p2(esk45_0)|~epred14_1(esk1_0)|(~p2(esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(r1(X99,esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99)))))))&((((((r1(esk1_0,esk45_0)|~epred14_1(esk1_0)|(r1(X101,esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(~p3(esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99))))&((p3(esk45_0)|~epred14_1(esk1_0)|(r1(X101,esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(~p3(esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99))))&(~r1(esk45_0,X104)|p3(X104)|~epred14_1(esk1_0)|(r1(X101,esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(~p3(esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99))))))&(~p2(esk45_0)|~epred14_1(esk1_0)|(r1(X101,esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(~p3(esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99)))))&(~p3(esk45_0)|~epred14_1(esk1_0)|(r1(X101,esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(~p3(esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99)))))&(((p2(esk45_0)|~epred14_1(esk1_0)|(r1(X101,esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(~p3(esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99))))&(~r1(esk45_0,X105)|p2(X105)|~epred14_1(esk1_0)|(r1(X101,esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(~p3(esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99)))))&(p2(esk45_0)|~epred14_1(esk1_0)|(r1(X101,esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(~p3(esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99))))))&(((((r1(esk1_0,esk45_0)|~epred14_1(esk1_0)|(~p2(esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(~p3(esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99))))&((p3(esk45_0)|~epred14_1(esk1_0)|(~p2(esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(~p3(esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99))))&(~r1(esk45_0,X104)|p3(X104)|~epred14_1(esk1_0)|(~p2(esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(~p3(esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99))))))&(~p2(esk45_0)|~epred14_1(esk1_0)|(~p2(esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(~p3(esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99)))))&(~p3(esk45_0)|~epred14_1(esk1_0)|(~p2(esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(~p3(esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99)))))&(((p2(esk45_0)|~epred14_1(esk1_0)|(~p2(esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(~p3(esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99))))&(~r1(esk45_0,X105)|p2(X105)|~epred14_1(esk1_0)|(~p2(esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(~p3(esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99)))))&(p2(esk45_0)|~epred14_1(esk1_0)|(~p2(esk44_1(X101))|~p2(X101)|~p2(X101)|(~r1(esk1_0,X101)|p3(X101))|(~p3(esk43_1(X99))|~p3(X99)|~r1(esk1_0,X99)|p2(X99)))))))))&(((((((r1(esk1_0,esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(r1(X106,esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106))))&((p2(esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(r1(X106,esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106))))&(~r1(esk48_0,X111)|p2(X111)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(r1(X106,esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106))))))&(~p1(esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(r1(X106,esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106)))))&(~p2(esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(r1(X106,esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106)))))&(((p1(esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(r1(X106,esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106))))&(~r1(esk48_0,X112)|p1(X112)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(r1(X106,esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106)))))&(p1(esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(r1(X106,esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106))))))&(((((r1(esk1_0,esk48_0)|~epred15_1(esk1_0)|(~p1(esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(r1(X106,esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106))))&((p2(esk48_0)|~epred15_1(esk1_0)|(~p1(esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(r1(X106,esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106))))&(~r1(esk48_0,X111)|p2(X111)|~epred15_1(esk1_0)|(~p1(esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(r1(X106,esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106))))))&(~p1(esk48_0)|~epred15_1(esk1_0)|(~p1(esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(r1(X106,esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106)))))&(~p2(esk48_0)|~epred15_1(esk1_0)|(~p1(esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(r1(X106,esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106)))))&(((p1(esk48_0)|~epred15_1(esk1_0)|(~p1(esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(r1(X106,esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106))))&(~r1(esk48_0,X112)|p1(X112)|~epred15_1(esk1_0)|(~p1(esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(r1(X106,esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106)))))&(p1(esk48_0)|~epred15_1(esk1_0)|(~p1(esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(r1(X106,esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106)))))))&((((((r1(esk1_0,esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(~p2(esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106))))&((p2(esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(~p2(esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106))))&(~r1(esk48_0,X111)|p2(X111)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(~p2(esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106))))))&(~p1(esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(~p2(esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106)))))&(~p2(esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(~p2(esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106)))))&(((p1(esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(~p2(esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106))))&(~r1(esk48_0,X112)|p1(X112)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(~p2(esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106)))))&(p1(esk48_0)|~epred15_1(esk1_0)|(r1(X108,esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(~p2(esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106))))))&(((((r1(esk1_0,esk48_0)|~epred15_1(esk1_0)|(~p1(esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(~p2(esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106))))&((p2(esk48_0)|~epred15_1(esk1_0)|(~p1(esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(~p2(esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106))))&(~r1(esk48_0,X111)|p2(X111)|~epred15_1(esk1_0)|(~p1(esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(~p2(esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106))))))&(~p1(esk48_0)|~epred15_1(esk1_0)|(~p1(esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(~p2(esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106)))))&(~p2(esk48_0)|~epred15_1(esk1_0)|(~p1(esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(~p2(esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106)))))&(((p1(esk48_0)|~epred15_1(esk1_0)|(~p1(esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(~p2(esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106))))&(~r1(esk48_0,X112)|p1(X112)|~epred15_1(esk1_0)|(~p1(esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(~p2(esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106)))))&(p1(esk48_0)|~epred15_1(esk1_0)|(~p1(esk47_1(X108))|~p1(X108)|~p1(X108)|(~r1(esk1_0,X108)|p2(X108))|(~p2(esk46_1(X106))|~p2(X106)|~r1(esk1_0,X106)|p1(X106)))))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_16])])])])])])).
% 0.75/0.57 cnf(c_0_18, negated_conjecture, (~p15(esk32_0)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.75/0.57 cnf(c_0_19, negated_conjecture, (p15(esk32_0)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.75/0.57 cnf(c_0_20, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_18, c_0_19])]), ['proof']).
% 0.75/0.57 % SZS output end Proof
% 0.75/0.57 % User time : 0.035 s
% 0.75/0.57 % System time : 0.011 s
% 0.75/0.57 % Total time : 0.046 s
% 0.75/0.57 % User time : 0.038 s
% 0.75/0.57 % System time : 0.013 s
% 0.75/0.57 % Total time : 0.051 s
% 0.75/0.57
%------------------------------------------------------------------------------