%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------%

------ Parsing...successful


------ Proving...
use I-
not ground preserving

Gamma_0: (extend-no-conflict)
  0: [a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0))]

Gamma_1: (extend-no-conflict)
  0: [a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0))]
  1: [an_open_function_from_onto(the_projection_function(X0,X1,X2),the_product_top_space_over(X3,X2),
apply(X3,X0))]

Gamma_2: (extend-no-conflict)
  0: [a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0))]
  1: [an_open_function_from_onto(the_projection_function(X0,X1,X2),the_product_top_space_over(X3,X2),
apply(X3,X0))]
  2: [a_continuous_function_from_onto(the_projection_function(X0,X1,X2),
the_product_top_space_over(X1,X2),apply(X1,X0))]

Gamma_3: (extend-no-conflict)
  0: [a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0))]
  1: [an_open_function_from_onto(the_projection_function(X0,X1,X2),the_product_top_space_over(X3,X2),
apply(X3,X0))]
  2: [a_continuous_function_from_onto(the_projection_function(X0,X1,X2),
the_product_top_space_over(X1,X2),apply(X1,X0))]
  3: ~(an_open_function_from_onto(the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,X0))), ~(
a_continuous_function_from_onto(the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,X0))), [a_locally_compact_top_space(
apply(esk1_0,X0))], ~(a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))

Gamma_4: (extend-conflict)
  0: [a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0))]
  1: [an_open_function_from_onto(the_projection_function(X0,X1,X2),the_product_top_space_over(X3,X2),
apply(X3,X0))]
  2: [a_continuous_function_from_onto(the_projection_function(X0,X1,X2),
the_product_top_space_over(X1,X2),apply(X1,X0))]
  3: ~(an_open_function_from_onto(the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,X0))), ~(
a_continuous_function_from_onto(the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,X0))), [a_locally_compact_top_space(
apply(esk1_0,X0))], ~(a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))
  4: [~(a_locally_compact_top_space(apply(esk1_0,esk3_0)))]

Gamma_5: (move)
  0: [a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0))]
  1: [an_open_function_from_onto(the_projection_function(X0,X1,X2),the_product_top_space_over(X3,X2),
apply(X3,X0))]
  2: [a_continuous_function_from_onto(the_projection_function(X0,X1,X2),
the_product_top_space_over(X1,X2),apply(X1,X0))]
  3: [~(a_locally_compact_top_space(apply(esk1_0,esk3_0)))]
  4: ~(an_open_function_from_onto(the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,X0))), ~(
a_continuous_function_from_onto(the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,X0))), [a_locally_compact_top_space(
apply(esk1_0,X0))], ~(a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))

Gamma_6: (right-split)
  0: [a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0))]
  1: [an_open_function_from_onto(the_projection_function(X0,X1,X2),the_product_top_space_over(X3,X2),
apply(X3,X0))]
  2: [a_continuous_function_from_onto(the_projection_function(X0,X1,X2),
the_product_top_space_over(X1,X2),apply(X1,X0))]
  3: [~(a_locally_compact_top_space(apply(esk1_0,esk3_0)))]
  4: ~(an_open_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0))), ~(
a_continuous_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0))), [a_locally_compact_top_space(
apply(esk1_0,esk3_0))], ~(a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))
  5: top(X0) != esk3_0 | ~(an_open_function_from_onto(the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,X0))), ~(
a_continuous_function_from_onto(the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,X0))), [a_locally_compact_top_space(
apply(esk1_0,X0))], ~(a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))

Gamma_7: (right-split)
  0: [a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0))]
  1: [an_open_function_from_onto(the_projection_function(X0,X1,X2),the_product_top_space_over(X3,X2),
apply(X3,X0))]
  2: [a_continuous_function_from_onto(the_projection_function(X0,X1,X2),
the_product_top_space_over(X1,X2),apply(X1,X0))]
  3: [~(a_locally_compact_top_space(apply(esk1_0,esk3_0)))]
  4: ~(an_open_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0))), ~(
a_continuous_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0))), [a_locally_compact_top_space(
apply(esk1_0,esk3_0))], ~(a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))
  5: top(X0) != esk3_0 | ~(an_open_function_from_onto(the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,X0))), ~(
a_continuous_function_from_onto(the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,X0))), [a_locally_compact_top_space(
apply(esk1_0,X0))], ~(a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))

Gamma_8: (resolve)
  0: [a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0))]
  1: [an_open_function_from_onto(the_projection_function(X0,X1,X2),the_product_top_space_over(X3,X2),
apply(X3,X0))]
  2: [a_continuous_function_from_onto(the_projection_function(X0,X1,X2),
the_product_top_space_over(X1,X2),apply(X1,X0))]
  3: [~(a_locally_compact_top_space(apply(esk1_0,esk3_0)))]
  4: [~(an_open_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0)))], ~(
a_continuous_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0))), ~(
a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))
  5: top(X0) != esk3_0 | ~(an_open_function_from_onto(the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,X0))), ~(
a_continuous_function_from_onto(the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,X0))), [a_locally_compact_top_space(
apply(esk1_0,X0))], ~(a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))

Gamma_9: (extend-conflict)
  0: [a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0))]
  1: [an_open_function_from_onto(the_projection_function(X0,X1,X2),the_product_top_space_over(X3,X2),
apply(X3,X0))]
  2: [a_continuous_function_from_onto(the_projection_function(X0,X1,X2),
the_product_top_space_over(X1,X2),apply(X1,X0))]
  3: [~(a_locally_compact_top_space(apply(esk1_0,esk3_0)))]
  4: ~(an_open_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0))), [~(
a_continuous_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0)))], ~(
a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))
  5: top(X0) != esk3_0 | ~(an_open_function_from_onto(the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,X0))), ~(
a_continuous_function_from_onto(the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,X0))), [a_locally_compact_top_space(
apply(esk1_0,X0))], ~(a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))

Gamma_10: (move)
  0: [a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0))]
  1: [an_open_function_from_onto(the_projection_function(X0,X1,X2),the_product_top_space_over(X3,X2),
apply(X3,X0))]
  2: ~(an_open_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0))), [~(
a_continuous_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0)))], ~(
a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))
  3: [a_continuous_function_from_onto(the_projection_function(X0,X1,X2),
the_product_top_space_over(X1,X2),apply(X1,X0))]
  4: [~(a_locally_compact_top_space(apply(esk1_0,esk3_0)))]
  5: top(X0) != esk3_0 | ~(an_open_function_from_onto(the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,X0))), ~(
a_continuous_function_from_onto(the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,X0))), [a_locally_compact_top_space(
apply(esk1_0,X0))], ~(a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))

Gamma_11: (right-split)
  0: [a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0))]
  1: [an_open_function_from_onto(the_projection_function(X0,X1,X2),the_product_top_space_over(X3,X2),
apply(X3,X0))]
  2: ~(an_open_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0))), [~(
a_continuous_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0)))], ~(
a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))
  3: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 | [a_continuous_function_from_onto(
the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,esk3_0))]
  4: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,X0))]
  5: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X1) != esk1_0 | [a_continuous_function_from_onto(
the_projection_function(esk3_0,X0,esk2_0),the_product_top_space_over(X0,esk2_0),
apply(X0,esk3_0))]
  6: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,X1,esk2_0),the_product_top_space_over(X1,esk2_0),
apply(X1,X0))]
  7: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 | [a_continuous_function_from_onto(
the_projection_function(esk3_0,esk1_0,X0),the_product_top_space_over(esk1_0,X0),
apply(esk1_0,esk3_0))]
  8: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,esk1_0,X1),the_product_top_space_over(esk1_0,X1),
apply(esk1_0,X0))]
  9: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 | [a_continuous_function_from_onto(
the_projection_function(esk3_0,X0,X1),the_product_top_space_over(X0,X1),
apply(X0,esk3_0))]
  10: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,X1,X2),the_product_top_space_over(X1,X2),apply(X1,X0))]
  11: [~(a_locally_compact_top_space(apply(esk1_0,esk3_0)))]
  12: top(X0) != esk3_0 | ~(an_open_function_from_onto(the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,X0))), ~(
a_continuous_function_from_onto(the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,X0))), [a_locally_compact_top_space(
apply(esk1_0,X0))], ~(a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))

Gamma_12: (right-split)
  0: [a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0))]
  1: [an_open_function_from_onto(the_projection_function(X0,X1,X2),the_product_top_space_over(X3,X2),
apply(X3,X0))]
  2: ~(an_open_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0))), [~(
a_continuous_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0)))], ~(
a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))
  3: [a_continuous_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),
the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0))]
  4: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,X0))]
  5: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X1) != esk1_0 | [a_continuous_function_from_onto(
the_projection_function(esk3_0,X0,esk2_0),the_product_top_space_over(X0,esk2_0),
apply(X0,esk3_0))]
  6: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,X1,esk2_0),the_product_top_space_over(X1,esk2_0),
apply(X1,X0))]
  7: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 | [a_continuous_function_from_onto(
the_projection_function(esk3_0,esk1_0,X0),the_product_top_space_over(esk1_0,X0),
apply(esk1_0,esk3_0))]
  8: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,esk1_0,X1),the_product_top_space_over(esk1_0,X1),
apply(esk1_0,X0))]
  9: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 | [a_continuous_function_from_onto(
the_projection_function(esk3_0,X0,X1),the_product_top_space_over(X0,X1),
apply(X0,esk3_0))]
  10: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,X1,X2),the_product_top_space_over(X1,X2),apply(X1,X0))]
  11: [~(a_locally_compact_top_space(apply(esk1_0,esk3_0)))]
  12: top(X0) != esk3_0 | ~(an_open_function_from_onto(the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,X0))), ~(
a_continuous_function_from_onto(the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,X0))), [a_locally_compact_top_space(
apply(esk1_0,X0))], ~(a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))

Gamma_13: (resolve)
  0: [a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0))]
  1: [an_open_function_from_onto(the_projection_function(X0,X1,X2),the_product_top_space_over(X3,X2),
apply(X3,X0))]
  2: ~(an_open_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0))), [~(
a_continuous_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0)))], ~(
a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))
  3: [~(an_open_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0)))], ~(
a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))
  4: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,X0))]
  5: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X1) != esk1_0 | [a_continuous_function_from_onto(
the_projection_function(esk3_0,X0,esk2_0),the_product_top_space_over(X0,esk2_0),
apply(X0,esk3_0))]
  6: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,X1,esk2_0),the_product_top_space_over(X1,esk2_0),
apply(X1,X0))]
  7: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 | [a_continuous_function_from_onto(
the_projection_function(esk3_0,esk1_0,X0),the_product_top_space_over(esk1_0,X0),
apply(esk1_0,esk3_0))]
  8: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,esk1_0,X1),the_product_top_space_over(esk1_0,X1),
apply(esk1_0,X0))]
  9: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 | [a_continuous_function_from_onto(
the_projection_function(esk3_0,X0,X1),the_product_top_space_over(X0,X1),
apply(X0,esk3_0))]
  10: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,X1,X2),the_product_top_space_over(X1,X2),apply(X1,X0))]
  11: [~(a_locally_compact_top_space(apply(esk1_0,esk3_0)))]

Gamma_14: (extend-conflict)
  0: [a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0))]
  1: [an_open_function_from_onto(the_projection_function(X0,X1,X2),the_product_top_space_over(X3,X2),
apply(X3,X0))]
  2: ~(an_open_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0))), [~(
a_continuous_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0)))], ~(
a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))
  3: [~(an_open_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0)))], ~(
a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))
  4: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,X0))]
  5: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X1) != esk1_0 | [a_continuous_function_from_onto(
the_projection_function(esk3_0,X0,esk2_0),the_product_top_space_over(X0,esk2_0),
apply(X0,esk3_0))]
  6: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,X1,esk2_0),the_product_top_space_over(X1,esk2_0),
apply(X1,X0))]
  7: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 | [a_continuous_function_from_onto(
the_projection_function(esk3_0,esk1_0,X0),the_product_top_space_over(esk1_0,X0),
apply(esk1_0,esk3_0))]
  8: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,esk1_0,X1),the_product_top_space_over(esk1_0,X1),
apply(esk1_0,X0))]
  9: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 | [a_continuous_function_from_onto(
the_projection_function(esk3_0,X0,X1),the_product_top_space_over(X0,X1),
apply(X0,esk3_0))]
  10: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,X1,X2),the_product_top_space_over(X1,X2),apply(X1,X0))]
  11: [~(a_locally_compact_top_space(apply(esk1_0,esk3_0)))]

Gamma_15: (move)
  0: [a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0))]
  1: [~(an_open_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0)))], ~(
a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))
  2: [an_open_function_from_onto(the_projection_function(X0,X1,X2),the_product_top_space_over(X3,X2),
apply(X3,X0))]
  3: ~(an_open_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0))), [~(
a_continuous_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0)))], ~(
a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))
  4: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,X0))]
  5: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X1) != esk1_0 | [a_continuous_function_from_onto(
the_projection_function(esk3_0,X0,esk2_0),the_product_top_space_over(X0,esk2_0),
apply(X0,esk3_0))]
  6: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,X1,esk2_0),the_product_top_space_over(X1,esk2_0),
apply(X1,X0))]
  7: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 | [a_continuous_function_from_onto(
the_projection_function(esk3_0,esk1_0,X0),the_product_top_space_over(esk1_0,X0),
apply(esk1_0,esk3_0))]
  8: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,esk1_0,X1),the_product_top_space_over(esk1_0,X1),
apply(esk1_0,X0))]
  9: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 | [a_continuous_function_from_onto(
the_projection_function(esk3_0,X0,X1),the_product_top_space_over(X0,X1),
apply(X0,esk3_0))]
  10: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,X1,X2),the_product_top_space_over(X1,X2),apply(X1,X0))]
  11: [~(a_locally_compact_top_space(apply(esk1_0,esk3_0)))]

Gamma_16: (right-split)
  0: [a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0))]
  1: [~(an_open_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0)))], ~(
a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))
  2: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,esk3_0))]
  3: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,X0))]
  4: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,X0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,esk3_0))]
  5: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,X1,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,X0))]
  6: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X2) != esk2_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,esk1_0,X0),the_product_top_space_over(esk1_0,X0),
apply(esk1_0,esk3_0))]
  7: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X2) != esk2_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,esk1_0,X1),the_product_top_space_over(esk1_0,X1),
apply(esk1_0,X0))]
  8: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X2) != esk2_0 & top(X1) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,X0,X1),the_product_top_space_over(esk1_0,X1),
apply(esk1_0,esk3_0))]
  9: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,X1,X2),the_product_top_space_over(esk1_0,X2),
apply(esk1_0,X0))]
  10: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(X0,esk2_0),
apply(X0,esk3_0))]
  11: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(X1,esk2_0),
apply(X1,X0))]
  12: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X1) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,X0,esk2_0),the_product_top_space_over(X1,esk2_0),
apply(X1,esk3_0))]
  13: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,X1,esk2_0),the_product_top_space_over(X2,esk2_0),
apply(X2,X0))]
  14: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X2) != esk2_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,esk1_0,X0),the_product_top_space_over(X1,X0),
apply(X1,esk3_0))]
  15: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,esk1_0,X1),the_product_top_space_over(X2,X1),
apply(X2,X0))]
  16: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,X0,X1),the_product_top_space_over(X2,X1),
apply(X2,esk3_0))]
  17: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,X1,X2),the_product_top_space_over(X3,X2),apply(X3,X0))]
  18: ~(an_open_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0))), [~(
a_continuous_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0)))], ~(
a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))
  19: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,X0))]
  20: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X1) != esk1_0 | [a_continuous_function_from_onto(
the_projection_function(esk3_0,X0,esk2_0),the_product_top_space_over(X0,esk2_0),
apply(X0,esk3_0))]
  21: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,X1,esk2_0),the_product_top_space_over(X1,esk2_0),
apply(X1,X0))]
  22: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 | [a_continuous_function_from_onto(
the_projection_function(esk3_0,esk1_0,X0),the_product_top_space_over(esk1_0,X0),
apply(esk1_0,esk3_0))]
  23: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,esk1_0,X1),the_product_top_space_over(esk1_0,X1),
apply(esk1_0,X0))]
  24: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 | [a_continuous_function_from_onto(
the_projection_function(esk3_0,X0,X1),the_product_top_space_over(X0,X1),
apply(X0,esk3_0))]
  25: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,X1,X2),the_product_top_space_over(X1,X2),apply(X1,X0))]
  26: [~(a_locally_compact_top_space(apply(esk1_0,esk3_0)))]

Gamma_17: (right-split)
  0: [a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0))]
  1: [~(an_open_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0)))], ~(
a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))
  2: [an_open_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),
the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0))]
  3: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,X0))]
  4: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,X0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,esk3_0))]
  5: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,X1,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,X0))]
  6: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X2) != esk2_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,esk1_0,X0),the_product_top_space_over(esk1_0,X0),
apply(esk1_0,esk3_0))]
  7: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X2) != esk2_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,esk1_0,X1),the_product_top_space_over(esk1_0,X1),
apply(esk1_0,X0))]
  8: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X2) != esk2_0 & top(X1) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,X0,X1),the_product_top_space_over(esk1_0,X1),
apply(esk1_0,esk3_0))]
  9: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,X1,X2),the_product_top_space_over(esk1_0,X2),
apply(esk1_0,X0))]
  10: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(X0,esk2_0),
apply(X0,esk3_0))]
  11: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(X1,esk2_0),
apply(X1,X0))]
  12: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X1) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,X0,esk2_0),the_product_top_space_over(X1,esk2_0),
apply(X1,esk3_0))]
  13: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,X1,esk2_0),the_product_top_space_over(X2,esk2_0),
apply(X2,X0))]
  14: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X2) != esk2_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,esk1_0,X0),the_product_top_space_over(X1,X0),
apply(X1,esk3_0))]
  15: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,esk1_0,X1),the_product_top_space_over(X2,X1),
apply(X2,X0))]
  16: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,X0,X1),the_product_top_space_over(X2,X1),
apply(X2,esk3_0))]
  17: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,X1,X2),the_product_top_space_over(X3,X2),apply(X3,X0))]
  18: ~(an_open_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0))), [~(
a_continuous_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0)))], ~(
a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))
  19: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,X0))]
  20: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X1) != esk1_0 | [a_continuous_function_from_onto(
the_projection_function(esk3_0,X0,esk2_0),the_product_top_space_over(X0,esk2_0),
apply(X0,esk3_0))]
  21: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,X1,esk2_0),the_product_top_space_over(X1,esk2_0),
apply(X1,X0))]
  22: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 | [a_continuous_function_from_onto(
the_projection_function(esk3_0,esk1_0,X0),the_product_top_space_over(esk1_0,X0),
apply(esk1_0,esk3_0))]
  23: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,esk1_0,X1),the_product_top_space_over(esk1_0,X1),
apply(esk1_0,X0))]
  24: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 | [a_continuous_function_from_onto(
the_projection_function(esk3_0,X0,X1),the_product_top_space_over(X0,X1),
apply(X0,esk3_0))]
  25: top(X0) != esk3_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [a_continuous_function_from_onto(
the_projection_function(X0,X1,X2),the_product_top_space_over(X1,X2),apply(X1,X0))]
  26: [~(a_locally_compact_top_space(apply(esk1_0,esk3_0)))]

Gamma_18: (resolve)
  0: [a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0))]
  1: [~(an_open_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0)))], ~(
a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))
  2: [~(a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))]
  3: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,X0))]
  4: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,X0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,esk3_0))]
  5: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,X1,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,X0))]
  6: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X2) != esk2_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,esk1_0,X0),the_product_top_space_over(esk1_0,X0),
apply(esk1_0,esk3_0))]
  7: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X2) != esk2_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,esk1_0,X1),the_product_top_space_over(esk1_0,X1),
apply(esk1_0,X0))]
  8: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X2) != esk2_0 & top(X1) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,X0,X1),the_product_top_space_over(esk1_0,X1),
apply(esk1_0,esk3_0))]
  9: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,X1,X2),the_product_top_space_over(esk1_0,X2),
apply(esk1_0,X0))]
  10: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(X0,esk2_0),
apply(X0,esk3_0))]
  11: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(X1,esk2_0),
apply(X1,X0))]
  12: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X1) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,X0,esk2_0),the_product_top_space_over(X1,esk2_0),
apply(X1,esk3_0))]
  13: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,X1,esk2_0),the_product_top_space_over(X2,esk2_0),
apply(X2,X0))]
  14: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X2) != esk2_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,esk1_0,X0),the_product_top_space_over(X1,X0),
apply(X1,esk3_0))]
  15: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,esk1_0,X1),the_product_top_space_over(X2,X1),
apply(X2,X0))]
  16: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,X0,X1),the_product_top_space_over(X2,X1),
apply(X2,esk3_0))]
  17: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,X1,X2),the_product_top_space_over(X3,X2),apply(X3,X0))]
  18: [~(a_locally_compact_top_space(apply(esk1_0,esk3_0)))]

Gamma_19: (extend-conflict)
  0: [a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0))]
  1: [~(an_open_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0)))], ~(
a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))
  2: [~(a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))]
  3: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,X0))]
  4: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,X0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,esk3_0))]
  5: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,X1,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,X0))]
  6: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X2) != esk2_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,esk1_0,X0),the_product_top_space_over(esk1_0,X0),
apply(esk1_0,esk3_0))]
  7: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X2) != esk2_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,esk1_0,X1),the_product_top_space_over(esk1_0,X1),
apply(esk1_0,X0))]
  8: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X2) != esk2_0 & top(X1) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,X0,X1),the_product_top_space_over(esk1_0,X1),
apply(esk1_0,esk3_0))]
  9: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,X1,X2),the_product_top_space_over(esk1_0,X2),
apply(esk1_0,X0))]
  10: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(X0,esk2_0),
apply(X0,esk3_0))]
  11: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(X1,esk2_0),
apply(X1,X0))]
  12: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X1) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,X0,esk2_0),the_product_top_space_over(X1,esk2_0),
apply(X1,esk3_0))]
  13: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,X1,esk2_0),the_product_top_space_over(X2,esk2_0),
apply(X2,X0))]
  14: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X2) != esk2_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,esk1_0,X0),the_product_top_space_over(X1,X0),
apply(X1,esk3_0))]
  15: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,esk1_0,X1),the_product_top_space_over(X2,X1),
apply(X2,X0))]
  16: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,X0,X1),the_product_top_space_over(X2,X1),
apply(X2,esk3_0))]
  17: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,X1,X2),the_product_top_space_over(X3,X2),apply(X3,X0))]
  18: [~(a_locally_compact_top_space(apply(esk1_0,esk3_0)))]

Gamma_20: (move)
  0: [~(a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))]
  1: [a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0))]
  2: [~(an_open_function_from_onto(the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),apply(esk1_0,esk3_0)))], ~(
a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))
  3: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,X0))]
  4: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,X0,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,esk3_0))]
  5: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,X1,esk2_0),the_product_top_space_over(esk1_0,esk2_0),
apply(esk1_0,X0))]
  6: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X2) != esk2_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,esk1_0,X0),the_product_top_space_over(esk1_0,X0),
apply(esk1_0,esk3_0))]
  7: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X2) != esk2_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,esk1_0,X1),the_product_top_space_over(esk1_0,X1),
apply(esk1_0,X0))]
  8: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X2) != esk2_0 & top(X1) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,X0,X1),the_product_top_space_over(esk1_0,X1),
apply(esk1_0,esk3_0))]
  9: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,X1,X2),the_product_top_space_over(esk1_0,X2),
apply(esk1_0,X0))]
  10: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,esk1_0,esk2_0),the_product_top_space_over(X0,esk2_0),
apply(X0,esk3_0))]
  11: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,esk1_0,esk2_0),the_product_top_space_over(X1,esk2_0),
apply(X1,X0))]
  12: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X1) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,X0,esk2_0),the_product_top_space_over(X1,esk2_0),
apply(X1,esk3_0))]
  13: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,X1,esk2_0),the_product_top_space_over(X2,esk2_0),
apply(X2,X0))]
  14: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X2) != esk2_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,esk1_0,X0),the_product_top_space_over(X1,X0),
apply(X1,esk3_0))]
  15: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,esk1_0,X1),the_product_top_space_over(X2,X1),
apply(X2,X0))]
  16: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 | [an_open_function_from_onto(
the_projection_function(esk3_0,X0,X1),the_product_top_space_over(X2,X1),
apply(X2,esk3_0))]
  17: top(X0) != esk3_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X3) != esk1_0 & top(X2) != esk2_0 & top(X1) != esk1_0 & top(X0) != esk3_0 | [an_open_function_from_onto(
the_projection_function(X0,X1,X2),the_product_top_space_over(X3,X2),apply(X3,X0))]
  18: [~(a_locally_compact_top_space(apply(esk1_0,esk3_0)))]

Gamma_21: (resolve)
  0: [~(a_locally_compact_top_space(the_product_top_space_over(esk1_0,esk2_0)))]
  1: []
  2: [~(a_locally_compact_top_space(apply(esk1_0,esk3_0)))]

SZS status Unsatisfiable