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

------ Parsing...successful


------ Proving...
use I-

Gamma_0: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]

Gamma_1: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]

Gamma_2: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))

Gamma_3: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]

Gamma_4: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]

Gamma_5: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))

Gamma_6: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))

Gamma_7: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]

Gamma_8: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]

Gamma_9: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))

Gamma_10: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]

Gamma_11: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))

Gamma_12: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]

Gamma_13: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]

Gamma_14: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]

Gamma_15: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))

Gamma_16: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))

Gamma_17: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]

Gamma_18: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]

Gamma_19: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))

Gamma_20: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]

Gamma_21: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]

Gamma_22: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))

Gamma_23: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))
  23: [genlmt(c_basekb,c_universalvocabularymt)]

Gamma_24: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))
  23: [genlmt(c_basekb,c_universalvocabularymt)]
  24: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(
genlmt(c_basekb,c_universalvocabularymt))

Gamma_25: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))
  23: [genlmt(c_basekb,c_universalvocabularymt)]
  24: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(
genlmt(c_basekb,c_universalvocabularymt))
  25: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory(
c_universalvocabularymt)]

Gamma_26: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))
  23: [genlmt(c_basekb,c_universalvocabularymt)]
  24: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(
genlmt(c_basekb,c_universalvocabularymt))
  25: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory(
c_universalvocabularymt)]
  26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt))

Gamma_27: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))
  23: [genlmt(c_basekb,c_universalvocabularymt)]
  24: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(
genlmt(c_basekb,c_universalvocabularymt))
  25: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory(
c_universalvocabularymt)]
  26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt))
  27: [genlmt(c_calendarsmt,c_calendarsvocabularymt)]

Gamma_28: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))
  23: [genlmt(c_basekb,c_universalvocabularymt)]
  24: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(
genlmt(c_basekb,c_universalvocabularymt))
  25: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory(
c_universalvocabularymt)]
  26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt))
  27: [genlmt(c_calendarsmt,c_calendarsvocabularymt)]
  28: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_universalvocabularymt)]

Gamma_29: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))
  23: [genlmt(c_basekb,c_universalvocabularymt)]
  24: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(
genlmt(c_basekb,c_universalvocabularymt))
  25: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory(
c_universalvocabularymt)]
  26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt))
  27: [genlmt(c_calendarsmt,c_calendarsvocabularymt)]
  28: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_universalvocabularymt)]
  29: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt))

Gamma_30: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))
  23: [genlmt(c_basekb,c_universalvocabularymt)]
  24: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(
genlmt(c_basekb,c_universalvocabularymt))
  25: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory(
c_universalvocabularymt)]
  26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt))
  27: [genlmt(c_calendarsmt,c_calendarsvocabularymt)]
  28: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_universalvocabularymt)]
  29: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt))
  30: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_universalvocabularymt)]

Gamma_31: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))
  23: [genlmt(c_basekb,c_universalvocabularymt)]
  24: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(
genlmt(c_basekb,c_universalvocabularymt))
  25: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory(
c_universalvocabularymt)]
  26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt))
  27: [genlmt(c_calendarsmt,c_calendarsvocabularymt)]
  28: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_universalvocabularymt)]
  29: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt))
  30: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_universalvocabularymt)]
  31: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~(
genlmt(c_calendarsmt,c_universalvocabularymt))

Gamma_32: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))
  23: [genlmt(c_basekb,c_universalvocabularymt)]
  24: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(
genlmt(c_basekb,c_universalvocabularymt))
  25: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory(
c_universalvocabularymt)]
  26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt))
  27: [genlmt(c_calendarsmt,c_calendarsvocabularymt)]
  28: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_universalvocabularymt)]
  29: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt))
  30: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_universalvocabularymt)]
  31: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~(
genlmt(c_calendarsmt,c_universalvocabularymt))
  32: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_basekb)]

Gamma_33: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))
  23: [genlmt(c_basekb,c_universalvocabularymt)]
  24: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(
genlmt(c_basekb,c_universalvocabularymt))
  25: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory(
c_universalvocabularymt)]
  26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt))
  27: [genlmt(c_calendarsmt,c_calendarsvocabularymt)]
  28: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_universalvocabularymt)]
  29: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt))
  30: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_universalvocabularymt)]
  31: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~(
genlmt(c_calendarsmt,c_universalvocabularymt))
  32: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_basekb)]
  33: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_basekb)], ~(genlmt(c_calendarsmt,c_basekb))

Gamma_34: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))
  23: [genlmt(c_basekb,c_universalvocabularymt)]
  24: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(
genlmt(c_basekb,c_universalvocabularymt))
  25: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory(
c_universalvocabularymt)]
  26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt))
  27: [genlmt(c_calendarsmt,c_calendarsvocabularymt)]
  28: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_universalvocabularymt)]
  29: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt))
  30: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_universalvocabularymt)]
  31: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~(
genlmt(c_calendarsmt,c_universalvocabularymt))
  32: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_basekb)]
  33: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_basekb)], ~(genlmt(c_calendarsmt,c_basekb))
  34: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_basekb)]

Gamma_35: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))
  23: [genlmt(c_basekb,c_universalvocabularymt)]
  24: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(
genlmt(c_basekb,c_universalvocabularymt))
  25: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory(
c_universalvocabularymt)]
  26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt))
  27: [genlmt(c_calendarsmt,c_calendarsvocabularymt)]
  28: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_universalvocabularymt)]
  29: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt))
  30: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_universalvocabularymt)]
  31: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~(
genlmt(c_calendarsmt,c_universalvocabularymt))
  32: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_basekb)]
  33: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_basekb)], ~(genlmt(c_calendarsmt,c_basekb))
  34: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_basekb)]
  35: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~(
genlmt(c_calendarsmt,c_basekb))

Gamma_36: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))
  23: [genlmt(c_basekb,c_universalvocabularymt)]
  24: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(
genlmt(c_basekb,c_universalvocabularymt))
  25: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory(
c_universalvocabularymt)]
  26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt))
  27: [genlmt(c_calendarsmt,c_calendarsvocabularymt)]
  28: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_universalvocabularymt)]
  29: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt))
  30: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_universalvocabularymt)]
  31: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~(
genlmt(c_calendarsmt,c_universalvocabularymt))
  32: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_basekb)]
  33: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_basekb)], ~(genlmt(c_calendarsmt,c_basekb))
  34: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_basekb)]
  35: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~(
genlmt(c_calendarsmt,c_basekb))
  36: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(
genlmt(c_calendarsmt,c_calendarsvocabularymt))

Gamma_37: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))
  23: [genlmt(c_basekb,c_universalvocabularymt)]
  24: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(
genlmt(c_basekb,c_universalvocabularymt))
  25: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory(
c_universalvocabularymt)]
  26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt))
  27: [genlmt(c_calendarsmt,c_calendarsvocabularymt)]
  28: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_universalvocabularymt)]
  29: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt))
  30: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_universalvocabularymt)]
  31: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~(
genlmt(c_calendarsmt,c_universalvocabularymt))
  32: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_basekb)]
  33: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_basekb)], ~(genlmt(c_calendarsmt,c_basekb))
  34: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_basekb)]
  35: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~(
genlmt(c_calendarsmt,c_basekb))
  36: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(
genlmt(c_calendarsmt,c_calendarsvocabularymt))
  37: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsvocabularymt)]

Gamma_38: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))
  23: [genlmt(c_basekb,c_universalvocabularymt)]
  24: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(
genlmt(c_basekb,c_universalvocabularymt))
  25: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory(
c_universalvocabularymt)]
  26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt))
  27: [genlmt(c_calendarsmt,c_calendarsvocabularymt)]
  28: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_universalvocabularymt)]
  29: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt))
  30: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_universalvocabularymt)]
  31: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~(
genlmt(c_calendarsmt,c_universalvocabularymt))
  32: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_basekb)]
  33: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_basekb)], ~(genlmt(c_calendarsmt,c_basekb))
  34: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_basekb)]
  35: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~(
genlmt(c_calendarsmt,c_basekb))
  36: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(
genlmt(c_calendarsmt,c_calendarsvocabularymt))
  37: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsvocabularymt)]
  38: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(
genlmt(c_calendarsmt,c_calendarsvocabularymt))

Gamma_39: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))
  23: [genlmt(c_basekb,c_universalvocabularymt)]
  24: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(
genlmt(c_basekb,c_universalvocabularymt))
  25: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory(
c_universalvocabularymt)]
  26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt))
  27: [genlmt(c_calendarsmt,c_calendarsvocabularymt)]
  28: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_universalvocabularymt)]
  29: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt))
  30: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_universalvocabularymt)]
  31: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~(
genlmt(c_calendarsmt,c_universalvocabularymt))
  32: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_basekb)]
  33: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_basekb)], ~(genlmt(c_calendarsmt,c_basekb))
  34: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_basekb)]
  35: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~(
genlmt(c_calendarsmt,c_basekb))
  36: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(
genlmt(c_calendarsmt,c_calendarsvocabularymt))
  37: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsvocabularymt)]
  38: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(
genlmt(c_calendarsmt,c_calendarsvocabularymt))
  39: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible(
c_basekb)]

Gamma_40: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))
  23: [genlmt(c_basekb,c_universalvocabularymt)]
  24: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(
genlmt(c_basekb,c_universalvocabularymt))
  25: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory(
c_universalvocabularymt)]
  26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt))
  27: [genlmt(c_calendarsmt,c_calendarsvocabularymt)]
  28: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_universalvocabularymt)]
  29: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt))
  30: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_universalvocabularymt)]
  31: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~(
genlmt(c_calendarsmt,c_universalvocabularymt))
  32: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_basekb)]
  33: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_basekb)], ~(genlmt(c_calendarsmt,c_basekb))
  34: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_basekb)]
  35: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~(
genlmt(c_calendarsmt,c_basekb))
  36: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(
genlmt(c_calendarsmt,c_calendarsvocabularymt))
  37: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsvocabularymt)]
  38: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(
genlmt(c_calendarsmt,c_calendarsvocabularymt))
  39: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible(
c_basekb)]
  40: ~(genlmt(c_cyclistsmt,c_universalvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible(
c_universalvocabularymt)]

Gamma_41: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))
  23: [genlmt(c_basekb,c_universalvocabularymt)]
  24: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(
genlmt(c_basekb,c_universalvocabularymt))
  25: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory(
c_universalvocabularymt)]
  26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt))
  27: [genlmt(c_calendarsmt,c_calendarsvocabularymt)]
  28: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_universalvocabularymt)]
  29: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt))
  30: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_universalvocabularymt)]
  31: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~(
genlmt(c_calendarsmt,c_universalvocabularymt))
  32: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_basekb)]
  33: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_basekb)], ~(genlmt(c_calendarsmt,c_basekb))
  34: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_basekb)]
  35: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~(
genlmt(c_calendarsmt,c_basekb))
  36: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(
genlmt(c_calendarsmt,c_calendarsvocabularymt))
  37: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsvocabularymt)]
  38: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(
genlmt(c_calendarsmt,c_calendarsvocabularymt))
  39: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible(
c_basekb)]
  40: ~(genlmt(c_cyclistsmt,c_universalvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible(
c_universalvocabularymt)]
  41: ~(genlmt(c_cyclistsmt,c_calendarsvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible(
c_calendarsvocabularymt)]

Gamma_42: (extend-no-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))
  23: [genlmt(c_basekb,c_universalvocabularymt)]
  24: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(
genlmt(c_basekb,c_universalvocabularymt))
  25: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory(
c_universalvocabularymt)]
  26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt))
  27: [genlmt(c_calendarsmt,c_calendarsvocabularymt)]
  28: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_universalvocabularymt)]
  29: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt))
  30: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_universalvocabularymt)]
  31: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~(
genlmt(c_calendarsmt,c_universalvocabularymt))
  32: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_basekb)]
  33: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_basekb)], ~(genlmt(c_calendarsmt,c_basekb))
  34: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_basekb)]
  35: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~(
genlmt(c_calendarsmt,c_basekb))
  36: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(
genlmt(c_calendarsmt,c_calendarsvocabularymt))
  37: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsvocabularymt)]
  38: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(
genlmt(c_calendarsmt,c_calendarsvocabularymt))
  39: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible(
c_basekb)]
  40: ~(genlmt(c_cyclistsmt,c_universalvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible(
c_universalvocabularymt)]
  41: ~(genlmt(c_cyclistsmt,c_calendarsvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible(
c_calendarsvocabularymt)]
  42: [individual(c_tptptptpcol_16_25985)]

Gamma_43: (extend-conflict)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))
  23: [genlmt(c_basekb,c_universalvocabularymt)]
  24: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(
genlmt(c_basekb,c_universalvocabularymt))
  25: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory(
c_universalvocabularymt)]
  26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt))
  27: [genlmt(c_calendarsmt,c_calendarsvocabularymt)]
  28: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_universalvocabularymt)]
  29: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt))
  30: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_universalvocabularymt)]
  31: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~(
genlmt(c_calendarsmt,c_universalvocabularymt))
  32: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_basekb)]
  33: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_basekb)], ~(genlmt(c_calendarsmt,c_basekb))
  34: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_basekb)]
  35: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~(
genlmt(c_calendarsmt,c_basekb))
  36: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(
genlmt(c_calendarsmt,c_calendarsvocabularymt))
  37: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsvocabularymt)]
  38: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(
genlmt(c_calendarsmt,c_calendarsvocabularymt))
  39: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible(
c_basekb)]
  40: ~(genlmt(c_cyclistsmt,c_universalvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible(
c_universalvocabularymt)]
  41: ~(genlmt(c_cyclistsmt,c_calendarsvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible(
c_calendarsvocabularymt)]
  42: [individual(c_tptptptpcol_16_25985)]
  43: [~(individual(c_tptptptpcol_16_25985))]

Gamma_44: (move)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))
  23: [genlmt(c_basekb,c_universalvocabularymt)]
  24: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(
genlmt(c_basekb,c_universalvocabularymt))
  25: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory(
c_universalvocabularymt)]
  26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt))
  27: [genlmt(c_calendarsmt,c_calendarsvocabularymt)]
  28: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_universalvocabularymt)]
  29: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt))
  30: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_universalvocabularymt)]
  31: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~(
genlmt(c_calendarsmt,c_universalvocabularymt))
  32: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_basekb)]
  33: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_basekb)], ~(genlmt(c_calendarsmt,c_basekb))
  34: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_basekb)]
  35: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~(
genlmt(c_calendarsmt,c_basekb))
  36: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(
genlmt(c_calendarsmt,c_calendarsvocabularymt))
  37: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsvocabularymt)]
  38: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(
genlmt(c_calendarsmt,c_calendarsvocabularymt))
  39: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible(
c_basekb)]
  40: ~(genlmt(c_cyclistsmt,c_universalvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible(
c_universalvocabularymt)]
  41: ~(genlmt(c_cyclistsmt,c_calendarsvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible(
c_calendarsvocabularymt)]
  42: [~(individual(c_tptptptpcol_16_25985))]
  43: [individual(c_tptptptpcol_16_25985)]

Gamma_45: (resolve)
  0: [mtvisible(c_tptp_member2089_mt)]
  1: [genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)]
  2: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2089_mt))
  3: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member2089_mt)]
  4: ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  5: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  6: [genlmt(c_tptp_member2089_mt,c_tptp_member2089_mt)], ~(microtheory(c_tptp_member2089_mt))
  7: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  8: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_cyclistsmt)]
  9: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member2089_mt))
  10: ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  11: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  12: [genlmt(c_calendarsvocabularymt,c_basekb)]
  13: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)]
  14: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)]
  15: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb))
  16: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt))
  17: [genlmt(c_cyclistsmt,c_calendarsmt)]
  18: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2089_mt,c_cyclistsmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsmt)]
  19: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt,
c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt))
  20: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible(
c_calendarsmt)]
  21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)]
  22: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt))
  23: [genlmt(c_basekb,c_universalvocabularymt)]
  24: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(
genlmt(c_basekb,c_universalvocabularymt))
  25: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory(
c_universalvocabularymt)]
  26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt))
  27: [genlmt(c_calendarsmt,c_calendarsvocabularymt)]
  28: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_universalvocabularymt)]
  29: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt))
  30: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_universalvocabularymt)]
  31: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~(
genlmt(c_calendarsmt,c_universalvocabularymt))
  32: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt(
c_calendarsmt,c_basekb)]
  33: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt,
c_basekb)], ~(genlmt(c_calendarsmt,c_basekb))
  34: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_basekb)]
  35: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~(
genlmt(c_calendarsmt,c_basekb))
  36: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(
genlmt(c_calendarsmt,c_calendarsvocabularymt))
  37: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2089_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member2089_mt,c_calendarsvocabularymt)]
  38: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(
genlmt(c_calendarsmt,c_calendarsvocabularymt))
  39: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible(
c_basekb)]
  40: ~(genlmt(c_cyclistsmt,c_universalvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible(
c_universalvocabularymt)]
  41: ~(genlmt(c_cyclistsmt,c_calendarsvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible(
c_calendarsvocabularymt)]
  42: [~(individual(c_tptptptpcol_16_25985))]
  43: []

SZS status Unsatisfiable