Theorem. (l18_hessenbe)
∀esk13_5 : setsetsetsetsetset, ∀v5_anproj_2 : setprop, ∀esk20_1 : setset, ∀l1_struct_0 : setprop, ∀esk12_0 : set, ∀esk8_0 : set, ∀esk6_0 : set, ∀esk28_1 : setset, ∀esk27_0 : set, ∀esk26_0 : set, ∀esk3_0 : set, ∀esk5_0 : set, ∀esk7_0 : set, ∀esk29_0 : set, ∀esk4_0 : set, ∀esk2_0 : set, ∀esk9_0 : set, ∀esk11_0 : set, ∀esk10_0 : set, ∀esk1_0 : set, ∀esk21_1 : setset, ∀esk22_1 : setset, ∀esk25_1 : setset, ∀esk24_1 : setset, ∀esk23_1 : setset, ∀esk16_1 : setset, ∀esk17_1 : setset, ∀esk14_1 : setset, ∀esk15_1 : setset, ∀esk18_1 : setset, ∀esk19_1 : setset, ∀v2_struct_0 : setprop, ∀v3_collsp : setprop, ∀v2_anproj_2 : setprop, ∀v6_anproj_2 : setprop, ∀l1_collsp : setprop, ∀m1_subset_1 : setsetprop, ∀u1_struct_0 : setset, ∀v7_anproj_2 : setprop, ∀v3_anproj_2 : setprop, ∀v4_collsp : setprop, ∀v2_collsp : setprop, ∀r1_collsp : setsetsetsetprop, (∀X5 X4 X3 X1 X10 X9 X8 X2 X6 X7, (X6 = X7False)(X5 = X7False)(X5 = X6False)(X3 = X4False)(X2 = X3False)(v2_struct_0 X1False)(r1_collsp X1 X10 X9 X8False)(r1_collsp X1 X4 X2 X7False)v2_collsp X1v3_collsp X1v4_collsp X1v2_anproj_2 X1v3_anproj_2 X1v6_anproj_2 X1v7_anproj_2 X1l1_collsp X1m1_subset_1 X10 (u1_struct_0 X1)m1_subset_1 X9 (u1_struct_0 X1)m1_subset_1 X8 (u1_struct_0 X1)m1_subset_1 X7 (u1_struct_0 X1)m1_subset_1 X6 (u1_struct_0 X1)m1_subset_1 X5 (u1_struct_0 X1)m1_subset_1 X4 (u1_struct_0 X1)m1_subset_1 X3 (u1_struct_0 X1)m1_subset_1 X2 (u1_struct_0 X1)r1_collsp X1 X7 X5 X6r1_collsp X1 X7 X2 X8r1_collsp X1 X4 X6 X9r1_collsp X1 X4 X5 X8r1_collsp X1 X4 X2 X3r1_collsp X1 X3 X7 X9r1_collsp X1 X3 X5 X10r1_collsp X1 X2 X6 X10False)(∀X4 X3 X2 X5 X1, (v2_struct_0 X1False)(r1_collsp X1 X2 X3 (esk13_5 X1 X2 X3 X4 X5)False)v2_collsp X1v3_collsp X1v4_collsp X1v2_anproj_2 X1v3_anproj_2 X1v7_anproj_2 X1l1_collsp X1m1_subset_1 X5 (u1_struct_0 X1)m1_subset_1 X4 (u1_struct_0 X1)m1_subset_1 X3 (u1_struct_0 X1)m1_subset_1 X2 (u1_struct_0 X1)False)(∀X4 X3 X2 X5 X1, (v2_struct_0 X1False)(r1_collsp X1 X2 X3 (esk13_5 X1 X4 X5 X2 X3)False)v2_collsp X1v3_collsp X1v4_collsp X1v2_anproj_2 X1v3_anproj_2 X1v7_anproj_2 X1l1_collsp X1m1_subset_1 X5 (u1_struct_0 X1)m1_subset_1 X4 (u1_struct_0 X1)m1_subset_1 X3 (u1_struct_0 X1)m1_subset_1 X2 (u1_struct_0 X1)False)(∀X4 X3 X2 X5 X1, (v2_struct_0 X1False)(m1_subset_1 (esk13_5 X1 X2 X3 X4 X5) (u1_struct_0 X1)False)v2_collsp X1v3_collsp X1v4_collsp X1v2_anproj_2 X1v3_anproj_2 X1v7_anproj_2 X1l1_collsp X1m1_subset_1 X5 (u1_struct_0 X1)m1_subset_1 X4 (u1_struct_0 X1)m1_subset_1 X3 (u1_struct_0 X1)m1_subset_1 X2 (u1_struct_0 X1)False)(∀X5 X4 X1 X2 X3 X6 X7, (X6 = X7False)(X4 = X5False)(X2 = X3False)(v2_struct_0 X1False)(r1_collsp X1 X2 X3 X4False)v2_collsp X1v3_collsp X1v4_collsp X1v2_anproj_2 X1v3_anproj_2 X1l1_collsp X1m1_subset_1 X7 (u1_struct_0 X1)m1_subset_1 X6 (u1_struct_0 X1)m1_subset_1 X5 (u1_struct_0 X1)m1_subset_1 X4 (u1_struct_0 X1)m1_subset_1 X3 (u1_struct_0 X1)m1_subset_1 X2 (u1_struct_0 X1)r1_collsp X1 X4 X5 X7r1_collsp X1 X4 X5 X6r1_collsp X1 X2 X3 X7r1_collsp X1 X2 X3 X6False)(∀X4 X1 X2 X3 X6 X5 X7, (X5 = X7False)(X4 = X7False)(X4 = X6False)(X1 = X6False)(v2_struct_0 X3False)(r1_collsp X3 X1 X4 X5False)X1 = X2v2_collsp X3v3_collsp X3v4_collsp X3v2_anproj_2 X3v3_anproj_2 X3l1_collsp X3m1_subset_1 X7 (u1_struct_0 X3)m1_subset_1 X6 (u1_struct_0 X3)m1_subset_1 X5 (u1_struct_0 X3)m1_subset_1 X4 (u1_struct_0 X3)m1_subset_1 X2 (u1_struct_0 X3)m1_subset_1 X1 (u1_struct_0 X3)r1_collsp X3 X7 X6 X2r1_collsp X3 X4 X5 X7r1_collsp X3 X1 X4 X6False)(∀X6 X1 X2 X3 X4 X5 X7, (X5 = X7False)(X5 = X6False)(X4 = X6False)(X1 = X7False)(v2_struct_0 X3False)(r1_collsp X3 X4 X5 X1False)X1 = X2v2_collsp X3v3_collsp X3v4_collsp X3v2_anproj_2 X3v3_anproj_2 X3l1_collsp X3m1_subset_1 X7 (u1_struct_0 X3)m1_subset_1 X6 (u1_struct_0 X3)m1_subset_1 X5 (u1_struct_0 X3)m1_subset_1 X4 (u1_struct_0 X3)m1_subset_1 X2 (u1_struct_0 X3)m1_subset_1 X1 (u1_struct_0 X3)r1_collsp X3 X7 X6 X2r1_collsp X3 X5 X1 X7r1_collsp X3 X4 X5 X6False)(∀X6 X2 X3 X7 X1 X4 X5, (X4 = X5False)(X2 = X6False)(v2_struct_0 X1False)(r1_collsp X1 X2 X3 X4False)X4 = X7v2_collsp X1v3_collsp X1v4_collsp X1v2_anproj_2 X1v3_anproj_2 X1l1_collsp X1m1_subset_1 X7 (u1_struct_0 X1)m1_subset_1 X6 (u1_struct_0 X1)m1_subset_1 X5 (u1_struct_0 X1)m1_subset_1 X4 (u1_struct_0 X1)m1_subset_1 X3 (u1_struct_0 X1)m1_subset_1 X2 (u1_struct_0 X1)r1_collsp X1 X6 X5 X7r1_collsp X1 X2 X4 X5r1_collsp X1 X2 X3 X6False)(∀X5 X4 X3 X1 X2 X6, (X2 = X6False)(X2 = X5False)(v2_struct_0 X1False)(r1_collsp X1 X2 X3 X4False)v2_collsp X1v3_collsp X1v4_collsp X1v2_anproj_2 X1v3_anproj_2 X1l1_collsp X1m1_subset_1 X6 (u1_struct_0 X1)m1_subset_1 X5 (u1_struct_0 X1)m1_subset_1 X4 (u1_struct_0 X1)m1_subset_1 X3 (u1_struct_0 X1)m1_subset_1 X2 (u1_struct_0 X1)r1_collsp X1 X5 X2 X6r1_collsp X1 X4 X6 X2r1_collsp X1 X2 X3 X5False)(∀X1 X4 X5 X6 X2 X3, (X2 = X3False)(v2_struct_0 X1False)(r1_collsp X1 X4 X5 X6False)v3_collsp X1l1_collsp X1m1_subset_1 X6 (u1_struct_0 X1)m1_subset_1 X5 (u1_struct_0 X1)m1_subset_1 X4 (u1_struct_0 X1)m1_subset_1 X3 (u1_struct_0 X1)m1_subset_1 X2 (u1_struct_0 X1)r1_collsp X1 X2 X3 X6r1_collsp X1 X2 X3 X5r1_collsp X1 X2 X3 X4False)(∀X1, (v2_struct_0 X1False)(v2_collsp X1False)l1_collsp X1r1_collsp X1 (esk18_1 X1) (esk18_1 X1) (esk19_1 X1)r1_collsp X1 (esk18_1 X1) (esk19_1 X1) (esk18_1 X1)r1_collsp X1 (esk18_1 X1) (esk19_1 X1) (esk19_1 X1)False)(∀X1 X4 X5 X2 X3, (X2 = X3False)(v2_struct_0 X1False)(r1_collsp X1 X2 X4 X5False)v2_collsp X1v3_collsp X1v4_collsp X1v2_anproj_2 X1v3_anproj_2 X1l1_collsp X1m1_subset_1 X5 (u1_struct_0 X1)m1_subset_1 X4 (u1_struct_0 X1)m1_subset_1 X3 (u1_struct_0 X1)m1_subset_1 X2 (u1_struct_0 X1)r1_collsp X1 X2 X3 X5r1_collsp X1 X2 X3 X4False)(∀X1 X3 X4 X2 X5, (X2 = X5False)(v2_struct_0 X1False)(r1_collsp X1 X2 X3 X4False)v2_collsp X1v3_collsp X1v4_collsp X1v2_anproj_2 X1v3_anproj_2 X1l1_collsp X1m1_subset_1 X5 (u1_struct_0 X1)m1_subset_1 X4 (u1_struct_0 X1)m1_subset_1 X3 (u1_struct_0 X1)m1_subset_1 X2 (u1_struct_0 X1)r1_collsp X1 X2 X4 X5r1_collsp X1 X2 X3 X5False)(∀X1 X3 X4 X2 X5, (X2 = X5False)(v2_struct_0 X1False)(r1_collsp X1 X2 X3 X4False)v2_collsp X1v3_collsp X1v4_collsp X1v2_anproj_2 X1v3_anproj_2 X1l1_collsp X1m1_subset_1 X5 (u1_struct_0 X1)m1_subset_1 X4 (u1_struct_0 X1)m1_subset_1 X3 (u1_struct_0 X1)m1_subset_1 X2 (u1_struct_0 X1)r1_collsp X1 X2 X5 X4r1_collsp X1 X2 X3 X5False)(∀X1 X2, (v2_struct_0 X2False)(v7_anproj_2 X2False)v2_collsp X2v3_collsp X2v4_collsp X2v2_anproj_2 X2v3_anproj_2 X2l1_collsp X2m1_subset_1 X1 (u1_struct_0 X2)r1_collsp X2 (esk14_1 X2) (esk15_1 X2) X1r1_collsp X2 (esk16_1 X2) (esk17_1 X2) X1False)(∀X4 X2 X3 X1, (v2_struct_0 X1False)(r1_collsp X1 X2 X3 X4False)v2_collsp X1v3_collsp X1v4_collsp X1v2_anproj_2 X1v3_anproj_2 X1l1_collsp X1m1_subset_1 X4 (u1_struct_0 X1)m1_subset_1 X3 (u1_struct_0 X1)m1_subset_1 X2 (u1_struct_0 X1)r1_collsp X1 X2 X4 X3False)(∀X4 X2 X3 X1, (v2_struct_0 X1False)(r1_collsp X1 X2 X3 X4False)v2_collsp X1v3_collsp X1v4_collsp X1v2_anproj_2 X1v3_anproj_2 X1l1_collsp X1m1_subset_1 X4 (u1_struct_0 X1)m1_subset_1 X3 (u1_struct_0 X1)m1_subset_1 X2 (u1_struct_0 X1)r1_collsp X1 X3 X2 X4False)(∀X4 X2 X3 X1, (v2_struct_0 X1False)(r1_collsp X1 X2 X3 X4False)v2_collsp X1v3_collsp X1v4_collsp X1v2_anproj_2 X1v3_anproj_2 X1l1_collsp X1m1_subset_1 X4 (u1_struct_0 X1)m1_subset_1 X3 (u1_struct_0 X1)m1_subset_1 X2 (u1_struct_0 X1)r1_collsp X1 X3 X4 X2False)(∀X4 X2 X3 X1, (v2_struct_0 X1False)(r1_collsp X1 X2 X3 X4False)v2_collsp X1v3_collsp X1v4_collsp X1v2_anproj_2 X1v3_anproj_2 X1l1_collsp X1m1_subset_1 X4 (u1_struct_0 X1)m1_subset_1 X3 (u1_struct_0 X1)m1_subset_1 X2 (u1_struct_0 X1)r1_collsp X1 X4 X2 X3False)(∀X4 X2 X3 X1, (v2_struct_0 X1False)(r1_collsp X1 X2 X3 X4False)v2_collsp X1v3_collsp X1v4_collsp X1v2_anproj_2 X1v3_anproj_2 X1l1_collsp X1m1_subset_1 X4 (u1_struct_0 X1)m1_subset_1 X3 (u1_struct_0 X1)m1_subset_1 X2 (u1_struct_0 X1)r1_collsp X1 X4 X3 X2False)(∀X1, (v2_struct_0 X1False)(v3_collsp X1False)l1_collsp X1r1_collsp X1 (esk23_1 X1) (esk24_1 X1) (esk25_1 X1)False)(∀X3 X2 X4 X1, (v2_struct_0 X1False)(r1_collsp X1 X2 X2 X3False)v2_collsp X1l1_collsp X1m1_subset_1 X4 (u1_struct_0 X1)m1_subset_1 X3 (u1_struct_0 X1)m1_subset_1 X2 (u1_struct_0 X1)False)(∀X3 X2 X4 X1, (v2_struct_0 X1False)(r1_collsp X1 X2 X3 X2False)v2_collsp X1l1_collsp X1m1_subset_1 X4 (u1_struct_0 X1)m1_subset_1 X3 (u1_struct_0 X1)m1_subset_1 X2 (u1_struct_0 X1)False)(∀X2 X3 X4 X1, (v2_struct_0 X1False)(r1_collsp X1 X2 X3 X3False)v2_collsp X1l1_collsp X1m1_subset_1 X4 (u1_struct_0 X1)m1_subset_1 X3 (u1_struct_0 X1)m1_subset_1 X2 (u1_struct_0 X1)False)(∀X1, (v2_struct_0 X1False)(v3_collsp X1False)(r1_collsp X1 (esk21_1 X1) (esk22_1 X1) (esk25_1 X1)False)l1_collsp X1False)(∀X1, (v2_struct_0 X1False)(v3_collsp X1False)(r1_collsp X1 (esk21_1 X1) (esk22_1 X1) (esk24_1 X1)False)l1_collsp X1False)(∀X1, (v2_struct_0 X1False)(v3_collsp X1False)(r1_collsp X1 (esk21_1 X1) (esk22_1 X1) (esk23_1 X1)False)l1_collsp X1False)(∀X1, (v2_struct_0 X1False)(v7_anproj_2 X1False)(m1_subset_1 (esk17_1 X1) (u1_struct_0 X1)False)v2_collsp X1v3_collsp X1v4_collsp X1v2_anproj_2 X1v3_anproj_2 X1l1_collsp X1False)(∀X1, (v2_struct_0 X1False)(v7_anproj_2 X1False)(m1_subset_1 (esk16_1 X1) (u1_struct_0 X1)False)v2_collsp X1v3_collsp X1v4_collsp X1v2_anproj_2 X1v3_anproj_2 X1l1_collsp X1False)(∀X1, (v2_struct_0 X1False)(v7_anproj_2 X1False)(m1_subset_1 (esk15_1 X1) (u1_struct_0 X1)False)v2_collsp X1v3_collsp X1v4_collsp X1v2_anproj_2 X1v3_anproj_2 X1l1_collsp X1False)(∀X1, (v2_struct_0 X1False)(v7_anproj_2 X1False)(m1_subset_1 (esk14_1 X1) (u1_struct_0 X1)False)v2_collsp X1v3_collsp X1v4_collsp X1v2_anproj_2 X1v3_anproj_2 X1l1_collsp X1False)(∀X1, (v2_struct_0 X1False)(v7_anproj_2 X1False)(v5_anproj_2 X1False)v2_collsp X1v3_collsp X1v4_collsp X1v2_anproj_2 X1v3_anproj_2 X1l1_collsp X1False)(∀X1, (v2_struct_0 X1False)(v3_collsp X1False)(m1_subset_1 (esk25_1 X1) (u1_struct_0 X1)False)l1_collsp X1False)(∀X1, (v2_struct_0 X1False)(v3_collsp X1False)(m1_subset_1 (esk24_1 X1) (u1_struct_0 X1)False)l1_collsp X1False)(∀X1, (v2_struct_0 X1False)(v3_collsp X1False)(m1_subset_1 (esk23_1 X1) (u1_struct_0 X1)False)l1_collsp X1False)(∀X1, (v2_struct_0 X1False)(v3_collsp X1False)(m1_subset_1 (esk22_1 X1) (u1_struct_0 X1)False)l1_collsp X1False)(∀X1, (v2_struct_0 X1False)(v3_collsp X1False)(m1_subset_1 (esk21_1 X1) (u1_struct_0 X1)False)l1_collsp X1False)(∀X1, (v2_struct_0 X1False)(v2_collsp X1False)(m1_subset_1 (esk20_1 X1) (u1_struct_0 X1)False)l1_collsp X1False)(∀X1, (v2_struct_0 X1False)(v2_collsp X1False)(m1_subset_1 (esk19_1 X1) (u1_struct_0 X1)False)l1_collsp X1False)(∀X1, (v2_struct_0 X1False)(v2_collsp X1False)(m1_subset_1 (esk18_1 X1) (u1_struct_0 X1)False)l1_collsp X1False)(∀X1, (v2_struct_0 X1False)(v3_collsp X1False)(esk22_1 X1) = (esk21_1 X1)l1_collsp X1False)(∀X1, (l1_struct_0 X1False)l1_collsp X1False)(r1_collsp esk1_0 esk9_0 esk11_0 esk10_0False)(r1_collsp esk1_0 esk9_0 esk10_0 esk12_0False)(r1_collsp esk1_0 esk2_0 esk9_0 esk10_0False)(r1_collsp esk1_0 esk2_0 esk6_0 esk8_0False)(r1_collsp esk1_0 esk2_0 esk4_0 esk8_0False)(r1_collsp esk1_0 esk2_0 esk4_0 esk6_0False)(v2_struct_0 esk29_0False)(v2_struct_0 esk1_0False)(esk8_0 = esk7_0False)(esk7_0 = esk2_0False)(esk6_0 = esk5_0False)(esk5_0 = esk2_0False)(esk4_0 = esk3_0False)(esk3_0 = esk2_0False)((r1_collsp esk1_0 esk6_0 esk8_0 esk9_0False)False)((r1_collsp esk1_0 esk5_0 esk7_0 esk9_0False)False)((r1_collsp esk1_0 esk4_0 esk8_0 esk12_0False)False)((r1_collsp esk1_0 esk4_0 esk8_0 esk11_0False)False)((r1_collsp esk1_0 esk4_0 esk6_0 esk10_0False)False)((r1_collsp esk1_0 esk3_0 esk7_0 esk11_0False)False)((r1_collsp esk1_0 esk3_0 esk5_0 esk10_0False)False)((r1_collsp esk1_0 esk2_0 esk8_0 esk7_0False)False)((r1_collsp esk1_0 esk2_0 esk6_0 esk12_0False)False)((r1_collsp esk1_0 esk2_0 esk6_0 esk5_0False)False)((r1_collsp esk1_0 esk2_0 esk4_0 esk3_0False)False)(∀X1, (m1_subset_1 (esk28_1 X1) X1False)False)((m1_subset_1 esk12_0 (u1_struct_0 esk1_0)False)False)((m1_subset_1 esk11_0 (u1_struct_0 esk1_0)False)False)((m1_subset_1 esk10_0 (u1_struct_0 esk1_0)False)False)((m1_subset_1 esk9_0 (u1_struct_0 esk1_0)False)False)((m1_subset_1 esk8_0 (u1_struct_0 esk1_0)False)False)((m1_subset_1 esk7_0 (u1_struct_0 esk1_0)False)False)((m1_subset_1 esk6_0 (u1_struct_0 esk1_0)False)False)((m1_subset_1 esk5_0 (u1_struct_0 esk1_0)False)False)((m1_subset_1 esk4_0 (u1_struct_0 esk1_0)False)False)((m1_subset_1 esk3_0 (u1_struct_0 esk1_0)False)False)((m1_subset_1 esk2_0 (u1_struct_0 esk1_0)False)False)((l1_struct_0 esk27_0False)False)((l1_collsp esk29_0False)False)((l1_collsp esk26_0False)False)((l1_collsp esk1_0False)False)((v7_anproj_2 esk1_0False)False)((v6_anproj_2 esk1_0False)False)((v3_anproj_2 esk29_0False)False)((v3_anproj_2 esk1_0False)False)((v2_anproj_2 esk29_0False)False)((v2_anproj_2 esk1_0False)False)((v4_collsp esk29_0False)False)((v4_collsp esk1_0False)False)((v3_collsp esk29_0False)False)((v3_collsp esk1_0False)False)((v2_collsp esk29_0False)False)((v2_collsp esk1_0False)False)False
Proof:
The rest of the proof is missing.