%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL644+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n005.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 1.05s 285.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL644+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.34 % Computer : n005.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Fri Sep 4 13:07:21 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.13/0.46 start to proof:theBenchmark.p
% 1.05/285.50 % Version : CSI_E---1.1
% 1.05/285.50 % Problem : theBenchmark.p
% 1.05/285.50 % Proof found!
% 1.05/285.50 % SZS status Theorem for theBenchmark.p
% 1.05/285.50 % SZS output start Proof
% 1.05/285.50 fof(main, conjecture, ~(?[X1]:(~((~((![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))|~((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))|p10(X2)|~((![X1]:((~(r1(X2,X1))|p10(X1)))&p10(X2)))))|![X2]:((~(r1(X1,X2))|p10(X2)|~((![X1]:((~(r1(X2,X1))|p10(X1)))&p10(X2)))))|~((![X2]:((~(r1(X1,X2))|~((p4(X2)&![X1]:((~(r1(X2,X1))|p4(X1)))))|p3(X2)))|![X2]:((~(r1(X1,X2))|p4(X2)|~(((p3(X2)&![X1]:((~(r1(X2,X1))|p3(X1))))&p3(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p4(X1)&![X2]:((~(r1(X1,X2))|p4(X2)))))|p3(X1)))|p4(X2)|~(((p3(X2)&![X1]:((~(r1(X2,X1))|p3(X1))))&p3(X2)))))&![X2]:((~(r1(X1,X2))|~((p4(X2)&![X1]:((~(r1(X2,X1))|p4(X1)))))|p3(X2)|![X1]:((~(r1(X2,X1))|p4(X1)|~(((p3(X1)&![X2]:((~(r1(X1,X2))|p3(X2))))&p3(X1))))))))&![X2]:((~(r1(X1,X2))|~((p4(X2)&![X1]:((~(r1(X2,X1))|p4(X1)))))|p3(X2)|p4(X2)|~(((p3(X2)&![X1]:((~(r1(X2,X1))|p3(X1))))&p3(X2)))))))))|~((![X2]:((~(r1(X1,X2))|~((p3(X2)&![X1]:((~(r1(X2,X1))|p3(X1)))))|p2(X2)))|![X2]:((~(r1(X1,X2))|p3(X2)|~(((p2(X2)&![X1]:((~(r1(X2,X1))|p2(X1))))&p2(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p3(X1)&![X2]:((~(r1(X1,X2))|p3(X2)))))|p2(X1)))|p3(X2)|~(((p2(X2)&![X1]:((~(r1(X2,X1))|p2(X1))))&p2(X2)))))&![X2]:((~(r1(X1,X2))|~((p3(X2)&![X1]:((~(r1(X2,X1))|p3(X1)))))|p2(X2)|![X1]:((~(r1(X2,X1))|p3(X1)|~(((p2(X1)&![X2]:((~(r1(X1,X2))|p2(X2))))&p2(X1))))))))&![X2]:((~(r1(X1,X2))|~((p3(X2)&![X1]:((~(r1(X2,X1))|p3(X1)))))|p2(X2)|p3(X2)|~(((p2(X2)&![X1]:((~(r1(X2,X1))|p2(X1))))&p2(X2)))))))))|~((![X2]:((~(r1(X1,X2))|~((p2(X2)&![X1]:((~(r1(X2,X1))|p2(X1)))))|p1(X2)))|![X2]:((~(r1(X1,X2))|p2(X2)|~(((p1(X2)&![X1]:((~(r1(X2,X1))|p1(X1))))&p1(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p2(X1)&![X2]:((~(r1(X1,X2))|p2(X2)))))|p1(X1)))|p2(X2)|~(((p1(X2)&![X1]:((~(r1(X2,X1))|p1(X1))))&p1(X2)))))&![X2]:((~(r1(X1,X2))|~((p2(X2)&![X1]:((~(r1(X2,X1))|p2(X1)))))|p1(X2)|![X1]:((~(r1(X2,X1))|p2(X1)|~(((p1(X1)&![X2]:((~(r1(X1,X2))|p1(X2))))&p1(X1))))))))&![X2]:((~(r1(X1,X2))|~((p2(X2)&![X1]:((~(r1(X2,X1))|p2(X1)))))|p1(X2)|p2(X2)|~(((p1(X2)&![X1]:((~(r1(X2,X1))|p1(X1))))&p1(X2))))))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', main)).
% 1.05/285.50 fof(c_0_1, plain, ![X1]:((epred1_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)).
% 1.05/285.50 fof(c_0_2, plain, ![X1]:((epred2_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)).
% 1.05/285.50 fof(c_0_3, plain, ![X1]:((epred3_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)).
% 1.05/285.50 fof(c_0_4, plain, ![X1]:((epred4_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)).
% 1.05/285.50 fof(c_0_5, plain, ![X1]:((epred5_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)).
% 1.05/285.50 fof(c_0_6, plain, ![X1]:((epred6_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)).
% 1.05/285.50 fof(c_0_7, plain, ![X1]:((epred7_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)).
% 1.05/285.50 fof(c_0_8, plain, ![X1]:((epred8_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)).
% 1.05/285.50 fof(c_0_9, plain, ![X1]:((epred9_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)).
% 1.05/285.50 fof(c_0_10, plain, ![X1]:((epred10_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)).
% 1.05/285.50 fof(c_0_11, negated_conjecture, ~(~(?[X1]:(~((~((![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)))))|~((epred1_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)))))|~((epred2_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)))))|~((epred3_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)))))|~((epred4_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)))))|~((epred5_1(X1)&![X2]:((~r1(X1,X2)|~((p7(X2)&![X1]:((~r1(X2,X1)|p7(X1)))))|p6(X2)|p7(X2)|~(((p6(X2)&![X1]:((~r1(X2,X1)|p6(X1))))&p6(X2)))))))))|~((![X2]:((~r1(X1,X2)|~((p6(X2)&![X1]:((~r1(X2,X1)|p6(X1)))))|p5(X2)))|![X2]:((~r1(X1,X2)|p6(X2)|~(((p5(X2)&![X1]:((~r1(X2,X1)|p5(X1))))&p5(X2)))))|~((epred6_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)))))|~((epred7_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)|p10(X2)|~((![X1]:((~r1(X2,X1)|p10(X1)))&p10(X2)))))|![X2]:((~r1(X1,X2)|p10(X2)|~((![X1]:((~r1(X2,X1)|p10(X1)))&p10(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)))))|~((epred8_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)))))|~((epred9_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)))))|~((epred10_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(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])).
% 1.05/285.50 fof(c_0_12, 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, X54, X56, X57, X59, X62, X63, X64, X66, X69, X70, X71, X73, X76, X77]:(((((((((((((((((((r1(esk1_0,esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(r1(X4,esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4))))&((p11(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(r1(X4,esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4))))&(~r1(esk4_0,X9)|p11(X9)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(r1(X4,esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4))))))&(~p10(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(r1(X4,esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4)))))&(~p11(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(r1(X4,esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4)))))&(((p10(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(r1(X4,esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4))))&(~r1(esk4_0,X10)|p10(X10)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(r1(X4,esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4)))))&(p10(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(r1(X4,esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4))))))&(((((r1(esk1_0,esk4_0)|~epred1_1(esk1_0)|(~p10(esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(r1(X4,esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4))))&((p11(esk4_0)|~epred1_1(esk1_0)|(~p10(esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(r1(X4,esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4))))&(~r1(esk4_0,X9)|p11(X9)|~epred1_1(esk1_0)|(~p10(esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(r1(X4,esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4))))))&(~p10(esk4_0)|~epred1_1(esk1_0)|(~p10(esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(r1(X4,esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4)))))&(~p11(esk4_0)|~epred1_1(esk1_0)|(~p10(esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(r1(X4,esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4)))))&(((p10(esk4_0)|~epred1_1(esk1_0)|(~p10(esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(r1(X4,esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4))))&(~r1(esk4_0,X10)|p10(X10)|~epred1_1(esk1_0)|(~p10(esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(r1(X4,esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4)))))&(p10(esk4_0)|~epred1_1(esk1_0)|(~p10(esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(r1(X4,esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4)))))))&((((((r1(esk1_0,esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(~p11(esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4))))&((p11(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(~p11(esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4))))&(~r1(esk4_0,X9)|p11(X9)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(~p11(esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4))))))&(~p10(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(~p11(esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4)))))&(~p11(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(~p11(esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4)))))&(((p10(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(~p11(esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4))))&(~r1(esk4_0,X10)|p10(X10)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(~p11(esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4)))))&(p10(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(~p11(esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4))))))&(((((r1(esk1_0,esk4_0)|~epred1_1(esk1_0)|(~p10(esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(~p11(esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4))))&((p11(esk4_0)|~epred1_1(esk1_0)|(~p10(esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(~p11(esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4))))&(~r1(esk4_0,X9)|p11(X9)|~epred1_1(esk1_0)|(~p10(esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(~p11(esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4))))))&(~p10(esk4_0)|~epred1_1(esk1_0)|(~p10(esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(~p11(esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4)))))&(~p11(esk4_0)|~epred1_1(esk1_0)|(~p10(esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(~p11(esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4)))))&(((p10(esk4_0)|~epred1_1(esk1_0)|(~p10(esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(~p11(esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4))))&(~r1(esk4_0,X10)|p10(X10)|~epred1_1(esk1_0)|(~p10(esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(~p11(esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4)))))&(p10(esk4_0)|~epred1_1(esk1_0)|(~p10(esk3_1(X6))|~p10(X6)|~p10(X6)|(~r1(esk1_0,X6)|p11(X6))|(~p11(esk2_1(X4))|~p11(X4)|~r1(esk1_0,X4)|p10(X4))))))))&(((((((r1(esk1_0,esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(r1(X11,esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11))))&((p10(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(r1(X11,esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11))))&(~r1(esk7_0,X16)|p10(X16)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(r1(X11,esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11))))))&(~p9(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(r1(X11,esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11)))))&(~p10(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(r1(X11,esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11)))))&(((p9(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(r1(X11,esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11))))&(~r1(esk7_0,X17)|p9(X17)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(r1(X11,esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11)))))&(p9(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(r1(X11,esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11))))))&(((((r1(esk1_0,esk7_0)|~epred2_1(esk1_0)|(~p9(esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(r1(X11,esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11))))&((p10(esk7_0)|~epred2_1(esk1_0)|(~p9(esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(r1(X11,esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11))))&(~r1(esk7_0,X16)|p10(X16)|~epred2_1(esk1_0)|(~p9(esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(r1(X11,esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11))))))&(~p9(esk7_0)|~epred2_1(esk1_0)|(~p9(esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(r1(X11,esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11)))))&(~p10(esk7_0)|~epred2_1(esk1_0)|(~p9(esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(r1(X11,esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11)))))&(((p9(esk7_0)|~epred2_1(esk1_0)|(~p9(esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(r1(X11,esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11))))&(~r1(esk7_0,X17)|p9(X17)|~epred2_1(esk1_0)|(~p9(esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(r1(X11,esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11)))))&(p9(esk7_0)|~epred2_1(esk1_0)|(~p9(esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(r1(X11,esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11)))))))&((((((r1(esk1_0,esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(~p10(esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11))))&((p10(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(~p10(esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11))))&(~r1(esk7_0,X16)|p10(X16)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(~p10(esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11))))))&(~p9(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(~p10(esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11)))))&(~p10(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(~p10(esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11)))))&(((p9(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(~p10(esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11))))&(~r1(esk7_0,X17)|p9(X17)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(~p10(esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11)))))&(p9(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(~p10(esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11))))))&(((((r1(esk1_0,esk7_0)|~epred2_1(esk1_0)|(~p9(esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(~p10(esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11))))&((p10(esk7_0)|~epred2_1(esk1_0)|(~p9(esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(~p10(esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11))))&(~r1(esk7_0,X16)|p10(X16)|~epred2_1(esk1_0)|(~p9(esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(~p10(esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11))))))&(~p9(esk7_0)|~epred2_1(esk1_0)|(~p9(esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(~p10(esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11)))))&(~p10(esk7_0)|~epred2_1(esk1_0)|(~p9(esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(~p10(esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11)))))&(((p9(esk7_0)|~epred2_1(esk1_0)|(~p9(esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(~p10(esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11))))&(~r1(esk7_0,X17)|p9(X17)|~epred2_1(esk1_0)|(~p9(esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(~p10(esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11)))))&(p9(esk7_0)|~epred2_1(esk1_0)|(~p9(esk6_1(X13))|~p9(X13)|~p9(X13)|(~r1(esk1_0,X13)|p10(X13))|(~p10(esk5_1(X11))|~p10(X11)|~r1(esk1_0,X11)|p9(X11)))))))))&(((((((r1(esk1_0,esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(r1(X18,esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18))))&((p9(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(r1(X18,esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18))))&(~r1(esk10_0,X23)|p9(X23)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(r1(X18,esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18))))))&(~p8(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(r1(X18,esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18)))))&(~p9(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(r1(X18,esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18)))))&(((p8(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(r1(X18,esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18))))&(~r1(esk10_0,X24)|p8(X24)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(r1(X18,esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18)))))&(p8(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(r1(X18,esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18))))))&(((((r1(esk1_0,esk10_0)|~epred3_1(esk1_0)|(~p8(esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(r1(X18,esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18))))&((p9(esk10_0)|~epred3_1(esk1_0)|(~p8(esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(r1(X18,esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18))))&(~r1(esk10_0,X23)|p9(X23)|~epred3_1(esk1_0)|(~p8(esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(r1(X18,esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18))))))&(~p8(esk10_0)|~epred3_1(esk1_0)|(~p8(esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(r1(X18,esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18)))))&(~p9(esk10_0)|~epred3_1(esk1_0)|(~p8(esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(r1(X18,esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18)))))&(((p8(esk10_0)|~epred3_1(esk1_0)|(~p8(esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(r1(X18,esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18))))&(~r1(esk10_0,X24)|p8(X24)|~epred3_1(esk1_0)|(~p8(esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(r1(X18,esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18)))))&(p8(esk10_0)|~epred3_1(esk1_0)|(~p8(esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(r1(X18,esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18)))))))&((((((r1(esk1_0,esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(~p9(esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18))))&((p9(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(~p9(esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18))))&(~r1(esk10_0,X23)|p9(X23)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(~p9(esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18))))))&(~p8(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(~p9(esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18)))))&(~p9(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(~p9(esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18)))))&(((p8(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(~p9(esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18))))&(~r1(esk10_0,X24)|p8(X24)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(~p9(esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18)))))&(p8(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(~p9(esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18))))))&(((((r1(esk1_0,esk10_0)|~epred3_1(esk1_0)|(~p8(esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(~p9(esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18))))&((p9(esk10_0)|~epred3_1(esk1_0)|(~p8(esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(~p9(esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18))))&(~r1(esk10_0,X23)|p9(X23)|~epred3_1(esk1_0)|(~p8(esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(~p9(esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18))))))&(~p8(esk10_0)|~epred3_1(esk1_0)|(~p8(esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(~p9(esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18)))))&(~p9(esk10_0)|~epred3_1(esk1_0)|(~p8(esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(~p9(esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18)))))&(((p8(esk10_0)|~epred3_1(esk1_0)|(~p8(esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(~p9(esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18))))&(~r1(esk10_0,X24)|p8(X24)|~epred3_1(esk1_0)|(~p8(esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(~p9(esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18)))))&(p8(esk10_0)|~epred3_1(esk1_0)|(~p8(esk9_1(X20))|~p8(X20)|~p8(X20)|(~r1(esk1_0,X20)|p9(X20))|(~p9(esk8_1(X18))|~p9(X18)|~r1(esk1_0,X18)|p8(X18)))))))))&(((((((r1(esk1_0,esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(r1(X25,esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25))))&((p8(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(r1(X25,esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25))))&(~r1(esk13_0,X30)|p8(X30)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(r1(X25,esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25))))))&(~p7(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(r1(X25,esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25)))))&(~p8(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(r1(X25,esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25)))))&(((p7(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(r1(X25,esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25))))&(~r1(esk13_0,X31)|p7(X31)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(r1(X25,esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25)))))&(p7(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(r1(X25,esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25))))))&(((((r1(esk1_0,esk13_0)|~epred4_1(esk1_0)|(~p7(esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(r1(X25,esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25))))&((p8(esk13_0)|~epred4_1(esk1_0)|(~p7(esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(r1(X25,esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25))))&(~r1(esk13_0,X30)|p8(X30)|~epred4_1(esk1_0)|(~p7(esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(r1(X25,esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25))))))&(~p7(esk13_0)|~epred4_1(esk1_0)|(~p7(esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(r1(X25,esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25)))))&(~p8(esk13_0)|~epred4_1(esk1_0)|(~p7(esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(r1(X25,esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25)))))&(((p7(esk13_0)|~epred4_1(esk1_0)|(~p7(esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(r1(X25,esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25))))&(~r1(esk13_0,X31)|p7(X31)|~epred4_1(esk1_0)|(~p7(esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(r1(X25,esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25)))))&(p7(esk13_0)|~epred4_1(esk1_0)|(~p7(esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(r1(X25,esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25)))))))&((((((r1(esk1_0,esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(~p8(esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25))))&((p8(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(~p8(esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25))))&(~r1(esk13_0,X30)|p8(X30)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(~p8(esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25))))))&(~p7(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(~p8(esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25)))))&(~p8(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(~p8(esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25)))))&(((p7(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(~p8(esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25))))&(~r1(esk13_0,X31)|p7(X31)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(~p8(esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25)))))&(p7(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(~p8(esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25))))))&(((((r1(esk1_0,esk13_0)|~epred4_1(esk1_0)|(~p7(esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(~p8(esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25))))&((p8(esk13_0)|~epred4_1(esk1_0)|(~p7(esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(~p8(esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25))))&(~r1(esk13_0,X30)|p8(X30)|~epred4_1(esk1_0)|(~p7(esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(~p8(esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25))))))&(~p7(esk13_0)|~epred4_1(esk1_0)|(~p7(esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(~p8(esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25)))))&(~p8(esk13_0)|~epred4_1(esk1_0)|(~p7(esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(~p8(esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25)))))&(((p7(esk13_0)|~epred4_1(esk1_0)|(~p7(esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(~p8(esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25))))&(~r1(esk13_0,X31)|p7(X31)|~epred4_1(esk1_0)|(~p7(esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(~p8(esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25)))))&(p7(esk13_0)|~epred4_1(esk1_0)|(~p7(esk12_1(X27))|~p7(X27)|~p7(X27)|(~r1(esk1_0,X27)|p8(X27))|(~p8(esk11_1(X25))|~p8(X25)|~r1(esk1_0,X25)|p7(X25)))))))))&(((((((r1(esk1_0,esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(r1(X32,esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32))))&((p7(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(r1(X32,esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32))))&(~r1(esk16_0,X37)|p7(X37)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(r1(X32,esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32))))))&(~p6(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(r1(X32,esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32)))))&(~p7(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(r1(X32,esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32)))))&(((p6(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(r1(X32,esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32))))&(~r1(esk16_0,X38)|p6(X38)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(r1(X32,esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32)))))&(p6(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(r1(X32,esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32))))))&(((((r1(esk1_0,esk16_0)|~epred5_1(esk1_0)|(~p6(esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(r1(X32,esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32))))&((p7(esk16_0)|~epred5_1(esk1_0)|(~p6(esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(r1(X32,esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32))))&(~r1(esk16_0,X37)|p7(X37)|~epred5_1(esk1_0)|(~p6(esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(r1(X32,esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32))))))&(~p6(esk16_0)|~epred5_1(esk1_0)|(~p6(esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(r1(X32,esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32)))))&(~p7(esk16_0)|~epred5_1(esk1_0)|(~p6(esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(r1(X32,esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32)))))&(((p6(esk16_0)|~epred5_1(esk1_0)|(~p6(esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(r1(X32,esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32))))&(~r1(esk16_0,X38)|p6(X38)|~epred5_1(esk1_0)|(~p6(esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(r1(X32,esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32)))))&(p6(esk16_0)|~epred5_1(esk1_0)|(~p6(esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(r1(X32,esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32)))))))&((((((r1(esk1_0,esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(~p7(esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32))))&((p7(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(~p7(esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32))))&(~r1(esk16_0,X37)|p7(X37)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(~p7(esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32))))))&(~p6(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(~p7(esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32)))))&(~p7(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(~p7(esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32)))))&(((p6(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(~p7(esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32))))&(~r1(esk16_0,X38)|p6(X38)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(~p7(esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32)))))&(p6(esk16_0)|~epred5_1(esk1_0)|(r1(X34,esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(~p7(esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32))))))&(((((r1(esk1_0,esk16_0)|~epred5_1(esk1_0)|(~p6(esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(~p7(esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32))))&((p7(esk16_0)|~epred5_1(esk1_0)|(~p6(esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(~p7(esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32))))&(~r1(esk16_0,X37)|p7(X37)|~epred5_1(esk1_0)|(~p6(esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(~p7(esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32))))))&(~p6(esk16_0)|~epred5_1(esk1_0)|(~p6(esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(~p7(esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32)))))&(~p7(esk16_0)|~epred5_1(esk1_0)|(~p6(esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(~p7(esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32)))))&(((p6(esk16_0)|~epred5_1(esk1_0)|(~p6(esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(~p7(esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32))))&(~r1(esk16_0,X38)|p6(X38)|~epred5_1(esk1_0)|(~p6(esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(~p7(esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32)))))&(p6(esk16_0)|~epred5_1(esk1_0)|(~p6(esk15_1(X34))|~p6(X34)|~p6(X34)|(~r1(esk1_0,X34)|p7(X34))|(~p7(esk14_1(X32))|~p7(X32)|~r1(esk1_0,X32)|p6(X32)))))))))&(((((((r1(esk1_0,esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(r1(X39,esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39))))&((p6(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(r1(X39,esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39))))&(~r1(esk19_0,X44)|p6(X44)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(r1(X39,esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39))))))&(~p5(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(r1(X39,esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39)))))&(~p6(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(r1(X39,esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39)))))&(((p5(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(r1(X39,esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39))))&(~r1(esk19_0,X45)|p5(X45)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(r1(X39,esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39)))))&(p5(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(r1(X39,esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39))))))&(((((r1(esk1_0,esk19_0)|~epred6_1(esk1_0)|(~p5(esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(r1(X39,esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39))))&((p6(esk19_0)|~epred6_1(esk1_0)|(~p5(esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(r1(X39,esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39))))&(~r1(esk19_0,X44)|p6(X44)|~epred6_1(esk1_0)|(~p5(esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(r1(X39,esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39))))))&(~p5(esk19_0)|~epred6_1(esk1_0)|(~p5(esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(r1(X39,esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39)))))&(~p6(esk19_0)|~epred6_1(esk1_0)|(~p5(esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(r1(X39,esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39)))))&(((p5(esk19_0)|~epred6_1(esk1_0)|(~p5(esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(r1(X39,esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39))))&(~r1(esk19_0,X45)|p5(X45)|~epred6_1(esk1_0)|(~p5(esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(r1(X39,esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39)))))&(p5(esk19_0)|~epred6_1(esk1_0)|(~p5(esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(r1(X39,esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39)))))))&((((((r1(esk1_0,esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(~p6(esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39))))&((p6(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(~p6(esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39))))&(~r1(esk19_0,X44)|p6(X44)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(~p6(esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39))))))&(~p5(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(~p6(esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39)))))&(~p6(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(~p6(esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39)))))&(((p5(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(~p6(esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39))))&(~r1(esk19_0,X45)|p5(X45)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(~p6(esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39)))))&(p5(esk19_0)|~epred6_1(esk1_0)|(r1(X41,esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(~p6(esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39))))))&(((((r1(esk1_0,esk19_0)|~epred6_1(esk1_0)|(~p5(esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(~p6(esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39))))&((p6(esk19_0)|~epred6_1(esk1_0)|(~p5(esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(~p6(esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39))))&(~r1(esk19_0,X44)|p6(X44)|~epred6_1(esk1_0)|(~p5(esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(~p6(esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39))))))&(~p5(esk19_0)|~epred6_1(esk1_0)|(~p5(esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(~p6(esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39)))))&(~p6(esk19_0)|~epred6_1(esk1_0)|(~p5(esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(~p6(esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39)))))&(((p5(esk19_0)|~epred6_1(esk1_0)|(~p5(esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(~p6(esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39))))&(~r1(esk19_0,X45)|p5(X45)|~epred6_1(esk1_0)|(~p5(esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(~p6(esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39)))))&(p5(esk19_0)|~epred6_1(esk1_0)|(~p5(esk18_1(X41))|~p5(X41)|~p5(X41)|(~r1(esk1_0,X41)|p6(X41))|(~p6(esk17_1(X39))|~p6(X39)|~r1(esk1_0,X39)|p5(X39)))))))))&(((((((r1(esk1_0,esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(r1(X46,esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46))))&((p5(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(r1(X46,esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46))))&(~r1(esk22_0,X51)|p5(X51)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(r1(X46,esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46))))))&(~p4(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(r1(X46,esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46)))))&(~p5(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(r1(X46,esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46)))))&(((p4(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(r1(X46,esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46))))&(~r1(esk22_0,X52)|p4(X52)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(r1(X46,esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46)))))&(p4(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(r1(X46,esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46))))))&(((((r1(esk1_0,esk22_0)|~epred7_1(esk1_0)|(~p4(esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(r1(X46,esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46))))&((p5(esk22_0)|~epred7_1(esk1_0)|(~p4(esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(r1(X46,esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46))))&(~r1(esk22_0,X51)|p5(X51)|~epred7_1(esk1_0)|(~p4(esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(r1(X46,esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46))))))&(~p4(esk22_0)|~epred7_1(esk1_0)|(~p4(esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(r1(X46,esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46)))))&(~p5(esk22_0)|~epred7_1(esk1_0)|(~p4(esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(r1(X46,esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46)))))&(((p4(esk22_0)|~epred7_1(esk1_0)|(~p4(esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(r1(X46,esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46))))&(~r1(esk22_0,X52)|p4(X52)|~epred7_1(esk1_0)|(~p4(esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(r1(X46,esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46)))))&(p4(esk22_0)|~epred7_1(esk1_0)|(~p4(esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(r1(X46,esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46)))))))&((((((r1(esk1_0,esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(~p5(esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46))))&((p5(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(~p5(esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46))))&(~r1(esk22_0,X51)|p5(X51)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(~p5(esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46))))))&(~p4(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(~p5(esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46)))))&(~p5(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(~p5(esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46)))))&(((p4(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(~p5(esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46))))&(~r1(esk22_0,X52)|p4(X52)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(~p5(esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46)))))&(p4(esk22_0)|~epred7_1(esk1_0)|(r1(X48,esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(~p5(esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46))))))&(((((r1(esk1_0,esk22_0)|~epred7_1(esk1_0)|(~p4(esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(~p5(esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46))))&((p5(esk22_0)|~epred7_1(esk1_0)|(~p4(esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(~p5(esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46))))&(~r1(esk22_0,X51)|p5(X51)|~epred7_1(esk1_0)|(~p4(esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(~p5(esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46))))))&(~p4(esk22_0)|~epred7_1(esk1_0)|(~p4(esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(~p5(esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46)))))&(~p5(esk22_0)|~epred7_1(esk1_0)|(~p4(esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(~p5(esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46)))))&(((p4(esk22_0)|~epred7_1(esk1_0)|(~p4(esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(~p5(esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46))))&(~r1(esk22_0,X52)|p4(X52)|~epred7_1(esk1_0)|(~p4(esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(~p5(esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46)))))&(p4(esk22_0)|~epred7_1(esk1_0)|(~p4(esk21_1(X48))|~p4(X48)|~p4(X48)|(~r1(esk1_0,X48)|p5(X48))|(~p5(esk20_1(X46))|~p5(X46)|~r1(esk1_0,X46)|p4(X46)))))))))&((r1(esk1_0,esk23_0)&~p10(esk23_0))&((~r1(esk23_0,X54)|p10(X54))&p10(esk23_0))))&((r1(esk1_0,esk24_0)&~p10(esk24_0))&((~r1(esk24_0,X56)|p10(X56))&p10(esk24_0))))&(((((((r1(esk1_0,esk27_0)|~epred8_1(esk1_0)|(r1(X59,esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(r1(X57,esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57))))&((p4(esk27_0)|~epred8_1(esk1_0)|(r1(X59,esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(r1(X57,esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57))))&(~r1(esk27_0,X62)|p4(X62)|~epred8_1(esk1_0)|(r1(X59,esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(r1(X57,esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57))))))&(~p3(esk27_0)|~epred8_1(esk1_0)|(r1(X59,esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(r1(X57,esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57)))))&(~p4(esk27_0)|~epred8_1(esk1_0)|(r1(X59,esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(r1(X57,esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57)))))&(((p3(esk27_0)|~epred8_1(esk1_0)|(r1(X59,esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(r1(X57,esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57))))&(~r1(esk27_0,X63)|p3(X63)|~epred8_1(esk1_0)|(r1(X59,esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(r1(X57,esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57)))))&(p3(esk27_0)|~epred8_1(esk1_0)|(r1(X59,esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(r1(X57,esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57))))))&(((((r1(esk1_0,esk27_0)|~epred8_1(esk1_0)|(~p3(esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(r1(X57,esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57))))&((p4(esk27_0)|~epred8_1(esk1_0)|(~p3(esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(r1(X57,esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57))))&(~r1(esk27_0,X62)|p4(X62)|~epred8_1(esk1_0)|(~p3(esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(r1(X57,esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57))))))&(~p3(esk27_0)|~epred8_1(esk1_0)|(~p3(esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(r1(X57,esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57)))))&(~p4(esk27_0)|~epred8_1(esk1_0)|(~p3(esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(r1(X57,esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57)))))&(((p3(esk27_0)|~epred8_1(esk1_0)|(~p3(esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(r1(X57,esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57))))&(~r1(esk27_0,X63)|p3(X63)|~epred8_1(esk1_0)|(~p3(esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(r1(X57,esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57)))))&(p3(esk27_0)|~epred8_1(esk1_0)|(~p3(esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(r1(X57,esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57)))))))&((((((r1(esk1_0,esk27_0)|~epred8_1(esk1_0)|(r1(X59,esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(~p4(esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57))))&((p4(esk27_0)|~epred8_1(esk1_0)|(r1(X59,esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(~p4(esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57))))&(~r1(esk27_0,X62)|p4(X62)|~epred8_1(esk1_0)|(r1(X59,esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(~p4(esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57))))))&(~p3(esk27_0)|~epred8_1(esk1_0)|(r1(X59,esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(~p4(esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57)))))&(~p4(esk27_0)|~epred8_1(esk1_0)|(r1(X59,esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(~p4(esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57)))))&(((p3(esk27_0)|~epred8_1(esk1_0)|(r1(X59,esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(~p4(esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57))))&(~r1(esk27_0,X63)|p3(X63)|~epred8_1(esk1_0)|(r1(X59,esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(~p4(esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57)))))&(p3(esk27_0)|~epred8_1(esk1_0)|(r1(X59,esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(~p4(esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57))))))&(((((r1(esk1_0,esk27_0)|~epred8_1(esk1_0)|(~p3(esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(~p4(esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57))))&((p4(esk27_0)|~epred8_1(esk1_0)|(~p3(esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(~p4(esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57))))&(~r1(esk27_0,X62)|p4(X62)|~epred8_1(esk1_0)|(~p3(esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(~p4(esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57))))))&(~p3(esk27_0)|~epred8_1(esk1_0)|(~p3(esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(~p4(esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57)))))&(~p4(esk27_0)|~epred8_1(esk1_0)|(~p3(esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(~p4(esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57)))))&(((p3(esk27_0)|~epred8_1(esk1_0)|(~p3(esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(~p4(esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57))))&(~r1(esk27_0,X63)|p3(X63)|~epred8_1(esk1_0)|(~p3(esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(~p4(esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57)))))&(p3(esk27_0)|~epred8_1(esk1_0)|(~p3(esk26_1(X59))|~p3(X59)|~p3(X59)|(~r1(esk1_0,X59)|p4(X59))|(~p4(esk25_1(X57))|~p4(X57)|~r1(esk1_0,X57)|p3(X57)))))))))&(((((((r1(esk1_0,esk30_0)|~epred9_1(esk1_0)|(r1(X66,esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(r1(X64,esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64))))&((p3(esk30_0)|~epred9_1(esk1_0)|(r1(X66,esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(r1(X64,esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64))))&(~r1(esk30_0,X69)|p3(X69)|~epred9_1(esk1_0)|(r1(X66,esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(r1(X64,esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64))))))&(~p2(esk30_0)|~epred9_1(esk1_0)|(r1(X66,esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(r1(X64,esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64)))))&(~p3(esk30_0)|~epred9_1(esk1_0)|(r1(X66,esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(r1(X64,esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64)))))&(((p2(esk30_0)|~epred9_1(esk1_0)|(r1(X66,esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(r1(X64,esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64))))&(~r1(esk30_0,X70)|p2(X70)|~epred9_1(esk1_0)|(r1(X66,esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(r1(X64,esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64)))))&(p2(esk30_0)|~epred9_1(esk1_0)|(r1(X66,esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(r1(X64,esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64))))))&(((((r1(esk1_0,esk30_0)|~epred9_1(esk1_0)|(~p2(esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(r1(X64,esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64))))&((p3(esk30_0)|~epred9_1(esk1_0)|(~p2(esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(r1(X64,esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64))))&(~r1(esk30_0,X69)|p3(X69)|~epred9_1(esk1_0)|(~p2(esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(r1(X64,esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64))))))&(~p2(esk30_0)|~epred9_1(esk1_0)|(~p2(esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(r1(X64,esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64)))))&(~p3(esk30_0)|~epred9_1(esk1_0)|(~p2(esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(r1(X64,esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64)))))&(((p2(esk30_0)|~epred9_1(esk1_0)|(~p2(esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(r1(X64,esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64))))&(~r1(esk30_0,X70)|p2(X70)|~epred9_1(esk1_0)|(~p2(esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(r1(X64,esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64)))))&(p2(esk30_0)|~epred9_1(esk1_0)|(~p2(esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(r1(X64,esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64)))))))&((((((r1(esk1_0,esk30_0)|~epred9_1(esk1_0)|(r1(X66,esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(~p3(esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64))))&((p3(esk30_0)|~epred9_1(esk1_0)|(r1(X66,esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(~p3(esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64))))&(~r1(esk30_0,X69)|p3(X69)|~epred9_1(esk1_0)|(r1(X66,esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(~p3(esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64))))))&(~p2(esk30_0)|~epred9_1(esk1_0)|(r1(X66,esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(~p3(esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64)))))&(~p3(esk30_0)|~epred9_1(esk1_0)|(r1(X66,esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(~p3(esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64)))))&(((p2(esk30_0)|~epred9_1(esk1_0)|(r1(X66,esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(~p3(esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64))))&(~r1(esk30_0,X70)|p2(X70)|~epred9_1(esk1_0)|(r1(X66,esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(~p3(esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64)))))&(p2(esk30_0)|~epred9_1(esk1_0)|(r1(X66,esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(~p3(esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64))))))&(((((r1(esk1_0,esk30_0)|~epred9_1(esk1_0)|(~p2(esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(~p3(esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64))))&((p3(esk30_0)|~epred9_1(esk1_0)|(~p2(esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(~p3(esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64))))&(~r1(esk30_0,X69)|p3(X69)|~epred9_1(esk1_0)|(~p2(esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(~p3(esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64))))))&(~p2(esk30_0)|~epred9_1(esk1_0)|(~p2(esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(~p3(esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64)))))&(~p3(esk30_0)|~epred9_1(esk1_0)|(~p2(esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(~p3(esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64)))))&(((p2(esk30_0)|~epred9_1(esk1_0)|(~p2(esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(~p3(esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64))))&(~r1(esk30_0,X70)|p2(X70)|~epred9_1(esk1_0)|(~p2(esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(~p3(esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64)))))&(p2(esk30_0)|~epred9_1(esk1_0)|(~p2(esk29_1(X66))|~p2(X66)|~p2(X66)|(~r1(esk1_0,X66)|p3(X66))|(~p3(esk28_1(X64))|~p3(X64)|~r1(esk1_0,X64)|p2(X64)))))))))&(((((((r1(esk1_0,esk33_0)|~epred10_1(esk1_0)|(r1(X73,esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(r1(X71,esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71))))&((p2(esk33_0)|~epred10_1(esk1_0)|(r1(X73,esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(r1(X71,esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71))))&(~r1(esk33_0,X76)|p2(X76)|~epred10_1(esk1_0)|(r1(X73,esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(r1(X71,esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71))))))&(~p1(esk33_0)|~epred10_1(esk1_0)|(r1(X73,esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(r1(X71,esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71)))))&(~p2(esk33_0)|~epred10_1(esk1_0)|(r1(X73,esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(r1(X71,esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71)))))&(((p1(esk33_0)|~epred10_1(esk1_0)|(r1(X73,esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(r1(X71,esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71))))&(~r1(esk33_0,X77)|p1(X77)|~epred10_1(esk1_0)|(r1(X73,esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(r1(X71,esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71)))))&(p1(esk33_0)|~epred10_1(esk1_0)|(r1(X73,esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(r1(X71,esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71))))))&(((((r1(esk1_0,esk33_0)|~epred10_1(esk1_0)|(~p1(esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(r1(X71,esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71))))&((p2(esk33_0)|~epred10_1(esk1_0)|(~p1(esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(r1(X71,esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71))))&(~r1(esk33_0,X76)|p2(X76)|~epred10_1(esk1_0)|(~p1(esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(r1(X71,esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71))))))&(~p1(esk33_0)|~epred10_1(esk1_0)|(~p1(esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(r1(X71,esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71)))))&(~p2(esk33_0)|~epred10_1(esk1_0)|(~p1(esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(r1(X71,esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71)))))&(((p1(esk33_0)|~epred10_1(esk1_0)|(~p1(esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(r1(X71,esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71))))&(~r1(esk33_0,X77)|p1(X77)|~epred10_1(esk1_0)|(~p1(esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(r1(X71,esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71)))))&(p1(esk33_0)|~epred10_1(esk1_0)|(~p1(esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(r1(X71,esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71)))))))&((((((r1(esk1_0,esk33_0)|~epred10_1(esk1_0)|(r1(X73,esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(~p2(esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71))))&((p2(esk33_0)|~epred10_1(esk1_0)|(r1(X73,esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(~p2(esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71))))&(~r1(esk33_0,X76)|p2(X76)|~epred10_1(esk1_0)|(r1(X73,esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(~p2(esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71))))))&(~p1(esk33_0)|~epred10_1(esk1_0)|(r1(X73,esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(~p2(esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71)))))&(~p2(esk33_0)|~epred10_1(esk1_0)|(r1(X73,esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(~p2(esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71)))))&(((p1(esk33_0)|~epred10_1(esk1_0)|(r1(X73,esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(~p2(esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71))))&(~r1(esk33_0,X77)|p1(X77)|~epred10_1(esk1_0)|(r1(X73,esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(~p2(esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71)))))&(p1(esk33_0)|~epred10_1(esk1_0)|(r1(X73,esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(~p2(esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71))))))&(((((r1(esk1_0,esk33_0)|~epred10_1(esk1_0)|(~p1(esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(~p2(esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71))))&((p2(esk33_0)|~epred10_1(esk1_0)|(~p1(esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(~p2(esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71))))&(~r1(esk33_0,X76)|p2(X76)|~epred10_1(esk1_0)|(~p1(esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(~p2(esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71))))))&(~p1(esk33_0)|~epred10_1(esk1_0)|(~p1(esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(~p2(esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71)))))&(~p2(esk33_0)|~epred10_1(esk1_0)|(~p1(esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(~p2(esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71)))))&(((p1(esk33_0)|~epred10_1(esk1_0)|(~p1(esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(~p2(esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71))))&(~r1(esk33_0,X77)|p1(X77)|~epred10_1(esk1_0)|(~p1(esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(~p2(esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71)))))&(p1(esk33_0)|~epred10_1(esk1_0)|(~p1(esk32_1(X73))|~p1(X73)|~p1(X73)|(~r1(esk1_0,X73)|p2(X73))|(~p2(esk31_1(X71))|~p2(X71)|~r1(esk1_0,X71)|p1(X71)))))))))), 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_11])])])])])])).
% 1.05/285.50 cnf(c_0_13, negated_conjecture, (~p10(esk23_0)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 1.05/285.50 cnf(c_0_14, negated_conjecture, (p10(esk23_0)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 1.05/285.50 cnf(c_0_15, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_13, c_0_14])]), ['proof']).
% 1.05/285.50 % SZS output end Proof
% 1.05/285.50 % User time : 0.036 s
% 1.05/285.50 % System time : 0.008 s
% 1.05/285.50 % Total time : 0.044 s
% 1.05/285.50 % User time : 0.106 s
% 1.05/285.50 % System time : 0.020 s
% 1.05/285.50 % Total time : 0.127 s
% 1.05/285.50
%------------------------------------------------------------------------------