%---------------- 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_2(X0),n_1,X0)] Gamma_2: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] Gamma_3: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] Gamma_4: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] Gamma_15: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) Gamma_16: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) Gamma_17: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] Gamma_18: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] Gamma_19: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] Gamma_20: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] Gamma_21: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) Gamma_22: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] Gamma_23: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 23: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [genlmt( c_tptp_spindlecollectormt,c_cyclistsmt)] Gamma_24: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 23: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [genlmt( c_tptp_spindlecollectormt,c_cyclistsmt)] 24: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [genlmt(c_tptp_member3993_mt, c_cyclistsmt)], ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)) Gamma_25: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 23: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [genlmt( c_tptp_spindlecollectormt,c_cyclistsmt)] 24: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [genlmt(c_tptp_member3993_mt, c_cyclistsmt)], ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)) 25: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), ~(mtvisible(c_tptp_member3993_mt)), [mtvisible( c_cyclistsmt)] Gamma_26: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 23: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [genlmt( c_tptp_spindlecollectormt,c_cyclistsmt)] 24: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [genlmt(c_tptp_member3993_mt, c_cyclistsmt)], ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)) 25: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), ~(mtvisible(c_tptp_member3993_mt)), [mtvisible( c_cyclistsmt)] 26: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] Gamma_27: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 23: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [genlmt( c_tptp_spindlecollectormt,c_cyclistsmt)] 24: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [genlmt(c_tptp_member3993_mt, c_cyclistsmt)], ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)) 25: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), ~(mtvisible(c_tptp_member3993_mt)), [mtvisible( c_cyclistsmt)] 26: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 27: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) Gamma_28: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 23: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [genlmt( c_tptp_spindlecollectormt,c_cyclistsmt)] 24: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [genlmt(c_tptp_member3993_mt, c_cyclistsmt)], ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)) 25: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), ~(mtvisible(c_tptp_member3993_mt)), [mtvisible( c_cyclistsmt)] 26: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 27: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 28: [runningshorts(c_tptprunningshorts)], ~(mtvisible(c_cyclistsmt)) Gamma_29: (extend-no-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 23: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [genlmt( c_tptp_spindlecollectormt,c_cyclistsmt)] 24: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [genlmt(c_tptp_member3993_mt, c_cyclistsmt)], ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)) 25: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), ~(mtvisible(c_tptp_member3993_mt)), [mtvisible( c_cyclistsmt)] 26: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 27: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 28: [runningshorts(c_tptprunningshorts)], ~(mtvisible(c_cyclistsmt)) 29: [tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756))], ~( runningshorts(c_tptprunningshorts)), ~(mtvisible(c_tptp_member2701_mt)) Gamma_30: (extend-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 23: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [genlmt( c_tptp_spindlecollectormt,c_cyclistsmt)] 24: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [genlmt(c_tptp_member3993_mt, c_cyclistsmt)], ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)) 25: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), ~(mtvisible(c_tptp_member3993_mt)), [mtvisible( c_cyclistsmt)] 26: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 27: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 28: [runningshorts(c_tptprunningshorts)], ~(mtvisible(c_cyclistsmt)) 29: [tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756))], ~( runningshorts(c_tptprunningshorts)), ~(mtvisible(c_tptp_member2701_mt)) 30: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_31: (move) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 23: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [genlmt( c_tptp_spindlecollectormt,c_cyclistsmt)] 24: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [genlmt(c_tptp_member3993_mt, c_cyclistsmt)], ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)) 25: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), ~(mtvisible(c_tptp_member3993_mt)), [mtvisible( c_cyclistsmt)] 26: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 27: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 28: [runningshorts(c_tptprunningshorts)], ~(mtvisible(c_cyclistsmt)) 29: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] 30: [tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756))], ~( runningshorts(c_tptprunningshorts)), ~(mtvisible(c_tptp_member2701_mt)) Gamma_32: (resolve) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 23: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [genlmt( c_tptp_spindlecollectormt,c_cyclistsmt)] 24: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [genlmt(c_tptp_member3993_mt, c_cyclistsmt)], ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)) 25: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), ~(mtvisible(c_tptp_member3993_mt)), [mtvisible( c_cyclistsmt)] 26: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 27: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 28: [runningshorts(c_tptprunningshorts)], ~(mtvisible(c_cyclistsmt)) 29: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] 30: [~(runningshorts(c_tptprunningshorts))], ~(mtvisible(c_tptp_member2701_mt)) Gamma_33: (extend-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 23: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [genlmt( c_tptp_spindlecollectormt,c_cyclistsmt)] 24: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [genlmt(c_tptp_member3993_mt, c_cyclistsmt)], ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)) 25: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), ~(mtvisible(c_tptp_member3993_mt)), [mtvisible( c_cyclistsmt)] 26: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 27: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 28: [runningshorts(c_tptprunningshorts)], ~(mtvisible(c_cyclistsmt)) 29: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] 30: [~(runningshorts(c_tptprunningshorts))], ~(mtvisible(c_tptp_member2701_mt)) Gamma_34: (move) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 23: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [genlmt( c_tptp_spindlecollectormt,c_cyclistsmt)] 24: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [genlmt(c_tptp_member3993_mt, c_cyclistsmt)], ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)) 25: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), ~(mtvisible(c_tptp_member3993_mt)), [mtvisible( c_cyclistsmt)] 26: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 27: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 28: [~(runningshorts(c_tptprunningshorts))], ~(mtvisible(c_tptp_member2701_mt)) 29: [runningshorts(c_tptprunningshorts)], ~(mtvisible(c_cyclistsmt)) 30: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_35: (resolve) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 23: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [genlmt( c_tptp_spindlecollectormt,c_cyclistsmt)] 24: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [genlmt(c_tptp_member3993_mt, c_cyclistsmt)], ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)) 25: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), ~(mtvisible(c_tptp_member3993_mt)), [mtvisible( c_cyclistsmt)] 26: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 27: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 28: [~(runningshorts(c_tptprunningshorts))], ~(mtvisible(c_tptp_member2701_mt)) 29: ~(mtvisible(c_tptp_member2701_mt)), [~(mtvisible(c_cyclistsmt))] 30: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_36: (extend-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 23: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [genlmt( c_tptp_spindlecollectormt,c_cyclistsmt)] 24: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [genlmt(c_tptp_member3993_mt, c_cyclistsmt)], ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)) 25: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), ~(mtvisible(c_tptp_member3993_mt)), [mtvisible( c_cyclistsmt)] 26: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 27: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 28: [~(runningshorts(c_tptprunningshorts))], ~(mtvisible(c_tptp_member2701_mt)) 29: ~(mtvisible(c_tptp_member2701_mt)), [~(mtvisible(c_cyclistsmt))] 30: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_37: (move) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 23: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [genlmt( c_tptp_spindlecollectormt,c_cyclistsmt)] 24: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [genlmt(c_tptp_member3993_mt, c_cyclistsmt)], ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)) 25: ~(mtvisible(c_tptp_member2701_mt)), [~(mtvisible(c_cyclistsmt))] 26: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), ~(mtvisible(c_tptp_member3993_mt)), [mtvisible( c_cyclistsmt)] 27: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 28: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 29: [~(runningshorts(c_tptprunningshorts))], ~(mtvisible(c_tptp_member2701_mt)) 30: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_38: (resolve) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 23: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [genlmt( c_tptp_spindlecollectormt,c_cyclistsmt)] 24: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [genlmt(c_tptp_member3993_mt, c_cyclistsmt)], ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)) 25: ~(mtvisible(c_tptp_member2701_mt)), [~(mtvisible(c_cyclistsmt))] 26: [~(genlmt(c_tptp_member3993_mt,c_cyclistsmt))], ~(mtvisible(c_tptp_member3993_mt)), ~( mtvisible(c_tptp_member2701_mt)) 27: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 28: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 29: [~(runningshorts(c_tptprunningshorts))], ~(mtvisible(c_tptp_member2701_mt)) 30: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_39: (extend-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 23: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [genlmt( c_tptp_spindlecollectormt,c_cyclistsmt)] 24: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [genlmt(c_tptp_member3993_mt, c_cyclistsmt)], ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)) 25: ~(mtvisible(c_tptp_member2701_mt)), [~(mtvisible(c_cyclistsmt))] 26: [~(genlmt(c_tptp_member3993_mt,c_cyclistsmt))], ~(mtvisible(c_tptp_member3993_mt)), ~( mtvisible(c_tptp_member2701_mt)) 27: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 28: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 29: [~(runningshorts(c_tptprunningshorts))], ~(mtvisible(c_tptp_member2701_mt)) 30: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_40: (move) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 23: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [genlmt( c_tptp_spindlecollectormt,c_cyclistsmt)] 24: [~(genlmt(c_tptp_member3993_mt,c_cyclistsmt))], ~(mtvisible(c_tptp_member3993_mt)), ~( mtvisible(c_tptp_member2701_mt)) 25: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [genlmt(c_tptp_member3993_mt, c_cyclistsmt)], ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)) 26: ~(mtvisible(c_tptp_member2701_mt)), [~(mtvisible(c_cyclistsmt))] 27: ~(genlmt(c_tptp_member3993_mt,c_cyclistsmt)), [microtheory(c_cyclistsmt)] 28: [genlmt(c_cyclistsmt,c_cyclistsmt)], ~(microtheory(c_cyclistsmt)) 29: [~(runningshorts(c_tptprunningshorts))], ~(mtvisible(c_tptp_member2701_mt)) 30: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_41: (resolve) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 23: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [genlmt( c_tptp_spindlecollectormt,c_cyclistsmt)] 24: [~(genlmt(c_tptp_member3993_mt,c_cyclistsmt))], ~(mtvisible(c_tptp_member3993_mt)), ~( mtvisible(c_tptp_member2701_mt)) 25: [~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt))], ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~( mtvisible(c_tptp_member3993_mt)), ~(mtvisible(c_tptp_member2701_mt)) 26: ~(mtvisible(c_tptp_member2701_mt)), [~(mtvisible(c_cyclistsmt))] 27: [~(runningshorts(c_tptprunningshorts))], ~(mtvisible(c_tptp_member2701_mt)) 28: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_42: (extend-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 23: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [genlmt( c_tptp_spindlecollectormt,c_cyclistsmt)] 24: [~(genlmt(c_tptp_member3993_mt,c_cyclistsmt))], ~(mtvisible(c_tptp_member3993_mt)), ~( mtvisible(c_tptp_member2701_mt)) 25: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt))], ~( mtvisible(c_tptp_member3993_mt)), ~(mtvisible(c_tptp_member2701_mt)) 26: ~(mtvisible(c_tptp_member2701_mt)), [~(mtvisible(c_cyclistsmt))] 27: [~(runningshorts(c_tptprunningshorts))], ~(mtvisible(c_tptp_member2701_mt)) 28: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_43: (move) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt))], ~( mtvisible(c_tptp_member3993_mt)), ~(mtvisible(c_tptp_member2701_mt)) 23: [genlmt(c_tptp_spindleheadmt,c_cyclistsmt)] 24: ~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)), ~(genlmt(c_tptp_spindlecollectormt,c_tptp_spindleheadmt)), [genlmt( c_tptp_spindlecollectormt,c_cyclistsmt)] 25: [~(genlmt(c_tptp_member3993_mt,c_cyclistsmt))], ~(mtvisible(c_tptp_member3993_mt)), ~( mtvisible(c_tptp_member2701_mt)) 26: ~(mtvisible(c_tptp_member2701_mt)), [~(mtvisible(c_cyclistsmt))] 27: [~(runningshorts(c_tptprunningshorts))], ~(mtvisible(c_tptp_member2701_mt)) 28: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_44: (resolve) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt))], ~( mtvisible(c_tptp_member3993_mt)), ~(mtvisible(c_tptp_member2701_mt)) 23: [~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt))], ~(mtvisible(c_tptp_member3993_mt)), ~( mtvisible(c_tptp_member2701_mt)) 24: [~(genlmt(c_tptp_member3993_mt,c_cyclistsmt))], ~(mtvisible(c_tptp_member3993_mt)), ~( mtvisible(c_tptp_member2701_mt)) 25: ~(mtvisible(c_tptp_member2701_mt)), [~(mtvisible(c_cyclistsmt))] 26: [~(runningshorts(c_tptprunningshorts))], ~(mtvisible(c_tptp_member2701_mt)) 27: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_45: (extend-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 16: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 17: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 20: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 21: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 22: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt))], ~( mtvisible(c_tptp_member3993_mt)), ~(mtvisible(c_tptp_member2701_mt)) 23: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(mtvisible(c_tptp_member3993_mt)), [~( mtvisible(c_tptp_member2701_mt))] 24: [~(genlmt(c_tptp_member3993_mt,c_cyclistsmt))], ~(mtvisible(c_tptp_member3993_mt)), ~( mtvisible(c_tptp_member2701_mt)) 25: ~(mtvisible(c_tptp_member2701_mt)), [~(mtvisible(c_cyclistsmt))] 26: [~(runningshorts(c_tptprunningshorts))], ~(mtvisible(c_tptp_member2701_mt)) 27: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_46: (move) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(mtvisible(c_tptp_member3993_mt)), [~( mtvisible(c_tptp_member2701_mt))] 16: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [mtvisible( c_tptp_member2701_mt)], ~(mtvisible(c_tptp_spindlecollectormt)) 17: [relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))], ~( mtvisible(c_tptp_member2701_mt)) 18: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [binarypredicate( c_tptpofobject)] 19: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [collection( c_runningshorts)] 20: ~(relationallinstance(c_tptpofobject,c_runningshorts,f_tptpquantityfn_2(n_756))), [thing( f_tptpquantityfn_2(n_756))] 21: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 22: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 23: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [~(genlmt(c_tptp_spindleheadmt,c_cyclistsmt))], ~( mtvisible(c_tptp_member3993_mt)), ~(mtvisible(c_tptp_member2701_mt)) 24: [~(genlmt(c_tptp_member3993_mt,c_cyclistsmt))], ~(mtvisible(c_tptp_member3993_mt)), ~( mtvisible(c_tptp_member2701_mt)) 25: ~(mtvisible(c_tptp_member2701_mt)), [~(mtvisible(c_cyclistsmt))] 26: [~(runningshorts(c_tptprunningshorts))], ~(mtvisible(c_tptp_member2701_mt)) 27: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_47: (resolve) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(mtvisible(c_tptp_member3993_mt)), [~( mtvisible(c_tptp_member2701_mt))] 16: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt))], ~( mtvisible(c_tptp_member3993_mt)), ~(mtvisible(c_tptp_spindlecollectormt)) 17: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 18: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 19: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_48: (extend-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member2701_mt)] 15: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(mtvisible(c_tptp_member3993_mt)), [~( mtvisible(c_tptp_member2701_mt))] 16: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), [~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt))], ~( mtvisible(c_tptp_member3993_mt)), ~(mtvisible(c_tptp_spindlecollectormt)) 17: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 18: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 19: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_49: (move) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member3993_mt,c_tptp_spindleheadmt)), [~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt))], ~( mtvisible(c_tptp_member3993_mt)), ~(mtvisible(c_tptp_spindlecollectormt)) 15: [genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)] 16: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(mtvisible(c_tptp_member3993_mt)), [~( mtvisible(c_tptp_member2701_mt))] 17: ~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt)), [microtheory( c_tptp_member2701_mt)] 18: [genlmt(c_tptp_member2701_mt,c_tptp_member2701_mt)], ~(microtheory(c_tptp_member2701_mt)) 19: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_50: (resolve) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member3993_mt,c_tptp_spindleheadmt)), [~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt))], ~( mtvisible(c_tptp_member3993_mt)), ~(mtvisible(c_tptp_spindlecollectormt)) 15: [~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt))], ~(mtvisible(c_tptp_member3993_mt)), ~( mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(mtvisible(c_tptp_member3993_mt)), [~( mtvisible(c_tptp_member2701_mt))] 17: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_51: (extend-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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_member3993_mt,c_tptp_spindleheadmt)), [~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt))], ~( mtvisible(c_tptp_member3993_mt)), ~(mtvisible(c_tptp_spindlecollectormt)) 15: [~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt))], ~(mtvisible(c_tptp_member3993_mt)), ~( mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(mtvisible(c_tptp_member3993_mt)), [~( mtvisible(c_tptp_member2701_mt))] 17: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_52: (move) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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))], ~(mtvisible(c_tptp_member3993_mt)), ~( mtvisible(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_member3993_mt,c_tptp_spindleheadmt)), [~(genlmt(c_tptp_spindlecollectormt,c_tptp_member2701_mt))], ~( mtvisible(c_tptp_member3993_mt)), ~(mtvisible(c_tptp_spindlecollectormt)) 16: ~(genlmt(c_tptp_member3993_mt,c_tptp_spindleheadmt)), ~(mtvisible(c_tptp_member3993_mt)), [~( mtvisible(c_tptp_member2701_mt))] 17: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_53: (resolve) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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))], ~(mtvisible(c_tptp_member3993_mt)), ~( mtvisible(c_tptp_spindlecollectormt)) 10: [~(mtvisible(c_tptp_member3993_mt))], ~(mtvisible(c_tptp_spindlecollectormt)) 11: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_54: (extend-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 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))], ~(mtvisible(c_tptp_member3993_mt)), ~( mtvisible(c_tptp_spindlecollectormt)) 10: [~(mtvisible(c_tptp_member3993_mt))], ~(mtvisible(c_tptp_spindlecollectormt)) 11: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_55: (move) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: [~(mtvisible(c_tptp_member3993_mt))], ~(mtvisible(c_tptp_spindlecollectormt)) 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))], ~(mtvisible(c_tptp_member3993_mt)), ~( mtvisible(c_tptp_spindlecollectormt)) 11: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_56: (resolve) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: [~(mtvisible(c_tptp_member3993_mt))], ~(mtvisible(c_tptp_spindlecollectormt)) 5: [~(genlmt(c_tptp_spindlecollectormt,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: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_57: (extend-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 3: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 4: [~(mtvisible(c_tptp_member3993_mt))], ~(mtvisible(c_tptp_spindlecollectormt)) 5: [~(genlmt(c_tptp_spindlecollectormt,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: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_58: (move) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 3: [~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt))], ~(mtvisible(c_tptp_spindlecollectormt)) 4: [genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt)] 5: [~(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: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_59: (resolve) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 3: [~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt))], ~(mtvisible(c_tptp_spindlecollectormt)) 4: [~(mtvisible(c_tptp_spindlecollectormt))] 5: [~(mtvisible(c_tptp_member3993_mt))], ~(mtvisible(c_tptp_spindlecollectormt)) 6: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_60: (extend-conflict) 0: [mtvisible(c_tptp_spindlecollectormt)] 1: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 2: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 3: [~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt))], ~(mtvisible(c_tptp_spindlecollectormt)) 4: [~(mtvisible(c_tptp_spindlecollectormt))] 5: [~(mtvisible(c_tptp_member3993_mt))], ~(mtvisible(c_tptp_spindlecollectormt)) 6: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_61: (move) 0: [~(mtvisible(c_tptp_spindlecollectormt))] 1: [mtvisible(c_tptp_spindlecollectormt)] 2: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 3: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 4: [~(genlmt(c_tptp_spindlecollectormt,c_tptp_member3993_mt))], ~(mtvisible(c_tptp_spindlecollectormt)) 5: [~(mtvisible(c_tptp_member3993_mt))], ~(mtvisible(c_tptp_spindlecollectormt)) 6: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] Gamma_62: (resolve) 0: [~(mtvisible(c_tptp_spindlecollectormt))] 1: [] 2: [natargument(f_tptpquantityfn_2(X0),n_1,X0)] 3: [natfunction(f_tptpquantityfn_2(X0),c_tptpquantityfn_2)] 4: [~(tptpofobject(c_tptprunningshorts,f_tptpquantityfn_2(n_756)))] SZS status Unsatisfiable