%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL644+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n026.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.24s 0.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL644+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.34 % Computer : n026.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 : Sat Sep 5 07:11:10 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.24/0.46 start to proof:theBenchmark.p
% 0.24/0.55 % Version : CSI_E---1.1
% 0.24/0.55 % Problem : theBenchmark.p
% 0.24/0.55 % Proof found!
% 0.24/0.55 % SZS status Theorem for theBenchmark.p
% 0.24/0.55 % SZS output start Proof
% 0.24/0.55 fof(main, conjecture, ~(?[X1]:(~((~((![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))|p5(X2)|~((![X1]:((~(r1(X2,X1))|p5(X1)))&p5(X2)))))|![X2]:((~(r1(X1,X2))|p5(X2)|~((![X1]:((~(r1(X2,X1))|p5(X1)))&p5(X2)))))|~((![X2]:((~(r1(X1,X2))|~((p2(X2)&![X1]:((~(r1(X2,X1))|p2(X1)))))|p1(X2)))|![X2]:((~(r1(X1,X2))|p2(X2)|~(((p1(X2)&![X1]:((~(r1(X2,X1))|p1(X1))))&p1(X2)))))|~(((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((p2(X1)&![X2]:((~(r1(X1,X2))|p2(X2)))))|p1(X1)))|p2(X2)|~(((p1(X2)&![X1]:((~(r1(X2,X1))|p1(X1))))&p1(X2)))))&![X2]:((~(r1(X1,X2))|~((p2(X2)&![X1]:((~(r1(X2,X1))|p2(X1)))))|p1(X2)|![X1]:((~(r1(X2,X1))|p2(X1)|~(((p1(X1)&![X2]:((~(r1(X1,X2))|p1(X2))))&p1(X1))))))))&![X2]:((~(r1(X1,X2))|~((p2(X2)&![X1]:((~(r1(X2,X1))|p2(X1)))))|p1(X2)|p2(X2)|~(((p1(X2)&![X1]:((~(r1(X2,X1))|p1(X1))))&p1(X2))))))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', main)).
% 0.24/0.55 fof(c_0_1, plain, ![X1]:((epred1_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.24/0.55 fof(c_0_2, plain, ![X1]:((epred2_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.24/0.55 fof(c_0_3, plain, ![X1]:((epred3_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.24/0.55 fof(c_0_4, plain, ![X1]:((epred4_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.24/0.55 fof(c_0_5, plain, ![X1]:((epred5_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.24/0.55 fof(c_0_6, negated_conjecture, ~(~(?[X1]:(~((~((![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)))))|~((epred1_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)))))|~((epred2_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)))))|~((epred3_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)))))|~((epred4_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)|p5(X2)|~((![X1]:((~r1(X2,X1)|p5(X1)))&p5(X2)))))|![X2]:((~r1(X1,X2)|p5(X2)|~((![X1]:((~r1(X2,X1)|p5(X1)))&p5(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)))))|~((epred5_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(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])).
% 0.24/0.55 fof(c_0_7, negated_conjecture, ![X4, X6, X9, X10, X11, X13, X16, X17, X18, X20, X23, X24, X25, X27, X30, X31, X33, X35, X36, X38, X41, X42]:((((((((((((((r1(esk1_0,esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(r1(X4,esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4))))&((p6(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(r1(X4,esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4))))&(~r1(esk4_0,X9)|p6(X9)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(r1(X4,esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4))))))&(~p5(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(r1(X4,esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4)))))&(~p6(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(r1(X4,esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4)))))&(((p5(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(r1(X4,esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4))))&(~r1(esk4_0,X10)|p5(X10)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(r1(X4,esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4)))))&(p5(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(r1(X4,esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4))))))&(((((r1(esk1_0,esk4_0)|~epred1_1(esk1_0)|(~p5(esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(r1(X4,esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4))))&((p6(esk4_0)|~epred1_1(esk1_0)|(~p5(esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(r1(X4,esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4))))&(~r1(esk4_0,X9)|p6(X9)|~epred1_1(esk1_0)|(~p5(esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(r1(X4,esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4))))))&(~p5(esk4_0)|~epred1_1(esk1_0)|(~p5(esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(r1(X4,esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4)))))&(~p6(esk4_0)|~epred1_1(esk1_0)|(~p5(esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(r1(X4,esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4)))))&(((p5(esk4_0)|~epred1_1(esk1_0)|(~p5(esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(r1(X4,esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4))))&(~r1(esk4_0,X10)|p5(X10)|~epred1_1(esk1_0)|(~p5(esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(r1(X4,esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4)))))&(p5(esk4_0)|~epred1_1(esk1_0)|(~p5(esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(r1(X4,esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4)))))))&((((((r1(esk1_0,esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(~p6(esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4))))&((p6(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(~p6(esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4))))&(~r1(esk4_0,X9)|p6(X9)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(~p6(esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4))))))&(~p5(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(~p6(esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4)))))&(~p6(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(~p6(esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4)))))&(((p5(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(~p6(esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4))))&(~r1(esk4_0,X10)|p5(X10)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(~p6(esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4)))))&(p5(esk4_0)|~epred1_1(esk1_0)|(r1(X6,esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(~p6(esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4))))))&(((((r1(esk1_0,esk4_0)|~epred1_1(esk1_0)|(~p5(esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(~p6(esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4))))&((p6(esk4_0)|~epred1_1(esk1_0)|(~p5(esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(~p6(esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4))))&(~r1(esk4_0,X9)|p6(X9)|~epred1_1(esk1_0)|(~p5(esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(~p6(esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4))))))&(~p5(esk4_0)|~epred1_1(esk1_0)|(~p5(esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(~p6(esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4)))))&(~p6(esk4_0)|~epred1_1(esk1_0)|(~p5(esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(~p6(esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4)))))&(((p5(esk4_0)|~epred1_1(esk1_0)|(~p5(esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(~p6(esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4))))&(~r1(esk4_0,X10)|p5(X10)|~epred1_1(esk1_0)|(~p5(esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(~p6(esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4)))))&(p5(esk4_0)|~epred1_1(esk1_0)|(~p5(esk3_1(X6))|~p5(X6)|~p5(X6)|(~r1(esk1_0,X6)|p6(X6))|(~p6(esk2_1(X4))|~p6(X4)|~r1(esk1_0,X4)|p5(X4))))))))&(((((((r1(esk1_0,esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(r1(X11,esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11))))&((p5(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(r1(X11,esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11))))&(~r1(esk7_0,X16)|p5(X16)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(r1(X11,esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11))))))&(~p4(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(r1(X11,esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11)))))&(~p5(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(r1(X11,esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11)))))&(((p4(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(r1(X11,esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11))))&(~r1(esk7_0,X17)|p4(X17)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(r1(X11,esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11)))))&(p4(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(r1(X11,esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11))))))&(((((r1(esk1_0,esk7_0)|~epred2_1(esk1_0)|(~p4(esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(r1(X11,esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11))))&((p5(esk7_0)|~epred2_1(esk1_0)|(~p4(esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(r1(X11,esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11))))&(~r1(esk7_0,X16)|p5(X16)|~epred2_1(esk1_0)|(~p4(esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(r1(X11,esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11))))))&(~p4(esk7_0)|~epred2_1(esk1_0)|(~p4(esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(r1(X11,esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11)))))&(~p5(esk7_0)|~epred2_1(esk1_0)|(~p4(esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(r1(X11,esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11)))))&(((p4(esk7_0)|~epred2_1(esk1_0)|(~p4(esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(r1(X11,esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11))))&(~r1(esk7_0,X17)|p4(X17)|~epred2_1(esk1_0)|(~p4(esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(r1(X11,esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11)))))&(p4(esk7_0)|~epred2_1(esk1_0)|(~p4(esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(r1(X11,esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11)))))))&((((((r1(esk1_0,esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(~p5(esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11))))&((p5(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(~p5(esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11))))&(~r1(esk7_0,X16)|p5(X16)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(~p5(esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11))))))&(~p4(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(~p5(esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11)))))&(~p5(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(~p5(esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11)))))&(((p4(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(~p5(esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11))))&(~r1(esk7_0,X17)|p4(X17)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(~p5(esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11)))))&(p4(esk7_0)|~epred2_1(esk1_0)|(r1(X13,esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(~p5(esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11))))))&(((((r1(esk1_0,esk7_0)|~epred2_1(esk1_0)|(~p4(esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(~p5(esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11))))&((p5(esk7_0)|~epred2_1(esk1_0)|(~p4(esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(~p5(esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11))))&(~r1(esk7_0,X16)|p5(X16)|~epred2_1(esk1_0)|(~p4(esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(~p5(esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11))))))&(~p4(esk7_0)|~epred2_1(esk1_0)|(~p4(esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(~p5(esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11)))))&(~p5(esk7_0)|~epred2_1(esk1_0)|(~p4(esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(~p5(esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11)))))&(((p4(esk7_0)|~epred2_1(esk1_0)|(~p4(esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(~p5(esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11))))&(~r1(esk7_0,X17)|p4(X17)|~epred2_1(esk1_0)|(~p4(esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(~p5(esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11)))))&(p4(esk7_0)|~epred2_1(esk1_0)|(~p4(esk6_1(X13))|~p4(X13)|~p4(X13)|(~r1(esk1_0,X13)|p5(X13))|(~p5(esk5_1(X11))|~p5(X11)|~r1(esk1_0,X11)|p4(X11)))))))))&(((((((r1(esk1_0,esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(r1(X18,esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18))))&((p4(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(r1(X18,esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18))))&(~r1(esk10_0,X23)|p4(X23)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(r1(X18,esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18))))))&(~p3(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(r1(X18,esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18)))))&(~p4(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(r1(X18,esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18)))))&(((p3(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(r1(X18,esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18))))&(~r1(esk10_0,X24)|p3(X24)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(r1(X18,esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18)))))&(p3(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(r1(X18,esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18))))))&(((((r1(esk1_0,esk10_0)|~epred3_1(esk1_0)|(~p3(esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(r1(X18,esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18))))&((p4(esk10_0)|~epred3_1(esk1_0)|(~p3(esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(r1(X18,esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18))))&(~r1(esk10_0,X23)|p4(X23)|~epred3_1(esk1_0)|(~p3(esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(r1(X18,esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18))))))&(~p3(esk10_0)|~epred3_1(esk1_0)|(~p3(esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(r1(X18,esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18)))))&(~p4(esk10_0)|~epred3_1(esk1_0)|(~p3(esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(r1(X18,esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18)))))&(((p3(esk10_0)|~epred3_1(esk1_0)|(~p3(esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(r1(X18,esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18))))&(~r1(esk10_0,X24)|p3(X24)|~epred3_1(esk1_0)|(~p3(esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(r1(X18,esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18)))))&(p3(esk10_0)|~epred3_1(esk1_0)|(~p3(esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(r1(X18,esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18)))))))&((((((r1(esk1_0,esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(~p4(esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18))))&((p4(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(~p4(esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18))))&(~r1(esk10_0,X23)|p4(X23)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(~p4(esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18))))))&(~p3(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(~p4(esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18)))))&(~p4(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(~p4(esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18)))))&(((p3(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(~p4(esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18))))&(~r1(esk10_0,X24)|p3(X24)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(~p4(esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18)))))&(p3(esk10_0)|~epred3_1(esk1_0)|(r1(X20,esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(~p4(esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18))))))&(((((r1(esk1_0,esk10_0)|~epred3_1(esk1_0)|(~p3(esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(~p4(esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18))))&((p4(esk10_0)|~epred3_1(esk1_0)|(~p3(esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(~p4(esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18))))&(~r1(esk10_0,X23)|p4(X23)|~epred3_1(esk1_0)|(~p3(esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(~p4(esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18))))))&(~p3(esk10_0)|~epred3_1(esk1_0)|(~p3(esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(~p4(esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18)))))&(~p4(esk10_0)|~epred3_1(esk1_0)|(~p3(esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(~p4(esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18)))))&(((p3(esk10_0)|~epred3_1(esk1_0)|(~p3(esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(~p4(esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18))))&(~r1(esk10_0,X24)|p3(X24)|~epred3_1(esk1_0)|(~p3(esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(~p4(esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18)))))&(p3(esk10_0)|~epred3_1(esk1_0)|(~p3(esk9_1(X20))|~p3(X20)|~p3(X20)|(~r1(esk1_0,X20)|p4(X20))|(~p4(esk8_1(X18))|~p4(X18)|~r1(esk1_0,X18)|p3(X18)))))))))&(((((((r1(esk1_0,esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(r1(X25,esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25))))&((p3(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(r1(X25,esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25))))&(~r1(esk13_0,X30)|p3(X30)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(r1(X25,esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25))))))&(~p2(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(r1(X25,esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25)))))&(~p3(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(r1(X25,esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25)))))&(((p2(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(r1(X25,esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25))))&(~r1(esk13_0,X31)|p2(X31)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(r1(X25,esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25)))))&(p2(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(r1(X25,esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25))))))&(((((r1(esk1_0,esk13_0)|~epred4_1(esk1_0)|(~p2(esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(r1(X25,esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25))))&((p3(esk13_0)|~epred4_1(esk1_0)|(~p2(esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(r1(X25,esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25))))&(~r1(esk13_0,X30)|p3(X30)|~epred4_1(esk1_0)|(~p2(esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(r1(X25,esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25))))))&(~p2(esk13_0)|~epred4_1(esk1_0)|(~p2(esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(r1(X25,esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25)))))&(~p3(esk13_0)|~epred4_1(esk1_0)|(~p2(esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(r1(X25,esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25)))))&(((p2(esk13_0)|~epred4_1(esk1_0)|(~p2(esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(r1(X25,esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25))))&(~r1(esk13_0,X31)|p2(X31)|~epred4_1(esk1_0)|(~p2(esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(r1(X25,esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25)))))&(p2(esk13_0)|~epred4_1(esk1_0)|(~p2(esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(r1(X25,esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25)))))))&((((((r1(esk1_0,esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(~p3(esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25))))&((p3(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(~p3(esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25))))&(~r1(esk13_0,X30)|p3(X30)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(~p3(esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25))))))&(~p2(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(~p3(esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25)))))&(~p3(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(~p3(esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25)))))&(((p2(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(~p3(esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25))))&(~r1(esk13_0,X31)|p2(X31)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(~p3(esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25)))))&(p2(esk13_0)|~epred4_1(esk1_0)|(r1(X27,esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(~p3(esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25))))))&(((((r1(esk1_0,esk13_0)|~epred4_1(esk1_0)|(~p2(esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(~p3(esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25))))&((p3(esk13_0)|~epred4_1(esk1_0)|(~p2(esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(~p3(esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25))))&(~r1(esk13_0,X30)|p3(X30)|~epred4_1(esk1_0)|(~p2(esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(~p3(esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25))))))&(~p2(esk13_0)|~epred4_1(esk1_0)|(~p2(esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(~p3(esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25)))))&(~p3(esk13_0)|~epred4_1(esk1_0)|(~p2(esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(~p3(esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25)))))&(((p2(esk13_0)|~epred4_1(esk1_0)|(~p2(esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(~p3(esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25))))&(~r1(esk13_0,X31)|p2(X31)|~epred4_1(esk1_0)|(~p2(esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(~p3(esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25)))))&(p2(esk13_0)|~epred4_1(esk1_0)|(~p2(esk12_1(X27))|~p2(X27)|~p2(X27)|(~r1(esk1_0,X27)|p3(X27))|(~p3(esk11_1(X25))|~p3(X25)|~r1(esk1_0,X25)|p2(X25)))))))))&((r1(esk1_0,esk14_0)&~p5(esk14_0))&((~r1(esk14_0,X33)|p5(X33))&p5(esk14_0))))&((r1(esk1_0,esk15_0)&~p5(esk15_0))&((~r1(esk15_0,X35)|p5(X35))&p5(esk15_0))))&(((((((r1(esk1_0,esk18_0)|~epred5_1(esk1_0)|(r1(X38,esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(r1(X36,esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36))))&((p2(esk18_0)|~epred5_1(esk1_0)|(r1(X38,esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(r1(X36,esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36))))&(~r1(esk18_0,X41)|p2(X41)|~epred5_1(esk1_0)|(r1(X38,esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(r1(X36,esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36))))))&(~p1(esk18_0)|~epred5_1(esk1_0)|(r1(X38,esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(r1(X36,esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36)))))&(~p2(esk18_0)|~epred5_1(esk1_0)|(r1(X38,esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(r1(X36,esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36)))))&(((p1(esk18_0)|~epred5_1(esk1_0)|(r1(X38,esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(r1(X36,esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36))))&(~r1(esk18_0,X42)|p1(X42)|~epred5_1(esk1_0)|(r1(X38,esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(r1(X36,esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36)))))&(p1(esk18_0)|~epred5_1(esk1_0)|(r1(X38,esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(r1(X36,esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36))))))&(((((r1(esk1_0,esk18_0)|~epred5_1(esk1_0)|(~p1(esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(r1(X36,esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36))))&((p2(esk18_0)|~epred5_1(esk1_0)|(~p1(esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(r1(X36,esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36))))&(~r1(esk18_0,X41)|p2(X41)|~epred5_1(esk1_0)|(~p1(esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(r1(X36,esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36))))))&(~p1(esk18_0)|~epred5_1(esk1_0)|(~p1(esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(r1(X36,esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36)))))&(~p2(esk18_0)|~epred5_1(esk1_0)|(~p1(esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(r1(X36,esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36)))))&(((p1(esk18_0)|~epred5_1(esk1_0)|(~p1(esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(r1(X36,esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36))))&(~r1(esk18_0,X42)|p1(X42)|~epred5_1(esk1_0)|(~p1(esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(r1(X36,esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36)))))&(p1(esk18_0)|~epred5_1(esk1_0)|(~p1(esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(r1(X36,esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36)))))))&((((((r1(esk1_0,esk18_0)|~epred5_1(esk1_0)|(r1(X38,esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(~p2(esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36))))&((p2(esk18_0)|~epred5_1(esk1_0)|(r1(X38,esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(~p2(esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36))))&(~r1(esk18_0,X41)|p2(X41)|~epred5_1(esk1_0)|(r1(X38,esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(~p2(esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36))))))&(~p1(esk18_0)|~epred5_1(esk1_0)|(r1(X38,esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(~p2(esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36)))))&(~p2(esk18_0)|~epred5_1(esk1_0)|(r1(X38,esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(~p2(esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36)))))&(((p1(esk18_0)|~epred5_1(esk1_0)|(r1(X38,esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(~p2(esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36))))&(~r1(esk18_0,X42)|p1(X42)|~epred5_1(esk1_0)|(r1(X38,esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(~p2(esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36)))))&(p1(esk18_0)|~epred5_1(esk1_0)|(r1(X38,esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(~p2(esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36))))))&(((((r1(esk1_0,esk18_0)|~epred5_1(esk1_0)|(~p1(esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(~p2(esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36))))&((p2(esk18_0)|~epred5_1(esk1_0)|(~p1(esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(~p2(esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36))))&(~r1(esk18_0,X41)|p2(X41)|~epred5_1(esk1_0)|(~p1(esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(~p2(esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36))))))&(~p1(esk18_0)|~epred5_1(esk1_0)|(~p1(esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(~p2(esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36)))))&(~p2(esk18_0)|~epred5_1(esk1_0)|(~p1(esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(~p2(esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36)))))&(((p1(esk18_0)|~epred5_1(esk1_0)|(~p1(esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(~p2(esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36))))&(~r1(esk18_0,X42)|p1(X42)|~epred5_1(esk1_0)|(~p1(esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(~p2(esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36)))))&(p1(esk18_0)|~epred5_1(esk1_0)|(~p1(esk17_1(X38))|~p1(X38)|~p1(X38)|(~r1(esk1_0,X38)|p2(X38))|(~p2(esk16_1(X36))|~p2(X36)|~r1(esk1_0,X36)|p1(X36)))))))))), 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_6])])])])])])).
% 0.24/0.55 cnf(c_0_8, negated_conjecture, (~p5(esk14_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.24/0.55 cnf(c_0_9, negated_conjecture, (p5(esk14_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.24/0.55 cnf(c_0_10, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_8, c_0_9])]), ['proof']).
% 0.24/0.55 % SZS output end Proof
% 0.24/0.55 % User time : 0.022 s
% 0.24/0.55 % System time : 0.003 s
% 0.24/0.55 % Total time : 0.026 s
% 0.24/0.55 % User time : 0.023 s
% 0.24/0.55 % System time : 0.007 s
% 0.24/0.55 % Total time : 0.029 s
% 0.24/0.55
%------------------------------------------------------------------------------