%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- not ground preserving Gamma_0: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] Gamma_1: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] Gamma_2: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] Gamma_3: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] Gamma_4: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) Gamma_5: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] Gamma_6: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] Gamma_7: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) Gamma_8: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) Gamma_9: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] Gamma_10: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] Gamma_11: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) Gamma_12: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] Gamma_13: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) Gamma_14: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] Gamma_15: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) Gamma_16: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] Gamma_17: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) Gamma_18: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) Gamma_19: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) Gamma_20: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] Gamma_21: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] Gamma_22: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) Gamma_23: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 23: [militaryperson(c_tptpnavypersonnel_3)], ~(navypersonnel(c_tptpnavypersonnel_3)) Gamma_24: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 23: [militaryperson(c_tptpnavypersonnel_3)], ~(navypersonnel(c_tptpnavypersonnel_3)) 24: [isa(c_tptpnavypersonnel_3,c_militaryperson)], ~(militaryperson(c_tptpnavypersonnel_3)) Gamma_25: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 23: [militaryperson(c_tptpnavypersonnel_3)], ~(navypersonnel(c_tptpnavypersonnel_3)) 24: [isa(c_tptpnavypersonnel_3,c_militaryperson)], ~(militaryperson(c_tptpnavypersonnel_3)) 25: ~(isa(c_tptpnavypersonnel_3,c_militaryperson)), [collection(c_militaryperson)] Gamma_26: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 23: [militaryperson(c_tptpnavypersonnel_3)], ~(navypersonnel(c_tptpnavypersonnel_3)) 24: [isa(c_tptpnavypersonnel_3,c_militaryperson)], ~(militaryperson(c_tptpnavypersonnel_3)) 25: ~(isa(c_tptpnavypersonnel_3,c_militaryperson)), [collection(c_militaryperson)] 26: [genls(c_militaryperson,c_militaryperson)], ~(collection(c_militaryperson)) Gamma_27: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 23: [militaryperson(c_tptpnavypersonnel_3)], ~(navypersonnel(c_tptpnavypersonnel_3)) 24: [isa(c_tptpnavypersonnel_3,c_militaryperson)], ~(militaryperson(c_tptpnavypersonnel_3)) 25: ~(isa(c_tptpnavypersonnel_3,c_militaryperson)), [collection(c_militaryperson)] 26: [genls(c_militaryperson,c_militaryperson)], ~(collection(c_militaryperson)) 27: [genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)] Gamma_28: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 23: [militaryperson(c_tptpnavypersonnel_3)], ~(navypersonnel(c_tptpnavypersonnel_3)) 24: [isa(c_tptpnavypersonnel_3,c_militaryperson)], ~(militaryperson(c_tptpnavypersonnel_3)) 25: ~(isa(c_tptpnavypersonnel_3,c_militaryperson)), [collection(c_militaryperson)] 26: [genls(c_militaryperson,c_militaryperson)], ~(collection(c_militaryperson)) 27: [genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)] 28: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)), [mtvisible( c_tptp_member698_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) Gamma_29: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 23: [militaryperson(c_tptpnavypersonnel_3)], ~(navypersonnel(c_tptpnavypersonnel_3)) 24: [isa(c_tptpnavypersonnel_3,c_militaryperson)], ~(militaryperson(c_tptpnavypersonnel_3)) 25: ~(isa(c_tptpnavypersonnel_3,c_militaryperson)), [collection(c_militaryperson)] 26: [genls(c_militaryperson,c_militaryperson)], ~(collection(c_militaryperson)) 27: [genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)] 28: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)), [mtvisible( c_tptp_member698_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 29: [relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))], ~( mtvisible(c_tptp_member698_mt)) Gamma_30: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 23: [militaryperson(c_tptpnavypersonnel_3)], ~(navypersonnel(c_tptpnavypersonnel_3)) 24: [isa(c_tptpnavypersonnel_3,c_militaryperson)], ~(militaryperson(c_tptpnavypersonnel_3)) 25: ~(isa(c_tptpnavypersonnel_3,c_militaryperson)), [collection(c_militaryperson)] 26: [genls(c_militaryperson,c_militaryperson)], ~(collection(c_militaryperson)) 27: [genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)] 28: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)), [mtvisible( c_tptp_member698_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 29: [relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))], ~( mtvisible(c_tptp_member698_mt)) 30: ~(relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))), [binarypredicate( c_tptpofobject)] Gamma_31: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 23: [militaryperson(c_tptpnavypersonnel_3)], ~(navypersonnel(c_tptpnavypersonnel_3)) 24: [isa(c_tptpnavypersonnel_3,c_militaryperson)], ~(militaryperson(c_tptpnavypersonnel_3)) 25: ~(isa(c_tptpnavypersonnel_3,c_militaryperson)), [collection(c_militaryperson)] 26: [genls(c_militaryperson,c_militaryperson)], ~(collection(c_militaryperson)) 27: [genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)] 28: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)), [mtvisible( c_tptp_member698_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 29: [relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))], ~( mtvisible(c_tptp_member698_mt)) 30: ~(relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))), [binarypredicate( c_tptpofobject)] 31: ~(relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))), [thing( f_tptpquantityfn_6(n_414))] Gamma_32: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 23: [militaryperson(c_tptpnavypersonnel_3)], ~(navypersonnel(c_tptpnavypersonnel_3)) 24: [isa(c_tptpnavypersonnel_3,c_militaryperson)], ~(militaryperson(c_tptpnavypersonnel_3)) 25: ~(isa(c_tptpnavypersonnel_3,c_militaryperson)), [collection(c_militaryperson)] 26: [genls(c_militaryperson,c_militaryperson)], ~(collection(c_militaryperson)) 27: [genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)] 28: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)), [mtvisible( c_tptp_member698_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 29: [relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))], ~( mtvisible(c_tptp_member698_mt)) 30: ~(relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))), [binarypredicate( c_tptpofobject)] 31: ~(relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))), [thing( f_tptpquantityfn_6(n_414))] 32: [tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414))], ~( militaryperson(c_tptpnavypersonnel_3)), ~(mtvisible(c_tptp_member698_mt)) Gamma_33: (extend-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 23: [militaryperson(c_tptpnavypersonnel_3)], ~(navypersonnel(c_tptpnavypersonnel_3)) 24: [isa(c_tptpnavypersonnel_3,c_militaryperson)], ~(militaryperson(c_tptpnavypersonnel_3)) 25: ~(isa(c_tptpnavypersonnel_3,c_militaryperson)), [collection(c_militaryperson)] 26: [genls(c_militaryperson,c_militaryperson)], ~(collection(c_militaryperson)) 27: [genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)] 28: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)), [mtvisible( c_tptp_member698_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 29: [relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))], ~( mtvisible(c_tptp_member698_mt)) 30: ~(relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))), [binarypredicate( c_tptpofobject)] 31: ~(relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))), [thing( f_tptpquantityfn_6(n_414))] 32: [tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414))], ~( militaryperson(c_tptpnavypersonnel_3)), ~(mtvisible(c_tptp_member698_mt)) 33: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] Gamma_34: (move) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 23: [militaryperson(c_tptpnavypersonnel_3)], ~(navypersonnel(c_tptpnavypersonnel_3)) 24: [isa(c_tptpnavypersonnel_3,c_militaryperson)], ~(militaryperson(c_tptpnavypersonnel_3)) 25: ~(isa(c_tptpnavypersonnel_3,c_militaryperson)), [collection(c_militaryperson)] 26: [genls(c_militaryperson,c_militaryperson)], ~(collection(c_militaryperson)) 27: [genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)] 28: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)), [mtvisible( c_tptp_member698_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 29: [relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))], ~( mtvisible(c_tptp_member698_mt)) 30: ~(relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))), [binarypredicate( c_tptpofobject)] 31: ~(relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))), [thing( f_tptpquantityfn_6(n_414))] 32: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] 33: [tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414))], ~( militaryperson(c_tptpnavypersonnel_3)), ~(mtvisible(c_tptp_member698_mt)) Gamma_35: (resolve) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 23: [militaryperson(c_tptpnavypersonnel_3)], ~(navypersonnel(c_tptpnavypersonnel_3)) 24: [isa(c_tptpnavypersonnel_3,c_militaryperson)], ~(militaryperson(c_tptpnavypersonnel_3)) 25: ~(isa(c_tptpnavypersonnel_3,c_militaryperson)), [collection(c_militaryperson)] 26: [genls(c_militaryperson,c_militaryperson)], ~(collection(c_militaryperson)) 27: [genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)] 28: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)), [mtvisible( c_tptp_member698_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 29: [relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))], ~( mtvisible(c_tptp_member698_mt)) 30: ~(relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))), [binarypredicate( c_tptpofobject)] 31: ~(relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))), [thing( f_tptpquantityfn_6(n_414))] 32: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] 33: [~(militaryperson(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_member698_mt)) Gamma_36: (extend-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 23: [militaryperson(c_tptpnavypersonnel_3)], ~(navypersonnel(c_tptpnavypersonnel_3)) 24: [isa(c_tptpnavypersonnel_3,c_militaryperson)], ~(militaryperson(c_tptpnavypersonnel_3)) 25: ~(isa(c_tptpnavypersonnel_3,c_militaryperson)), [collection(c_militaryperson)] 26: [genls(c_militaryperson,c_militaryperson)], ~(collection(c_militaryperson)) 27: [genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)] 28: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)), [mtvisible( c_tptp_member698_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 29: [relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))], ~( mtvisible(c_tptp_member698_mt)) 30: ~(relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))), [binarypredicate( c_tptpofobject)] 31: ~(relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))), [thing( f_tptpquantityfn_6(n_414))] 32: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] 33: ~(militaryperson(c_tptpnavypersonnel_3)), [~(mtvisible(c_tptp_member698_mt))] Gamma_37: (move) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 23: [militaryperson(c_tptpnavypersonnel_3)], ~(navypersonnel(c_tptpnavypersonnel_3)) 24: [isa(c_tptpnavypersonnel_3,c_militaryperson)], ~(militaryperson(c_tptpnavypersonnel_3)) 25: ~(isa(c_tptpnavypersonnel_3,c_militaryperson)), [collection(c_militaryperson)] 26: [genls(c_militaryperson,c_militaryperson)], ~(collection(c_militaryperson)) 27: [genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)] 28: ~(militaryperson(c_tptpnavypersonnel_3)), [~(mtvisible(c_tptp_member698_mt))] 29: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)), [mtvisible( c_tptp_member698_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 30: [relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))], ~( mtvisible(c_tptp_member698_mt)) 31: ~(relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))), [binarypredicate( c_tptpofobject)] 32: ~(relationallinstance(c_tptpofobject,c_militaryperson,f_tptpquantityfn_6(n_414))), [thing( f_tptpquantityfn_6(n_414))] 33: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] Gamma_38: (resolve) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 23: [militaryperson(c_tptpnavypersonnel_3)], ~(navypersonnel(c_tptpnavypersonnel_3)) 24: [isa(c_tptpnavypersonnel_3,c_militaryperson)], ~(militaryperson(c_tptpnavypersonnel_3)) 25: ~(isa(c_tptpnavypersonnel_3,c_militaryperson)), [collection(c_militaryperson)] 26: [genls(c_militaryperson,c_militaryperson)], ~(collection(c_militaryperson)) 27: [genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)] 28: ~(militaryperson(c_tptpnavypersonnel_3)), [~(mtvisible(c_tptp_member698_mt))] 29: [~(genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt))], ~(militaryperson(c_tptpnavypersonnel_3)), ~( mtvisible(c_tptp_spindlecollectormt)) 30: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] Gamma_39: (extend-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 23: [militaryperson(c_tptpnavypersonnel_3)], ~(navypersonnel(c_tptpnavypersonnel_3)) 24: [isa(c_tptpnavypersonnel_3,c_militaryperson)], ~(militaryperson(c_tptpnavypersonnel_3)) 25: ~(isa(c_tptpnavypersonnel_3,c_militaryperson)), [collection(c_militaryperson)] 26: [genls(c_militaryperson,c_militaryperson)], ~(collection(c_militaryperson)) 27: [genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)] 28: ~(militaryperson(c_tptpnavypersonnel_3)), [~(mtvisible(c_tptp_member698_mt))] 29: [~(genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt))], ~(militaryperson(c_tptpnavypersonnel_3)), ~( mtvisible(c_tptp_spindlecollectormt)) 30: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] Gamma_40: (move) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 23: [militaryperson(c_tptpnavypersonnel_3)], ~(navypersonnel(c_tptpnavypersonnel_3)) 24: [isa(c_tptpnavypersonnel_3,c_militaryperson)], ~(militaryperson(c_tptpnavypersonnel_3)) 25: ~(isa(c_tptpnavypersonnel_3,c_militaryperson)), [collection(c_militaryperson)] 26: [genls(c_militaryperson,c_militaryperson)], ~(collection(c_militaryperson)) 27: [~(genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt))], ~(militaryperson(c_tptpnavypersonnel_3)), ~( mtvisible(c_tptp_spindlecollectormt)) 28: [genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)] 29: ~(militaryperson(c_tptpnavypersonnel_3)), [~(mtvisible(c_tptp_member698_mt))] 30: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] Gamma_41: (resolve) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 23: [militaryperson(c_tptpnavypersonnel_3)], ~(navypersonnel(c_tptpnavypersonnel_3)) 24: [isa(c_tptpnavypersonnel_3,c_militaryperson)], ~(militaryperson(c_tptpnavypersonnel_3)) 25: ~(isa(c_tptpnavypersonnel_3,c_militaryperson)), [collection(c_militaryperson)] 26: [genls(c_militaryperson,c_militaryperson)], ~(collection(c_militaryperson)) 27: [~(genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt))], ~(militaryperson(c_tptpnavypersonnel_3)), ~( mtvisible(c_tptp_spindlecollectormt)) 28: [~(militaryperson(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 29: ~(militaryperson(c_tptpnavypersonnel_3)), [~(mtvisible(c_tptp_member698_mt))] 30: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] Gamma_42: (extend-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 23: [militaryperson(c_tptpnavypersonnel_3)], ~(navypersonnel(c_tptpnavypersonnel_3)) 24: [isa(c_tptpnavypersonnel_3,c_militaryperson)], ~(militaryperson(c_tptpnavypersonnel_3)) 25: ~(isa(c_tptpnavypersonnel_3,c_militaryperson)), [collection(c_militaryperson)] 26: [genls(c_militaryperson,c_militaryperson)], ~(collection(c_militaryperson)) 27: [~(genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt))], ~(militaryperson(c_tptpnavypersonnel_3)), ~( mtvisible(c_tptp_spindlecollectormt)) 28: [~(militaryperson(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 29: ~(militaryperson(c_tptpnavypersonnel_3)), [~(mtvisible(c_tptp_member698_mt))] 30: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] Gamma_43: (move) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 23: [~(militaryperson(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 24: [militaryperson(c_tptpnavypersonnel_3)], ~(navypersonnel(c_tptpnavypersonnel_3)) 25: [isa(c_tptpnavypersonnel_3,c_militaryperson)], ~(militaryperson(c_tptpnavypersonnel_3)) 26: ~(isa(c_tptpnavypersonnel_3,c_militaryperson)), [collection(c_militaryperson)] 27: [genls(c_militaryperson,c_militaryperson)], ~(collection(c_militaryperson)) 28: [~(genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt))], ~(militaryperson(c_tptpnavypersonnel_3)), ~( mtvisible(c_tptp_spindlecollectormt)) 29: ~(militaryperson(c_tptpnavypersonnel_3)), [~(mtvisible(c_tptp_member698_mt))] 30: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] Gamma_44: (resolve) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 23: [~(militaryperson(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 24: [~(navypersonnel(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 25: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] Gamma_45: (extend-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 19: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 20: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 22: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 23: [~(militaryperson(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 24: [~(navypersonnel(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 25: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] Gamma_46: (move) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [~(navypersonnel(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 19: [navypersonnel(c_tptpnavypersonnel_3)], ~(mtvisible(c_tptp_member1672_mt)) 20: [isa(c_tptpnavypersonnel_3,c_navypersonnel)], ~(navypersonnel(c_tptpnavypersonnel_3)) 21: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [thing(c_tptpnavypersonnel_3)] 22: ~(isa(c_tptpnavypersonnel_3,c_navypersonnel)), [collection(c_navypersonnel)] 23: [genls(c_navypersonnel,c_navypersonnel)], ~(collection(c_navypersonnel)) 24: [~(militaryperson(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 25: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] Gamma_47: (resolve) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [~(navypersonnel(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 19: [~(mtvisible(c_tptp_member1672_mt))], ~(mtvisible(c_tptp_spindlecollectormt)) 20: [~(militaryperson(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 21: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] Gamma_48: (extend-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 17: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 18: [~(navypersonnel(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 19: [~(mtvisible(c_tptp_member1672_mt))], ~(mtvisible(c_tptp_spindlecollectormt)) 20: [~(militaryperson(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 21: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] Gamma_49: (move) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: [~(mtvisible(c_tptp_member1672_mt))], ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [mtvisible( c_tptp_member1672_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 17: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 18: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 19: [~(navypersonnel(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 20: [~(militaryperson(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 21: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] Gamma_50: (resolve) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: [~(mtvisible(c_tptp_member1672_mt))], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt))], ~( mtvisible(c_tptp_spindlecollectormt)) 17: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 18: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 19: [~(navypersonnel(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 20: [~(militaryperson(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 21: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] Gamma_51: (extend-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 15: [~(mtvisible(c_tptp_member1672_mt))], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt))], ~( mtvisible(c_tptp_spindlecollectormt)) 17: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 18: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 19: [~(navypersonnel(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 20: [~(militaryperson(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 21: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] Gamma_52: (move) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt))], ~( mtvisible(c_tptp_spindlecollectormt)) 15: [genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)] 16: [~(mtvisible(c_tptp_member1672_mt))], ~(mtvisible(c_tptp_spindlecollectormt)) 17: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)), [microtheory( c_tptp_member1672_mt)] 18: [genlmt(c_tptp_member1672_mt,c_tptp_member1672_mt)], ~(microtheory(c_tptp_member1672_mt)) 19: [~(navypersonnel(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 20: [~(militaryperson(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 21: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] Gamma_53: (resolve) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt))], ~( mtvisible(c_tptp_spindlecollectormt)) 15: [~(mtvisible(c_tptp_spindlecollectormt))] 16: [~(mtvisible(c_tptp_member1672_mt))], ~(mtvisible(c_tptp_spindlecollectormt)) 17: [~(navypersonnel(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 18: [~(militaryperson(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 19: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] Gamma_54: (extend-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 13: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 14: [~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt))], ~( mtvisible(c_tptp_spindlecollectormt)) 15: [~(mtvisible(c_tptp_spindlecollectormt))] 16: [~(mtvisible(c_tptp_member1672_mt))], ~(mtvisible(c_tptp_spindlecollectormt)) 17: [~(navypersonnel(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 18: [~(militaryperson(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 19: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] Gamma_55: (move) 0: [~(mtvisible(c_tptp_spindlecollectormt))] 1: [mtvisible(c_tptp_spindlecollectormt)] 2: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 3: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 4: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [mtvisible( c_tptp_member3993_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 7: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 8: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 9: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 10: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 12: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [mtvisible( c_tptp_spindleheadmt)], ~(mtvisible(c_tptp_spindlecollectormt)) 13: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 14: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 15: [~(genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt))], ~( mtvisible(c_tptp_spindlecollectormt)) 16: [~(mtvisible(c_tptp_member1672_mt))], ~(mtvisible(c_tptp_spindlecollectormt)) 17: [~(navypersonnel(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 18: [~(militaryperson(c_tptpnavypersonnel_3))], ~(mtvisible(c_tptp_spindlecollectormt)) 19: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] Gamma_56: (resolve) 0: [~(mtvisible(c_tptp_spindlecollectormt))] 1: [] 2: [natargument(f_tptpquantityfn_6(X0),n_1,X0)] 3: [natfunction(f_tptpquantityfn_6(X0),c_tptpquantityfn_6)] 4: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 5: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_spindlecollectormt)] 6: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [microtheory( c_tptp_member3993_mt)] 7: [genlmt(c_tptp_member3993_mt,c_tptp_member3993_mt)], ~(microtheory(c_tptp_member3993_mt)) 8: [genlmt(c_tptp_spindlecollectormt,c_tptp_spindlecollectormt)], ~( microtheory(c_tptp_spindlecollectormt)) 9: [genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)] 10: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)), [genlmt( c_tptp_spindlecollectormt,c_tptp_spindleheadmt)] 11: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [microtheory( c_tptp_spindleheadmt)] 12: [genlmt(c_tptp_spindleheadmt,c_tptp_spindleheadmt)], ~(microtheory(c_tptp_spindleheadmt)) 13: [~(tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))] SZS status Unsatisfiable