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

------ Parsing...successful


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

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

Gamma_1: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]

Gamma_2: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]

Gamma_3: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]

Gamma_4: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))

Gamma_5: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))

Gamma_6: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]

Gamma_7: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]

Gamma_8: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]

Gamma_9: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]

Gamma_10: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]

Gamma_11: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))

Gamma_12: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))

Gamma_13: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))

Gamma_14: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]

Gamma_15: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]

Gamma_16: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  16: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member3717_mt))

Gamma_17: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  16: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member3717_mt))
  17: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]

Gamma_18: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  16: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member3717_mt))
  17: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  18: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))

Gamma_19: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  16: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member3717_mt))
  17: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  18: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  19: [artsupplies(c_tptpartsupplies)], ~(mtvisible(c_cyclistsmt))

Gamma_20: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  16: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member3717_mt))
  17: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  18: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  19: [artsupplies(c_tptpartsupplies)], ~(mtvisible(c_cyclistsmt))
  20: [isa(c_tptpartsupplies,c_artsupplies)], ~(artsupplies(c_tptpartsupplies))

Gamma_21: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  16: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member3717_mt))
  17: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  18: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  19: [artsupplies(c_tptpartsupplies)], ~(mtvisible(c_cyclistsmt))
  20: [isa(c_tptpartsupplies,c_artsupplies)], ~(artsupplies(c_tptpartsupplies))
  21: ~(isa(c_tptpartsupplies,c_artsupplies)), [thing(c_tptpartsupplies)]

Gamma_22: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  16: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member3717_mt))
  17: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  18: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  19: [artsupplies(c_tptpartsupplies)], ~(mtvisible(c_cyclistsmt))
  20: [isa(c_tptpartsupplies,c_artsupplies)], ~(artsupplies(c_tptpartsupplies))
  21: ~(isa(c_tptpartsupplies,c_artsupplies)), [thing(c_tptpartsupplies)]
  22: ~(isa(c_tptpartsupplies,c_artsupplies)), [collection(c_artsupplies)]

Gamma_23: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  16: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member3717_mt))
  17: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  18: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  19: [artsupplies(c_tptpartsupplies)], ~(mtvisible(c_cyclistsmt))
  20: [isa(c_tptpartsupplies,c_artsupplies)], ~(artsupplies(c_tptpartsupplies))
  21: ~(isa(c_tptpartsupplies,c_artsupplies)), [thing(c_tptpartsupplies)]
  22: ~(isa(c_tptpartsupplies,c_artsupplies)), [collection(c_artsupplies)]
  23: [genls(c_artsupplies,c_artsupplies)], ~(collection(c_artsupplies))

Gamma_24: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  16: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member3717_mt))
  17: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  18: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  19: [artsupplies(c_tptpartsupplies)], ~(mtvisible(c_cyclistsmt))
  20: [isa(c_tptpartsupplies,c_artsupplies)], ~(artsupplies(c_tptpartsupplies))
  21: ~(isa(c_tptpartsupplies,c_artsupplies)), [thing(c_tptpartsupplies)]
  22: ~(isa(c_tptpartsupplies,c_artsupplies)), [collection(c_artsupplies)]
  23: [genls(c_artsupplies,c_artsupplies)], ~(collection(c_artsupplies))
  24: [supplies(c_tptpartsupplies)], ~(artsupplies(c_tptpartsupplies))

Gamma_25: (extend-no-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  16: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member3717_mt))
  17: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  18: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  19: [artsupplies(c_tptpartsupplies)], ~(mtvisible(c_cyclistsmt))
  20: [isa(c_tptpartsupplies,c_artsupplies)], ~(artsupplies(c_tptpartsupplies))
  21: ~(isa(c_tptpartsupplies,c_artsupplies)), [thing(c_tptpartsupplies)]
  22: ~(isa(c_tptpartsupplies,c_artsupplies)), [collection(c_artsupplies)]
  23: [genls(c_artsupplies,c_artsupplies)], ~(collection(c_artsupplies))
  24: [supplies(c_tptpartsupplies)], ~(artsupplies(c_tptpartsupplies))
  25: [tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232))], ~(
supplies(c_tptpartsupplies)), ~(mtvisible(c_tptp_spindleheadmt))

Gamma_26: (extend-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  16: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member3717_mt))
  17: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  18: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  19: [artsupplies(c_tptpartsupplies)], ~(mtvisible(c_cyclistsmt))
  20: [isa(c_tptpartsupplies,c_artsupplies)], ~(artsupplies(c_tptpartsupplies))
  21: ~(isa(c_tptpartsupplies,c_artsupplies)), [thing(c_tptpartsupplies)]
  22: ~(isa(c_tptpartsupplies,c_artsupplies)), [collection(c_artsupplies)]
  23: [genls(c_artsupplies,c_artsupplies)], ~(collection(c_artsupplies))
  24: [supplies(c_tptpartsupplies)], ~(artsupplies(c_tptpartsupplies))
  25: [tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232))], ~(
supplies(c_tptpartsupplies)), ~(mtvisible(c_tptp_spindleheadmt))
  26: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

Gamma_27: (move)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  16: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member3717_mt))
  17: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  18: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  19: [artsupplies(c_tptpartsupplies)], ~(mtvisible(c_cyclistsmt))
  20: [isa(c_tptpartsupplies,c_artsupplies)], ~(artsupplies(c_tptpartsupplies))
  21: ~(isa(c_tptpartsupplies,c_artsupplies)), [thing(c_tptpartsupplies)]
  22: ~(isa(c_tptpartsupplies,c_artsupplies)), [collection(c_artsupplies)]
  23: [genls(c_artsupplies,c_artsupplies)], ~(collection(c_artsupplies))
  24: [supplies(c_tptpartsupplies)], ~(artsupplies(c_tptpartsupplies))
  25: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]
  26: [tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232))], ~(
supplies(c_tptpartsupplies)), ~(mtvisible(c_tptp_spindleheadmt))

Gamma_28: (resolve)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  16: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member3717_mt))
  17: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  18: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  19: [artsupplies(c_tptpartsupplies)], ~(mtvisible(c_cyclistsmt))
  20: [isa(c_tptpartsupplies,c_artsupplies)], ~(artsupplies(c_tptpartsupplies))
  21: ~(isa(c_tptpartsupplies,c_artsupplies)), [thing(c_tptpartsupplies)]
  22: ~(isa(c_tptpartsupplies,c_artsupplies)), [collection(c_artsupplies)]
  23: [genls(c_artsupplies,c_artsupplies)], ~(collection(c_artsupplies))
  24: [supplies(c_tptpartsupplies)], ~(artsupplies(c_tptpartsupplies))
  25: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]
  26: [~(supplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))

Gamma_29: (extend-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  16: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member3717_mt))
  17: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  18: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  19: [artsupplies(c_tptpartsupplies)], ~(mtvisible(c_cyclistsmt))
  20: [isa(c_tptpartsupplies,c_artsupplies)], ~(artsupplies(c_tptpartsupplies))
  21: ~(isa(c_tptpartsupplies,c_artsupplies)), [thing(c_tptpartsupplies)]
  22: ~(isa(c_tptpartsupplies,c_artsupplies)), [collection(c_artsupplies)]
  23: [genls(c_artsupplies,c_artsupplies)], ~(collection(c_artsupplies))
  24: [supplies(c_tptpartsupplies)], ~(artsupplies(c_tptpartsupplies))
  25: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]
  26: [~(supplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))

Gamma_30: (move)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  16: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member3717_mt))
  17: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  18: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  19: [artsupplies(c_tptpartsupplies)], ~(mtvisible(c_cyclistsmt))
  20: [isa(c_tptpartsupplies,c_artsupplies)], ~(artsupplies(c_tptpartsupplies))
  21: ~(isa(c_tptpartsupplies,c_artsupplies)), [thing(c_tptpartsupplies)]
  22: ~(isa(c_tptpartsupplies,c_artsupplies)), [collection(c_artsupplies)]
  23: [genls(c_artsupplies,c_artsupplies)], ~(collection(c_artsupplies))
  24: [~(supplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  25: [supplies(c_tptpartsupplies)], ~(artsupplies(c_tptpartsupplies))
  26: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

Gamma_31: (resolve)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  16: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member3717_mt))
  17: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  18: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  19: [artsupplies(c_tptpartsupplies)], ~(mtvisible(c_cyclistsmt))
  20: [isa(c_tptpartsupplies,c_artsupplies)], ~(artsupplies(c_tptpartsupplies))
  21: ~(isa(c_tptpartsupplies,c_artsupplies)), [thing(c_tptpartsupplies)]
  22: ~(isa(c_tptpartsupplies,c_artsupplies)), [collection(c_artsupplies)]
  23: [genls(c_artsupplies,c_artsupplies)], ~(collection(c_artsupplies))
  24: [~(supplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  25: [~(artsupplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  26: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

Gamma_32: (extend-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  16: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member3717_mt))
  17: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  18: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  19: [artsupplies(c_tptpartsupplies)], ~(mtvisible(c_cyclistsmt))
  20: [isa(c_tptpartsupplies,c_artsupplies)], ~(artsupplies(c_tptpartsupplies))
  21: ~(isa(c_tptpartsupplies,c_artsupplies)), [thing(c_tptpartsupplies)]
  22: ~(isa(c_tptpartsupplies,c_artsupplies)), [collection(c_artsupplies)]
  23: [genls(c_artsupplies,c_artsupplies)], ~(collection(c_artsupplies))
  24: [~(supplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  25: [~(artsupplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  26: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

Gamma_33: (move)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  16: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member3717_mt))
  17: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  18: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  19: [~(artsupplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  20: [artsupplies(c_tptpartsupplies)], ~(mtvisible(c_cyclistsmt))
  21: [isa(c_tptpartsupplies,c_artsupplies)], ~(artsupplies(c_tptpartsupplies))
  22: ~(isa(c_tptpartsupplies,c_artsupplies)), [thing(c_tptpartsupplies)]
  23: ~(isa(c_tptpartsupplies,c_artsupplies)), [collection(c_artsupplies)]
  24: [genls(c_artsupplies,c_artsupplies)], ~(collection(c_artsupplies))
  25: [~(supplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  26: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

Gamma_34: (resolve)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  16: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member3717_mt))
  17: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  18: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  19: [~(artsupplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  20: ~(mtvisible(c_tptp_spindleheadmt)), [~(mtvisible(c_cyclistsmt))]
  21: [~(supplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  22: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

Gamma_35: (extend-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  16: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member3717_mt))
  17: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  18: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  19: [~(artsupplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  20: ~(mtvisible(c_tptp_spindleheadmt)), [~(mtvisible(c_cyclistsmt))]
  21: [~(supplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  22: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

Gamma_36: (move)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  16: ~(mtvisible(c_tptp_spindleheadmt)), [~(mtvisible(c_cyclistsmt))]
  17: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~(
mtvisible(c_tptp_member3717_mt))
  18: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  19: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  20: [~(artsupplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  21: [~(supplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  22: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

Gamma_37: (resolve)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  16: ~(mtvisible(c_tptp_spindleheadmt)), [~(mtvisible(c_cyclistsmt))]
  17: [~(genlmt(c_tptp_member3717_mt,c_cyclistsmt))], ~(mtvisible(c_tptp_spindleheadmt)), ~(
mtvisible(c_tptp_member3717_mt))
  18: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  19: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  20: [~(artsupplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  21: [~(supplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  22: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

Gamma_38: (extend-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  16: ~(mtvisible(c_tptp_spindleheadmt)), [~(mtvisible(c_cyclistsmt))]
  17: [~(genlmt(c_tptp_member3717_mt,c_cyclistsmt))], ~(mtvisible(c_tptp_spindleheadmt)), ~(
mtvisible(c_tptp_member3717_mt))
  18: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  19: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  20: [~(artsupplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  21: [~(supplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  22: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

Gamma_39: (move)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: [~(genlmt(c_tptp_member3717_mt,c_cyclistsmt))], ~(mtvisible(c_tptp_spindleheadmt)), ~(
mtvisible(c_tptp_member3717_mt))
  16: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [genlmt(
c_tptp_member3717_mt,c_cyclistsmt)]
  17: ~(mtvisible(c_tptp_spindleheadmt)), [~(mtvisible(c_cyclistsmt))]
  18: ~(genlmt(c_tptp_member3717_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)]
  19: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt))
  20: [~(artsupplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  21: [~(supplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  22: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

Gamma_40: (resolve)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: [~(genlmt(c_tptp_member3717_mt,c_cyclistsmt))], ~(mtvisible(c_tptp_spindleheadmt)), ~(
mtvisible(c_tptp_member3717_mt))
  16: [~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt))], ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), ~(
mtvisible(c_tptp_spindleheadmt)), ~(mtvisible(c_tptp_member3717_mt))
  17: ~(mtvisible(c_tptp_spindleheadmt)), [~(mtvisible(c_cyclistsmt))]
  18: [~(artsupplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  19: [~(supplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  20: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

Gamma_41: (extend-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  15: [~(genlmt(c_tptp_member3717_mt,c_cyclistsmt))], ~(mtvisible(c_tptp_spindleheadmt)), ~(
mtvisible(c_tptp_member3717_mt))
  16: [~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt))], ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), ~(
mtvisible(c_tptp_spindleheadmt)), ~(mtvisible(c_tptp_member3717_mt))
  17: ~(mtvisible(c_tptp_spindleheadmt)), [~(mtvisible(c_cyclistsmt))]
  18: [~(artsupplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  19: [~(supplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  20: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

Gamma_42: (move)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt))], ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), ~(
mtvisible(c_tptp_spindleheadmt)), ~(mtvisible(c_tptp_member3717_mt))
  15: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)]
  16: [~(genlmt(c_tptp_member3717_mt,c_cyclistsmt))], ~(mtvisible(c_tptp_spindleheadmt)), ~(
mtvisible(c_tptp_member3717_mt))
  17: ~(mtvisible(c_tptp_spindleheadmt)), [~(mtvisible(c_cyclistsmt))]
  18: [~(artsupplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  19: [~(supplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  20: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

Gamma_43: (resolve)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt))], ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), ~(
mtvisible(c_tptp_spindleheadmt)), ~(mtvisible(c_tptp_member3717_mt))
  15: [~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt))], ~(mtvisible(c_tptp_spindleheadmt)), ~(
mtvisible(c_tptp_member3717_mt))
  16: [~(genlmt(c_tptp_member3717_mt,c_cyclistsmt))], ~(mtvisible(c_tptp_spindleheadmt)), ~(
mtvisible(c_tptp_member3717_mt))
  17: ~(mtvisible(c_tptp_spindleheadmt)), [~(mtvisible(c_cyclistsmt))]
  18: [~(artsupplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  19: [~(supplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  20: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

Gamma_44: (extend-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  5: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  6: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  9: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  11: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  13: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  14: [~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt))], ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), ~(
mtvisible(c_tptp_spindleheadmt)), ~(mtvisible(c_tptp_member3717_mt))
  15: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [~(mtvisible(c_tptp_spindleheadmt))], ~(
mtvisible(c_tptp_member3717_mt))
  16: [~(genlmt(c_tptp_member3717_mt,c_cyclistsmt))], ~(mtvisible(c_tptp_spindleheadmt)), ~(
mtvisible(c_tptp_member3717_mt))
  17: ~(mtvisible(c_tptp_spindleheadmt)), [~(mtvisible(c_cyclistsmt))]
  18: [~(artsupplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  19: [~(supplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  20: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

Gamma_45: (move)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [~(mtvisible(c_tptp_spindleheadmt))], ~(
mtvisible(c_tptp_member3717_mt))
  5: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [mtvisible(
c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member3717_mt))
  6: [relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))], ~(
mtvisible(c_tptp_spindleheadmt))
  7: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [binarypredicate(
c_tptpofobject)]
  8: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [collection(
c_supplies)]
  9: ~(relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_14(n_232))), [thing(
f_tptpquantityfn_14(n_232))]
  10: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  11: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  12: [genls(c_supplies,c_supplies)], ~(collection(c_supplies))
  13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  14: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  15: [~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt))], ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), ~(
mtvisible(c_tptp_spindleheadmt)), ~(mtvisible(c_tptp_member3717_mt))
  16: [~(genlmt(c_tptp_member3717_mt,c_cyclistsmt))], ~(mtvisible(c_tptp_spindleheadmt)), ~(
mtvisible(c_tptp_member3717_mt))
  17: ~(mtvisible(c_tptp_spindleheadmt)), [~(mtvisible(c_cyclistsmt))]
  18: [~(artsupplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  19: [~(supplies(c_tptpartsupplies))], ~(mtvisible(c_tptp_spindleheadmt))
  20: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

Gamma_46: (resolve)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [~(mtvisible(c_tptp_spindleheadmt))], ~(
mtvisible(c_tptp_member3717_mt))
  5: [~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt))], ~(mtvisible(c_tptp_member3717_mt))
  6: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  7: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  8: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  9: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  10: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

Gamma_47: (extend-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  4: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [~(mtvisible(c_tptp_spindleheadmt))], ~(
mtvisible(c_tptp_member3717_mt))
  5: [~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt))], ~(mtvisible(c_tptp_member3717_mt))
  6: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  7: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  8: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  9: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  10: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

Gamma_48: (move)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt))], ~(mtvisible(c_tptp_member3717_mt))
  4: [genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)]
  5: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [~(mtvisible(c_tptp_spindleheadmt))], ~(
mtvisible(c_tptp_member3717_mt))
  6: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_member3717_mt)]
  7: ~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)), [microtheory(
c_tptp_spindleheadmt)]
  8: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt))
  9: [genlmt(c_tptp_member3717_mt,c_tptp_member3717_mt)], ~(microtheory(c_tptp_member3717_mt))
  10: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

Gamma_49: (resolve)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt))], ~(mtvisible(c_tptp_member3717_mt))
  4: [~(mtvisible(c_tptp_member3717_mt))]
  5: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

Gamma_50: (extend-conflict)
  0: [mtvisible(c_tptp_member3717_mt)]
  1: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  2: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  3: [~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt))], ~(mtvisible(c_tptp_member3717_mt))
  4: [~(mtvisible(c_tptp_member3717_mt))]
  5: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

Gamma_51: (move)
  0: [~(mtvisible(c_tptp_member3717_mt))]
  1: [mtvisible(c_tptp_member3717_mt)]
  2: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  3: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  4: [~(genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt))], ~(mtvisible(c_tptp_member3717_mt))
  5: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

Gamma_52: (resolve)
  0: [~(mtvisible(c_tptp_member3717_mt))]
  1: []
  2: [natargument(f_tptpquantityfn_14(X0),n_1,X0)]
  3: [natfunction(f_tptpquantityfn_14(X0),c_tptpquantityfn_14)]
  4: [~(tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)))]

SZS status Unsatisfiable