%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- not ground preserving Gamma_0: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] Gamma_1: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] Gamma_2: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] Gamma_3: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] Gamma_4: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) Gamma_5: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) Gamma_6: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] Gamma_7: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] Gamma_8: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] Gamma_9: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] Gamma_10: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] Gamma_11: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) Gamma_12: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) Gamma_13: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] Gamma_14: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] Gamma_15: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) Gamma_16: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] Gamma_17: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) Gamma_18: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] Gamma_19: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] Gamma_20: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] Gamma_21: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) Gamma_22: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) Gamma_23: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] Gamma_24: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] Gamma_25: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) Gamma_26: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] Gamma_27: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] Gamma_28: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) Gamma_29: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] Gamma_30: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) Gamma_31: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] Gamma_32: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) Gamma_33: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] Gamma_34: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] Gamma_35: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) Gamma_36: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 36: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] Gamma_37: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 36: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) Gamma_38: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 36: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 38: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] Gamma_39: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 36: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 38: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 39: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) Gamma_40: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 36: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 38: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 39: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 40: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_basekb)] Gamma_41: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 36: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 38: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 39: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 40: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_basekb)] 41: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) Gamma_42: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 36: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 38: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 39: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 40: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_basekb)] 41: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 42: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) Gamma_43: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 36: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 38: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 39: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 40: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_basekb)] 41: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 42: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 43: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_calendarsvocabularymt)] Gamma_44: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 36: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 38: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 39: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 40: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_basekb)] 41: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 42: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 43: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_calendarsvocabularymt)] 44: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) Gamma_45: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 36: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 38: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 39: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 40: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_basekb)] 41: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 42: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 43: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_calendarsvocabularymt)] 44: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 45: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_basekb)] Gamma_46: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 36: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 38: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 39: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 40: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_basekb)] 41: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 42: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 43: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_calendarsvocabularymt)] 44: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 45: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_basekb)] 46: ~(genlmt(c_cyclistsmt,c_universalvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_universalvocabularymt)] Gamma_47: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 36: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 38: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 39: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 40: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_basekb)] 41: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 42: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 43: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_calendarsvocabularymt)] 44: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 45: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_basekb)] 46: ~(genlmt(c_cyclistsmt,c_universalvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_universalvocabularymt)] 47: ~(genlmt(c_cyclistsmt,c_calendarsvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_calendarsvocabularymt)] Gamma_48: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 36: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 38: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 39: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 40: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_basekb)] 41: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 42: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 43: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_calendarsvocabularymt)] 44: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 45: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_basekb)] 46: ~(genlmt(c_cyclistsmt,c_universalvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_universalvocabularymt)] 47: ~(genlmt(c_cyclistsmt,c_calendarsvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_calendarsvocabularymt)] 48: [tptpquantity(f_tptpquantityfn_1(X0))] Gamma_49: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 36: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 38: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 39: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 40: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_basekb)] 41: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 42: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 43: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_calendarsvocabularymt)] 44: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 45: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_basekb)] 46: ~(genlmt(c_cyclistsmt,c_universalvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_universalvocabularymt)] 47: ~(genlmt(c_cyclistsmt,c_calendarsvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_calendarsvocabularymt)] 48: [tptpquantity(f_tptpquantityfn_1(X0))] 49: [furpelt(c_theprototypicalfurpelt)] Gamma_50: (extend-no-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 36: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 38: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 39: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 40: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_basekb)] 41: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 42: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 43: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_calendarsvocabularymt)] 44: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 45: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_basekb)] 46: ~(genlmt(c_cyclistsmt,c_universalvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_universalvocabularymt)] 47: ~(genlmt(c_cyclistsmt,c_calendarsvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_calendarsvocabularymt)] 48: [tptpquantity(f_tptpquantityfn_1(X0))] 49: [furpelt(c_theprototypicalfurpelt)] 50: [tptpofobject(c_theprototypicalfurpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)), ~(furpelt(c_theprototypicalfurpelt)) Gamma_51: (extend-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 36: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 38: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 39: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 40: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_basekb)] 41: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 42: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 43: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_calendarsvocabularymt)] 44: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 45: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_basekb)] 46: ~(genlmt(c_cyclistsmt,c_universalvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_universalvocabularymt)] 47: ~(genlmt(c_cyclistsmt,c_calendarsvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_calendarsvocabularymt)] 48: [tptpquantity(f_tptpquantityfn_1(X0))] 49: [furpelt(c_theprototypicalfurpelt)] 50: [tptpofobject(c_theprototypicalfurpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)), ~(furpelt(c_theprototypicalfurpelt)) 51: [~(tptpofobject(c_theprototypicalfurpelt,f_tptpquantityfn_1(n_328)))] Gamma_52: (move) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 36: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 38: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 39: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 40: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_basekb)] 41: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 42: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 43: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_calendarsvocabularymt)] 44: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 45: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_basekb)] 46: ~(genlmt(c_cyclistsmt,c_universalvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_universalvocabularymt)] 47: ~(genlmt(c_cyclistsmt,c_calendarsvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_calendarsvocabularymt)] 48: [tptpquantity(f_tptpquantityfn_1(X0))] 49: [furpelt(c_theprototypicalfurpelt)] 50: [~(tptpofobject(c_theprototypicalfurpelt,f_tptpquantityfn_1(n_328)))] 51: [tptpofobject(c_theprototypicalfurpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)), ~(furpelt(c_theprototypicalfurpelt)) Gamma_53: (resolve) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 36: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 38: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 39: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 40: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_basekb)] 41: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 42: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 43: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_calendarsvocabularymt)] 44: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 45: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_basekb)] 46: ~(genlmt(c_cyclistsmt,c_universalvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_universalvocabularymt)] 47: ~(genlmt(c_cyclistsmt,c_calendarsvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_calendarsvocabularymt)] 48: [tptpquantity(f_tptpquantityfn_1(X0))] 49: [furpelt(c_theprototypicalfurpelt)] 50: [~(tptpofobject(c_theprototypicalfurpelt,f_tptpquantityfn_1(n_328)))] 51: [~(mtvisible(c_tptp_spindleheadmt))], ~(furpelt(c_theprototypicalfurpelt)) Gamma_54: (extend-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 36: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 38: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 39: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 40: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_basekb)] 41: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 42: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 43: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_calendarsvocabularymt)] 44: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 45: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_basekb)] 46: ~(genlmt(c_cyclistsmt,c_universalvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_universalvocabularymt)] 47: ~(genlmt(c_cyclistsmt,c_calendarsvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_calendarsvocabularymt)] 48: [tptpquantity(f_tptpquantityfn_1(X0))] 49: [furpelt(c_theprototypicalfurpelt)] 50: [~(tptpofobject(c_theprototypicalfurpelt,f_tptpquantityfn_1(n_328)))] 51: ~(mtvisible(c_tptp_spindleheadmt)), [~(furpelt(c_theprototypicalfurpelt))] Gamma_55: (move) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 36: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 38: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 39: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 40: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_basekb)] 41: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 42: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 43: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_calendarsvocabularymt)] 44: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 45: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_basekb)] 46: ~(genlmt(c_cyclistsmt,c_universalvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_universalvocabularymt)] 47: ~(genlmt(c_cyclistsmt,c_calendarsvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_calendarsvocabularymt)] 48: [tptpquantity(f_tptpquantityfn_1(X0))] 49: ~(mtvisible(c_tptp_spindleheadmt)), [~(furpelt(c_theprototypicalfurpelt))] 50: [furpelt(c_theprototypicalfurpelt)] 51: [~(tptpofobject(c_theprototypicalfurpelt,f_tptpquantityfn_1(n_328)))] Gamma_56: (resolve) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 36: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 38: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 39: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 40: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_basekb)] 41: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 42: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 43: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_calendarsvocabularymt)] 44: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 45: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_basekb)] 46: ~(genlmt(c_cyclistsmt,c_universalvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_universalvocabularymt)] 47: ~(genlmt(c_cyclistsmt,c_calendarsvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_calendarsvocabularymt)] 48: [tptpquantity(f_tptpquantityfn_1(X0))] 49: ~(mtvisible(c_tptp_spindleheadmt)), [~(furpelt(c_theprototypicalfurpelt))] 50: [~(mtvisible(c_tptp_spindleheadmt))] 51: [~(tptpofobject(c_theprototypicalfurpelt,f_tptpquantityfn_1(n_328)))] Gamma_57: (extend-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 5: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 6: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 9: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 11: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 12: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 13: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 14: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 17: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 18: [genlmt(c_calendarsvocabularymt,c_basekb)] 19: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 21: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 22: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 23: [genlmt(c_cyclistsmt,c_calendarsmt)] 24: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 25: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 26: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 28: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 29: [genlmt(c_basekb,c_universalvocabularymt)] 30: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 31: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 32: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 33: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 34: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 36: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 38: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 39: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 40: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_basekb)] 41: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 42: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 43: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_calendarsvocabularymt)] 44: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 45: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_basekb)] 46: ~(genlmt(c_cyclistsmt,c_universalvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_universalvocabularymt)] 47: ~(genlmt(c_cyclistsmt,c_calendarsvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_calendarsvocabularymt)] 48: [tptpquantity(f_tptpquantityfn_1(X0))] 49: ~(mtvisible(c_tptp_spindleheadmt)), [~(furpelt(c_theprototypicalfurpelt))] 50: [~(mtvisible(c_tptp_spindleheadmt))] 51: [~(tptpofobject(c_theprototypicalfurpelt,f_tptpquantityfn_1(n_328)))] Gamma_58: (move) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: [~(mtvisible(c_tptp_spindleheadmt))] 5: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_member2356_mt)) 6: [relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))], ~( mtvisible(c_tptp_spindleheadmt)) 7: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [binarypredicate( c_tptpofobject)] 8: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [collection( c_furpelt)] 9: ~(relationallinstance(c_tptpofobject,c_furpelt,f_tptpquantityfn_1(n_328))), [thing( f_tptpquantityfn_1(n_328))] 10: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 11: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 13: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 14: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 15: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 16: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 17: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 18: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 19: [genlmt(c_calendarsvocabularymt,c_basekb)] 20: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 21: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 22: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 23: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 24: [genlmt(c_cyclistsmt,c_calendarsmt)] 25: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 26: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 27: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~(mtvisible(c_tptp_spindleheadmt)), [mtvisible( c_calendarsmt)] 28: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 29: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 30: [genlmt(c_basekb,c_universalvocabularymt)] 31: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 32: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 33: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 34: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 35: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 36: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 37: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 38: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 39: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 40: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 41: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_basekb)] 42: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 43: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 44: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_calendarsvocabularymt)] 45: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 46: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_basekb)] 47: ~(genlmt(c_cyclistsmt,c_universalvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_universalvocabularymt)] 48: ~(genlmt(c_cyclistsmt,c_calendarsvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_calendarsvocabularymt)] 49: [tptpquantity(f_tptpquantityfn_1(X0))] 50: ~(mtvisible(c_tptp_spindleheadmt)), [~(furpelt(c_theprototypicalfurpelt))] 51: [~(tptpofobject(c_theprototypicalfurpelt,f_tptpquantityfn_1(n_328)))] Gamma_59: (resolve) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: [~(mtvisible(c_tptp_spindleheadmt))] 5: [~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt))], ~(mtvisible(c_tptp_member2356_mt)) 6: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 7: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 8: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 9: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 10: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 11: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 12: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 13: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 14: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 15: [genlmt(c_calendarsvocabularymt,c_basekb)] 16: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 17: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 18: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 19: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 20: [genlmt(c_cyclistsmt,c_calendarsmt)] 21: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 22: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 23: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 24: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 25: [genlmt(c_basekb,c_universalvocabularymt)] 26: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 27: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 28: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 29: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 30: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 31: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 32: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 33: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 34: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 36: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_basekb)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 38: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 39: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_calendarsvocabularymt)] 40: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 41: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_basekb)] 42: ~(genlmt(c_cyclistsmt,c_universalvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_universalvocabularymt)] 43: ~(genlmt(c_cyclistsmt,c_calendarsvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_calendarsvocabularymt)] 44: [tptpquantity(f_tptpquantityfn_1(X0))] 45: [~(tptpofobject(c_theprototypicalfurpelt,f_tptpquantityfn_1(n_328)))] Gamma_60: (extend-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 4: [~(mtvisible(c_tptp_spindleheadmt))] 5: [~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt))], ~(mtvisible(c_tptp_member2356_mt)) 6: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 7: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 8: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 9: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 10: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 11: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 12: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 13: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 14: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 15: [genlmt(c_calendarsvocabularymt,c_basekb)] 16: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 17: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 18: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 19: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 20: [genlmt(c_cyclistsmt,c_calendarsmt)] 21: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 22: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 23: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 24: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 25: [genlmt(c_basekb,c_universalvocabularymt)] 26: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 27: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 28: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 29: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 30: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 31: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 32: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 33: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 34: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 36: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_basekb)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 38: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 39: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_calendarsvocabularymt)] 40: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 41: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_basekb)] 42: ~(genlmt(c_cyclistsmt,c_universalvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_universalvocabularymt)] 43: ~(genlmt(c_cyclistsmt,c_calendarsvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_calendarsvocabularymt)] 44: [tptpquantity(f_tptpquantityfn_1(X0))] 45: [~(tptpofobject(c_theprototypicalfurpelt,f_tptpquantityfn_1(n_328)))] Gamma_61: (move) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt))], ~(mtvisible(c_tptp_member2356_mt)) 4: [genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)] 5: [~(mtvisible(c_tptp_spindleheadmt))] 6: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_member2356_mt)] 7: ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 8: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 9: [genlmt(c_tptp_member2356_mt,c_tptp_member2356_mt)], ~(microtheory(c_tptp_member2356_mt)) 10: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 11: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_cyclistsmt)] 12: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [mtvisible(c_cyclistsmt)], ~( mtvisible(c_tptp_member2356_mt)) 13: ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 14: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 15: [genlmt(c_calendarsvocabularymt,c_basekb)] 16: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 17: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 18: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 19: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 20: [genlmt(c_cyclistsmt,c_calendarsmt)] 21: ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~(genlmt(c_tptp_member2356_mt,c_cyclistsmt)), [genlmt( c_tptp_member2356_mt,c_calendarsmt)] 22: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 23: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 24: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 25: [genlmt(c_basekb,c_universalvocabularymt)] 26: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 27: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 28: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 29: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 30: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 31: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 32: ~(genlmt(c_tptp_spindleheadmt,c_universalvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_universalvocabularymt)] 33: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 34: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 35: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 36: ~(genlmt(c_tptp_spindleheadmt,c_basekb)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_basekb)] 37: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 38: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 39: ~(genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)), ~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt)), [genlmt( c_tptp_member2356_mt,c_calendarsvocabularymt)] 40: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 41: ~(genlmt(c_cyclistsmt,c_basekb)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_basekb)] 42: ~(genlmt(c_cyclistsmt,c_universalvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_universalvocabularymt)] 43: ~(genlmt(c_cyclistsmt,c_calendarsvocabularymt)), ~(mtvisible(c_cyclistsmt)), [mtvisible( c_calendarsvocabularymt)] 44: [tptpquantity(f_tptpquantityfn_1(X0))] 45: [~(tptpofobject(c_theprototypicalfurpelt,f_tptpquantityfn_1(n_328)))] Gamma_62: (resolve) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt))], ~(mtvisible(c_tptp_member2356_mt)) 4: [~(mtvisible(c_tptp_member2356_mt))] 5: [~(mtvisible(c_tptp_spindleheadmt))] 6: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 7: [genlmt(c_calendarsvocabularymt,c_basekb)] 8: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 9: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 10: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 11: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 12: [genlmt(c_cyclistsmt,c_calendarsmt)] 13: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 14: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 15: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 16: [genlmt(c_basekb,c_universalvocabularymt)] 17: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 18: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 19: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 20: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 21: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 22: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 23: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 24: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 25: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 26: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 27: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 28: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 29: [tptpquantity(f_tptpquantityfn_1(X0))] 30: [~(tptpofobject(c_theprototypicalfurpelt,f_tptpquantityfn_1(n_328)))] Gamma_63: (extend-conflict) 0: [mtvisible(c_tptp_member2356_mt)] 1: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 3: [~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt))], ~(mtvisible(c_tptp_member2356_mt)) 4: [~(mtvisible(c_tptp_member2356_mt))] 5: [~(mtvisible(c_tptp_spindleheadmt))] 6: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 7: [genlmt(c_calendarsvocabularymt,c_basekb)] 8: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 9: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 10: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 11: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 12: [genlmt(c_cyclistsmt,c_calendarsmt)] 13: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 14: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 15: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 16: [genlmt(c_basekb,c_universalvocabularymt)] 17: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 18: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 19: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 20: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 21: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 22: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 23: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 24: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 25: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 26: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 27: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 28: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 29: [tptpquantity(f_tptpquantityfn_1(X0))] 30: [~(tptpofobject(c_theprototypicalfurpelt,f_tptpquantityfn_1(n_328)))] Gamma_64: (move) 0: [~(mtvisible(c_tptp_member2356_mt))] 1: [mtvisible(c_tptp_member2356_mt)] 2: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 3: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 4: [~(genlmt(c_tptp_member2356_mt,c_tptp_spindleheadmt))], ~(mtvisible(c_tptp_member2356_mt)) 5: [~(mtvisible(c_tptp_spindleheadmt))] 6: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 7: [genlmt(c_calendarsvocabularymt,c_basekb)] 8: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 9: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 10: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 11: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 12: [genlmt(c_cyclistsmt,c_calendarsmt)] 13: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 14: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 15: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 16: [genlmt(c_basekb,c_universalvocabularymt)] 17: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 18: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 19: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 20: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 21: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 22: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 23: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 24: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 25: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 26: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 27: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 28: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 29: [tptpquantity(f_tptpquantityfn_1(X0))] 30: [~(tptpofobject(c_theprototypicalfurpelt,f_tptpquantityfn_1(n_328)))] Gamma_65: (resolve) 0: [~(mtvisible(c_tptp_member2356_mt))] 1: [] 2: [natargument(f_tptpquantityfn_1(X0),n_1,X0)] 3: [natfunction(f_tptpquantityfn_1(X0),c_tptpquantityfn_1)] 4: [~(mtvisible(c_tptp_spindleheadmt))] 5: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 6: [genlmt(c_calendarsvocabularymt,c_basekb)] 7: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_calendarsvocabularymt)] 8: ~(genlmt(c_calendarsvocabularymt,c_basekb)), [microtheory(c_basekb)] 9: [genlmt(c_basekb,c_basekb)], ~(microtheory(c_basekb)) 10: [genlmt(c_calendarsvocabularymt,c_calendarsvocabularymt)], ~(microtheory(c_calendarsvocabularymt)) 11: [genlmt(c_cyclistsmt,c_calendarsmt)] 12: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), [genlmt(c_tptp_spindleheadmt, c_calendarsmt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)) 13: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [microtheory(c_calendarsmt)] 14: [genlmt(c_calendarsmt,c_calendarsmt)], ~(microtheory(c_calendarsmt)) 15: [genlmt(c_basekb,c_universalvocabularymt)] 16: [genlmt(c_calendarsvocabularymt,c_universalvocabularymt)], ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~( genlmt(c_basekb,c_universalvocabularymt)) 17: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), [microtheory( c_universalvocabularymt)] 18: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 19: [genlmt(c_calendarsmt,c_calendarsvocabularymt)] 20: ~(genlmt(c_calendarsvocabularymt,c_universalvocabularymt)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_universalvocabularymt)] 21: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_universalvocabularymt)], ~(genlmt(c_calendarsmt,c_universalvocabularymt)) 22: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_universalvocabularymt)], ~( genlmt(c_calendarsmt,c_universalvocabularymt)) 23: ~(genlmt(c_calendarsvocabularymt,c_basekb)), ~(genlmt(c_calendarsmt,c_calendarsvocabularymt)), [genlmt( c_calendarsmt,c_basekb)] 24: ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), [genlmt(c_tptp_spindleheadmt, c_basekb)], ~(genlmt(c_calendarsmt,c_basekb)) 25: ~(genlmt(c_cyclistsmt,c_calendarsmt)), [genlmt(c_cyclistsmt,c_basekb)], ~( genlmt(c_calendarsmt,c_basekb)) 26: [genlmt(c_tptp_spindleheadmt,c_calendarsvocabularymt)], ~(genlmt(c_tptp_spindleheadmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 27: [genlmt(c_cyclistsmt,c_calendarsvocabularymt)], ~(genlmt(c_cyclistsmt,c_calendarsmt)), ~( genlmt(c_calendarsmt,c_calendarsvocabularymt)) 28: [tptpquantity(f_tptpquantityfn_1(X0))] 29: [~(tptpofobject(c_theprototypicalfurpelt,f_tptpquantityfn_1(n_328)))] SZS status Unsatisfiable