%------------------------------------------------------------------------------
% File : Etableau---0.67
% Problem : LCL644+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 12:01:33 PM UTC 2026
% Result : Theorem 0.09s 0.42s
% 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.04 % Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s
% 0.09/0.36 % Computer : n015.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 5 07:10:27 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.42 # No SInE strategy applied
% 0.09/0.42 # Auto-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S5PRR_RG_S04AN
% 0.09/0.42 # and selection function SelectComplexExceptUniqMaxHorn.
% 0.09/0.42 #
% 0.09/0.42 # Presaturation interreduction done
% 0.09/0.42
% 0.09/0.42 # Proof found!
% 0.09/0.42 # SZS status Theorem
% 0.09/0.42 # SZS output start CNFRefutation
% 0.09/0.42 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.09/0.42 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.09/0.42 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.09/0.42 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.09/0.42 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.09/0.42 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.09/0.42 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(assume_negation,[status(cth)],[main]), c_0_1]), c_0_2]), c_0_3]), c_0_4]), c_0_5])).
% 0.09/0.42 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(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_6])])])])])])).
% 0.09/0.42 cnf(c_0_8, negated_conjecture, (~p5(esk14_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.09/0.42 cnf(c_0_9, negated_conjecture, (p5(esk14_0)), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.09/0.42 cnf(c_0_10, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_8, c_0_9])]), ['proof']).
% 0.09/0.42 # SZS output end CNFRefutation
% 0.09/0.42 # Training examples: 0 positive, 0 negative
%------------------------------------------------------------------------------