%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] Gamma_1: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) Gamma_2: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] Gamma_3: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] Gamma_4: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) Gamma_5: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] Gamma_6: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] Gamma_7: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) Gamma_8: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] Gamma_9: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) Gamma_10: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] Gamma_11: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] Gamma_12: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] Gamma_13: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] Gamma_14: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) Gamma_15: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] Gamma_16: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) Gamma_17: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] Gamma_18: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] Gamma_19: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] Gamma_20: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] Gamma_21: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) Gamma_22: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) Gamma_23: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 23: [genlmt(c_universalvocabularymt,c_corecyclmt)] Gamma_24: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 23: [genlmt(c_universalvocabularymt,c_corecyclmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) Gamma_25: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 23: [genlmt(c_universalvocabularymt,c_corecyclmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] Gamma_26: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 23: [genlmt(c_universalvocabularymt,c_corecyclmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) Gamma_27: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 23: [genlmt(c_universalvocabularymt,c_corecyclmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 27: [mtvisible(c_universalvocabularymt)] Gamma_28: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 23: [genlmt(c_universalvocabularymt,c_corecyclmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 27: [mtvisible(c_universalvocabularymt)] 28: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] Gamma_29: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 23: [genlmt(c_universalvocabularymt,c_corecyclmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 27: [mtvisible(c_universalvocabularymt)] 28: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 29: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] Gamma_30: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 23: [genlmt(c_universalvocabularymt,c_corecyclmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 27: [mtvisible(c_universalvocabularymt)] 28: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 29: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 30: [mtvisible(c_basekb)] Gamma_31: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 23: [genlmt(c_universalvocabularymt,c_corecyclmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 27: [mtvisible(c_universalvocabularymt)] 28: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 29: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 30: [mtvisible(c_basekb)] 31: [transitivebinarypredicate(c_genlmt)] Gamma_32: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 23: [genlmt(c_universalvocabularymt,c_corecyclmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 27: [mtvisible(c_universalvocabularymt)] 28: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 29: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 30: [mtvisible(c_basekb)] 31: [transitivebinarypredicate(c_genlmt)] 32: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) Gamma_33: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 23: [genlmt(c_universalvocabularymt,c_corecyclmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 27: [mtvisible(c_universalvocabularymt)] 28: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 29: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 30: [mtvisible(c_basekb)] 31: [transitivebinarypredicate(c_genlmt)] 32: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 33: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] Gamma_34: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 23: [genlmt(c_universalvocabularymt,c_corecyclmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 27: [mtvisible(c_universalvocabularymt)] 28: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 29: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 30: [mtvisible(c_basekb)] 31: [transitivebinarypredicate(c_genlmt)] 32: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 33: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] 34: ~(isa(c_genlmt,c_transitivebinarypredicate)), [collection(c_transitivebinarypredicate)] Gamma_35: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 23: [genlmt(c_universalvocabularymt,c_corecyclmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 27: [mtvisible(c_universalvocabularymt)] 28: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 29: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 30: [mtvisible(c_basekb)] 31: [transitivebinarypredicate(c_genlmt)] 32: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 33: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] 34: ~(isa(c_genlmt,c_transitivebinarypredicate)), [collection(c_transitivebinarypredicate)] 35: [isa(c_transitivebinarypredicate,c_collection)], ~(collection(c_transitivebinarypredicate)) Gamma_36: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 23: [genlmt(c_universalvocabularymt,c_corecyclmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 27: [mtvisible(c_universalvocabularymt)] 28: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 29: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 30: [mtvisible(c_basekb)] 31: [transitivebinarypredicate(c_genlmt)] 32: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 33: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] 34: ~(isa(c_genlmt,c_transitivebinarypredicate)), [collection(c_transitivebinarypredicate)] 35: [isa(c_transitivebinarypredicate,c_collection)], ~(collection(c_transitivebinarypredicate)) 36: ~(isa(c_transitivebinarypredicate,c_collection)), [thing(c_transitivebinarypredicate)] Gamma_37: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 23: [genlmt(c_universalvocabularymt,c_corecyclmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 27: [mtvisible(c_universalvocabularymt)] 28: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 29: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 30: [mtvisible(c_basekb)] 31: [transitivebinarypredicate(c_genlmt)] 32: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 33: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] 34: ~(isa(c_genlmt,c_transitivebinarypredicate)), [collection(c_transitivebinarypredicate)] 35: [isa(c_transitivebinarypredicate,c_collection)], ~(collection(c_transitivebinarypredicate)) 36: ~(isa(c_transitivebinarypredicate,c_collection)), [thing(c_transitivebinarypredicate)] 37: [individual(c_xskijump_thegame)] Gamma_38: (extend-no-conflict) 0: [disjointwith(c_xskijump_thegame, c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 23: [genlmt(c_universalvocabularymt,c_corecyclmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 27: [mtvisible(c_universalvocabularymt)] 28: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 29: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 30: [mtvisible(c_basekb)] 31: [transitivebinarypredicate(c_genlmt)] 32: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 33: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] 34: ~(isa(c_genlmt,c_transitivebinarypredicate)), [collection(c_transitivebinarypredicate)] 35: [isa(c_transitivebinarypredicate,c_collection)], ~(collection(c_transitivebinarypredicate)) 36: ~(isa(c_transitivebinarypredicate,c_collection)), [thing(c_transitivebinarypredicate)] 37: [individual(c_xskijump_thegame)] 38: [isa(c_xskijump_thegame,c_individual)], ~(individual(c_xskijump_thegame)) Gamma_39: (extend-conflict) 0: [disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 23: [genlmt(c_universalvocabularymt,c_corecyclmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 27: [mtvisible(c_universalvocabularymt)] 28: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 29: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 30: [mtvisible(c_basekb)] 31: [transitivebinarypredicate(c_genlmt)] 32: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 33: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] 34: ~(isa(c_genlmt,c_transitivebinarypredicate)), [collection(c_transitivebinarypredicate)] 35: [isa(c_transitivebinarypredicate,c_collection)], ~(collection(c_transitivebinarypredicate)) 36: ~(isa(c_transitivebinarypredicate,c_collection)), [thing(c_transitivebinarypredicate)] 37: [individual(c_xskijump_thegame)] 38: [isa(c_xskijump_thegame,c_individual)], ~(individual(c_xskijump_thegame)) 39: [~(isa(c_xskijump_thegame,c_individual))], ~(isa(c_xskijump_thegame,c_collection)), ~( disjointwith(c_collection,c_individual)) Gamma_40: (move) 0: [disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 23: [genlmt(c_universalvocabularymt,c_corecyclmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 27: [mtvisible(c_universalvocabularymt)] 28: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 29: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 30: [mtvisible(c_basekb)] 31: [transitivebinarypredicate(c_genlmt)] 32: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 33: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] 34: ~(isa(c_genlmt,c_transitivebinarypredicate)), [collection(c_transitivebinarypredicate)] 35: [isa(c_transitivebinarypredicate,c_collection)], ~(collection(c_transitivebinarypredicate)) 36: ~(isa(c_transitivebinarypredicate,c_collection)), [thing(c_transitivebinarypredicate)] 37: [individual(c_xskijump_thegame)] 38: [~(isa(c_xskijump_thegame,c_individual))], ~(isa(c_xskijump_thegame,c_collection)), ~( disjointwith(c_collection,c_individual)) 39: [isa(c_xskijump_thegame,c_individual)], ~(individual(c_xskijump_thegame)) Gamma_41: (resolve) 0: [disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 23: [genlmt(c_universalvocabularymt,c_corecyclmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 27: [mtvisible(c_universalvocabularymt)] 28: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 29: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 30: [mtvisible(c_basekb)] 31: [transitivebinarypredicate(c_genlmt)] 32: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 33: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] 34: ~(isa(c_genlmt,c_transitivebinarypredicate)), [collection(c_transitivebinarypredicate)] 35: [isa(c_transitivebinarypredicate,c_collection)], ~(collection(c_transitivebinarypredicate)) 36: ~(isa(c_transitivebinarypredicate,c_collection)), [thing(c_transitivebinarypredicate)] 37: [individual(c_xskijump_thegame)] 38: [~(isa(c_xskijump_thegame,c_individual))], ~(isa(c_xskijump_thegame,c_collection)), ~( disjointwith(c_collection,c_individual)) 39: ~(isa(c_xskijump_thegame,c_collection)), ~(disjointwith(c_collection,c_individual)), [~( individual(c_xskijump_thegame))] Gamma_42: (extend-conflict) 0: [disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 23: [genlmt(c_universalvocabularymt,c_corecyclmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 27: [mtvisible(c_universalvocabularymt)] 28: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 29: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 30: [mtvisible(c_basekb)] 31: [transitivebinarypredicate(c_genlmt)] 32: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 33: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] 34: ~(isa(c_genlmt,c_transitivebinarypredicate)), [collection(c_transitivebinarypredicate)] 35: [isa(c_transitivebinarypredicate,c_collection)], ~(collection(c_transitivebinarypredicate)) 36: ~(isa(c_transitivebinarypredicate,c_collection)), [thing(c_transitivebinarypredicate)] 37: [individual(c_xskijump_thegame)] 38: [~(isa(c_xskijump_thegame,c_individual))], ~(isa(c_xskijump_thegame,c_collection)), ~( disjointwith(c_collection,c_individual)) 39: ~(isa(c_xskijump_thegame,c_collection)), ~(disjointwith(c_collection,c_individual)), [~( individual(c_xskijump_thegame))] Gamma_43: (move) 0: [disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 23: [genlmt(c_universalvocabularymt,c_corecyclmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 27: [mtvisible(c_universalvocabularymt)] 28: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 29: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 30: [mtvisible(c_basekb)] 31: [transitivebinarypredicate(c_genlmt)] 32: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 33: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] 34: ~(isa(c_genlmt,c_transitivebinarypredicate)), [collection(c_transitivebinarypredicate)] 35: [isa(c_transitivebinarypredicate,c_collection)], ~(collection(c_transitivebinarypredicate)) 36: ~(isa(c_transitivebinarypredicate,c_collection)), [thing(c_transitivebinarypredicate)] 37: ~(isa(c_xskijump_thegame,c_collection)), ~(disjointwith(c_collection,c_individual)), [~( individual(c_xskijump_thegame))] 38: [individual(c_xskijump_thegame)] 39: [~(isa(c_xskijump_thegame,c_individual))], ~(isa(c_xskijump_thegame,c_collection)), ~( disjointwith(c_collection,c_individual)) Gamma_44: (resolve) 0: [disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 23: [genlmt(c_universalvocabularymt,c_corecyclmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 27: [mtvisible(c_universalvocabularymt)] 28: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 29: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 30: [mtvisible(c_basekb)] 31: [transitivebinarypredicate(c_genlmt)] 32: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 33: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] 34: ~(isa(c_genlmt,c_transitivebinarypredicate)), [collection(c_transitivebinarypredicate)] 35: [isa(c_transitivebinarypredicate,c_collection)], ~(collection(c_transitivebinarypredicate)) 36: ~(isa(c_transitivebinarypredicate,c_collection)), [thing(c_transitivebinarypredicate)] 37: ~(isa(c_xskijump_thegame,c_collection)), ~(disjointwith(c_collection,c_individual)), [~( individual(c_xskijump_thegame))] 38: [~(isa(c_xskijump_thegame,c_collection))], ~(disjointwith(c_collection,c_individual)) 39: [~(isa(c_xskijump_thegame,c_individual))], ~(isa(c_xskijump_thegame,c_collection)), ~( disjointwith(c_collection,c_individual)) Gamma_45: (extend-conflict) 0: [disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [disjointwith(c_collection,c_individual)] 14: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 15: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 16: [isa(c_individual,c_collection)], ~(collection(c_individual)) 17: ~(isa(c_individual,c_collection)), [thing(c_individual)] 18: [genlmt(c_corecyclmt,c_logicaltruthmt)] 19: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 21: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 22: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 23: [genlmt(c_universalvocabularymt,c_corecyclmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 26: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 27: [mtvisible(c_universalvocabularymt)] 28: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 29: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 30: [mtvisible(c_basekb)] 31: [transitivebinarypredicate(c_genlmt)] 32: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 33: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] 34: ~(isa(c_genlmt,c_transitivebinarypredicate)), [collection(c_transitivebinarypredicate)] 35: [isa(c_transitivebinarypredicate,c_collection)], ~(collection(c_transitivebinarypredicate)) 36: ~(isa(c_transitivebinarypredicate,c_collection)), [thing(c_transitivebinarypredicate)] 37: ~(isa(c_xskijump_thegame,c_collection)), ~(disjointwith(c_collection,c_individual)), [~( individual(c_xskijump_thegame))] 38: ~(isa(c_xskijump_thegame,c_collection)), [~(disjointwith(c_collection,c_individual))] 39: [~(isa(c_xskijump_thegame,c_individual))], ~(isa(c_xskijump_thegame,c_collection)), ~( disjointwith(c_collection,c_individual)) Gamma_46: (move) 0: [disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: ~(isa(c_xskijump_thegame,c_collection)), [~(disjointwith(c_collection,c_individual))] 14: [disjointwith(c_collection,c_individual)] 15: [disjointwith(c_individual,c_collection)], ~(disjointwith(c_collection,c_individual)) 16: ~(disjointwith(c_individual,c_collection)), [collection(c_individual)] 17: [isa(c_individual,c_collection)], ~(collection(c_individual)) 18: ~(isa(c_individual,c_collection)), [thing(c_individual)] 19: [genlmt(c_corecyclmt,c_logicaltruthmt)] 20: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 21: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 22: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 23: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 24: [genlmt(c_universalvocabularymt,c_corecyclmt)] 25: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 26: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 27: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 28: [mtvisible(c_universalvocabularymt)] 29: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 30: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 31: [mtvisible(c_basekb)] 32: [transitivebinarypredicate(c_genlmt)] 33: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 34: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] 35: ~(isa(c_genlmt,c_transitivebinarypredicate)), [collection(c_transitivebinarypredicate)] 36: [isa(c_transitivebinarypredicate,c_collection)], ~(collection(c_transitivebinarypredicate)) 37: ~(isa(c_transitivebinarypredicate,c_collection)), [thing(c_transitivebinarypredicate)] 38: ~(isa(c_xskijump_thegame,c_collection)), ~(disjointwith(c_collection,c_individual)), [~( individual(c_xskijump_thegame))] 39: [~(isa(c_xskijump_thegame,c_individual))], ~(isa(c_xskijump_thegame,c_collection)), ~( disjointwith(c_collection,c_individual)) Gamma_47: (resolve) 0: [disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: ~(isa(c_xskijump_thegame,c_collection)), [~(disjointwith(c_collection,c_individual))] 14: [~(isa(c_xskijump_thegame,c_collection))] 15: [genlmt(c_corecyclmt,c_logicaltruthmt)] 16: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 17: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 18: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 19: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 20: [genlmt(c_universalvocabularymt,c_corecyclmt)] 21: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 22: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 23: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 24: [mtvisible(c_universalvocabularymt)] 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 26: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 27: [mtvisible(c_basekb)] 28: [transitivebinarypredicate(c_genlmt)] 29: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 30: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] 31: ~(isa(c_genlmt,c_transitivebinarypredicate)), [collection(c_transitivebinarypredicate)] 32: [isa(c_transitivebinarypredicate,c_collection)], ~(collection(c_transitivebinarypredicate)) 33: ~(isa(c_transitivebinarypredicate,c_collection)), [thing(c_transitivebinarypredicate)] Gamma_48: (extend-conflict) 0: [disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 10: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: ~(isa(c_xskijump_thegame,c_collection)), [~(disjointwith(c_collection,c_individual))] 14: [~(isa(c_xskijump_thegame,c_collection))] 15: [genlmt(c_corecyclmt,c_logicaltruthmt)] 16: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 17: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 18: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 19: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 20: [genlmt(c_universalvocabularymt,c_corecyclmt)] 21: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 22: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 23: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 24: [mtvisible(c_universalvocabularymt)] 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 26: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 27: [mtvisible(c_basekb)] 28: [transitivebinarypredicate(c_genlmt)] 29: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 30: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] 31: ~(isa(c_genlmt,c_transitivebinarypredicate)), [collection(c_transitivebinarypredicate)] 32: [isa(c_transitivebinarypredicate,c_collection)], ~(collection(c_transitivebinarypredicate)) 33: ~(isa(c_transitivebinarypredicate,c_collection)), [thing(c_transitivebinarypredicate)] Gamma_49: (move) 0: [disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [~(isa(c_xskijump_thegame,c_collection))] 10: [isa(c_xskijump_thegame,c_collection)], ~(collection(c_xskijump_thegame)) 11: ~(isa(c_xskijump_thegame,c_collection)), [thing(c_xskijump_thegame)] 12: [arg2isa(c_disjointwith,c_collection)] 13: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 14: ~(isa(c_xskijump_thegame,c_collection)), [~(disjointwith(c_collection,c_individual))] 15: [genlmt(c_corecyclmt,c_logicaltruthmt)] 16: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 17: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 18: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 19: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 20: [genlmt(c_universalvocabularymt,c_corecyclmt)] 21: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 22: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 23: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 24: [mtvisible(c_universalvocabularymt)] 25: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 26: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 27: [mtvisible(c_basekb)] 28: [transitivebinarypredicate(c_genlmt)] 29: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 30: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] 31: ~(isa(c_genlmt,c_transitivebinarypredicate)), [collection(c_transitivebinarypredicate)] 32: [isa(c_transitivebinarypredicate,c_collection)], ~(collection(c_transitivebinarypredicate)) 33: ~(isa(c_transitivebinarypredicate,c_collection)), [thing(c_transitivebinarypredicate)] Gamma_50: (resolve) 0: [disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [~(isa(c_xskijump_thegame,c_collection))] 10: [~(collection(c_xskijump_thegame))] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [genlmt(c_corecyclmt,c_logicaltruthmt)] 14: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 15: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 16: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 17: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 18: [genlmt(c_universalvocabularymt,c_corecyclmt)] 19: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 20: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 21: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 22: [mtvisible(c_universalvocabularymt)] 23: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 25: [mtvisible(c_basekb)] 26: [transitivebinarypredicate(c_genlmt)] 27: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 28: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] 29: ~(isa(c_genlmt,c_transitivebinarypredicate)), [collection(c_transitivebinarypredicate)] 30: [isa(c_transitivebinarypredicate,c_collection)], ~(collection(c_transitivebinarypredicate)) 31: ~(isa(c_transitivebinarypredicate,c_collection)), [thing(c_transitivebinarypredicate)] Gamma_51: (extend-conflict) 0: [disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 4: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 5: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 6: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 7: [isa(c_collection,c_collection)], ~(collection(c_collection)) 8: ~(isa(c_collection,c_collection)), [thing(c_collection)] 9: [~(isa(c_xskijump_thegame,c_collection))] 10: [~(collection(c_xskijump_thegame))] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [genlmt(c_corecyclmt,c_logicaltruthmt)] 14: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 15: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 16: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 17: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 18: [genlmt(c_universalvocabularymt,c_corecyclmt)] 19: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 20: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 21: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 22: [mtvisible(c_universalvocabularymt)] 23: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 25: [mtvisible(c_basekb)] 26: [transitivebinarypredicate(c_genlmt)] 27: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 28: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] 29: ~(isa(c_genlmt,c_transitivebinarypredicate)), [collection(c_transitivebinarypredicate)] 30: [isa(c_transitivebinarypredicate,c_collection)], ~(collection(c_transitivebinarypredicate)) 31: ~(isa(c_transitivebinarypredicate,c_collection)), [thing(c_transitivebinarypredicate)] Gamma_52: (move) 0: [disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: [~(collection(c_xskijump_thegame))] 4: ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)), [collection( c_xskijump_thegame)] 5: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 6: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 7: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 8: [isa(c_collection,c_collection)], ~(collection(c_collection)) 9: ~(isa(c_collection,c_collection)), [thing(c_collection)] 10: [~(isa(c_xskijump_thegame,c_collection))] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [genlmt(c_corecyclmt,c_logicaltruthmt)] 14: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 15: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 16: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 17: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 18: [genlmt(c_universalvocabularymt,c_corecyclmt)] 19: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 20: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 21: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 22: [mtvisible(c_universalvocabularymt)] 23: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 25: [mtvisible(c_basekb)] 26: [transitivebinarypredicate(c_genlmt)] 27: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 28: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] 29: ~(isa(c_genlmt,c_transitivebinarypredicate)), [collection(c_transitivebinarypredicate)] 30: [isa(c_transitivebinarypredicate,c_collection)], ~(collection(c_transitivebinarypredicate)) 31: ~(isa(c_transitivebinarypredicate,c_collection)), [thing(c_transitivebinarypredicate)] Gamma_53: (resolve) 0: [disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: [~(collection(c_xskijump_thegame))] 4: [~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301))] 5: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 6: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 7: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 8: [isa(c_collection,c_collection)], ~(collection(c_collection)) 9: ~(isa(c_collection,c_collection)), [thing(c_collection)] 10: [~(isa(c_xskijump_thegame,c_collection))] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [genlmt(c_corecyclmt,c_logicaltruthmt)] 14: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 15: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 16: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 17: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 18: [genlmt(c_universalvocabularymt,c_corecyclmt)] 19: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 20: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 21: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 22: [mtvisible(c_universalvocabularymt)] 23: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 25: [mtvisible(c_basekb)] 26: [transitivebinarypredicate(c_genlmt)] 27: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 28: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] 29: ~(isa(c_genlmt,c_transitivebinarypredicate)), [collection(c_transitivebinarypredicate)] 30: [isa(c_transitivebinarypredicate,c_collection)], ~(collection(c_transitivebinarypredicate)) 31: ~(isa(c_transitivebinarypredicate,c_collection)), [thing(c_transitivebinarypredicate)] Gamma_54: (extend-conflict) 0: [disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)] 1: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 2: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 3: [~(collection(c_xskijump_thegame))] 4: [~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301))] 5: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 6: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 7: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 8: [isa(c_collection,c_collection)], ~(collection(c_collection)) 9: ~(isa(c_collection,c_collection)), [thing(c_collection)] 10: [~(isa(c_xskijump_thegame,c_collection))] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [genlmt(c_corecyclmt,c_logicaltruthmt)] 14: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 15: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 16: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 17: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 18: [genlmt(c_universalvocabularymt,c_corecyclmt)] 19: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 20: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 21: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 22: [mtvisible(c_universalvocabularymt)] 23: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 25: [mtvisible(c_basekb)] 26: [transitivebinarypredicate(c_genlmt)] 27: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 28: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] 29: ~(isa(c_genlmt,c_transitivebinarypredicate)), [collection(c_transitivebinarypredicate)] 30: [isa(c_transitivebinarypredicate,c_collection)], ~(collection(c_transitivebinarypredicate)) 31: ~(isa(c_transitivebinarypredicate,c_collection)), [thing(c_transitivebinarypredicate)] Gamma_55: (move) 0: [~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301))] 1: [disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)] 2: [disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)], ~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301)) 3: ~(disjointwith(c_tptpcol_16_35301,c_xskijump_thegame)), [collection( c_tptpcol_16_35301)] 4: [~(collection(c_xskijump_thegame))] 5: [isa(c_tptpcol_16_35301,c_collection)], ~(collection(c_tptpcol_16_35301)) 6: ~(isa(c_tptpcol_16_35301,c_collection)), [thing(c_tptpcol_16_35301)] 7: ~(isa(c_tptpcol_16_35301,c_collection)), [collection(c_collection)] 8: [isa(c_collection,c_collection)], ~(collection(c_collection)) 9: ~(isa(c_collection,c_collection)), [thing(c_collection)] 10: [~(isa(c_xskijump_thegame,c_collection))] 11: [arg2isa(c_disjointwith,c_collection)] 12: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 13: [genlmt(c_corecyclmt,c_logicaltruthmt)] 14: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 15: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 16: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 17: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 18: [genlmt(c_universalvocabularymt,c_corecyclmt)] 19: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 20: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 21: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 22: [mtvisible(c_universalvocabularymt)] 23: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 24: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 25: [mtvisible(c_basekb)] 26: [transitivebinarypredicate(c_genlmt)] 27: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 28: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] 29: ~(isa(c_genlmt,c_transitivebinarypredicate)), [collection(c_transitivebinarypredicate)] 30: [isa(c_transitivebinarypredicate,c_collection)], ~(collection(c_transitivebinarypredicate)) 31: ~(isa(c_transitivebinarypredicate,c_collection)), [thing(c_transitivebinarypredicate)] Gamma_56: (resolve) 0: [~(disjointwith(c_xskijump_thegame,c_tptpcol_16_35301))] 1: [] 2: [~(collection(c_xskijump_thegame))] 3: [~(isa(c_xskijump_thegame,c_collection))] 4: [arg2isa(c_disjointwith,c_collection)] 5: ~(arg2isa(c_disjointwith,c_collection)), [relation(c_disjointwith)] 6: [genlmt(c_corecyclmt,c_logicaltruthmt)] 7: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_corecyclmt)] 8: ~(genlmt(c_corecyclmt,c_logicaltruthmt)), [microtheory(c_logicaltruthmt)] 9: [genlmt(c_logicaltruthmt,c_logicaltruthmt)], ~(microtheory(c_logicaltruthmt)) 10: [genlmt(c_corecyclmt,c_corecyclmt)], ~(microtheory(c_corecyclmt)) 11: [genlmt(c_universalvocabularymt,c_corecyclmt)] 12: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), [genlmt(c_universalvocabularymt, c_logicaltruthmt)], ~(genlmt(c_corecyclmt,c_logicaltruthmt)) 13: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), [microtheory( c_universalvocabularymt)] 14: [genlmt(c_universalvocabularymt,c_universalvocabularymt)], ~(microtheory(c_universalvocabularymt)) 15: [mtvisible(c_universalvocabularymt)] 16: ~(genlmt(c_universalvocabularymt,c_logicaltruthmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_logicaltruthmt)] 17: ~(genlmt(c_universalvocabularymt,c_corecyclmt)), ~(mtvisible(c_universalvocabularymt)), [mtvisible( c_corecyclmt)] 18: [mtvisible(c_basekb)] 19: [transitivebinarypredicate(c_genlmt)] 20: [isa(c_genlmt,c_transitivebinarypredicate)], ~(transitivebinarypredicate(c_genlmt)) 21: ~(isa(c_genlmt,c_transitivebinarypredicate)), [thing(c_genlmt)] 22: ~(isa(c_genlmt,c_transitivebinarypredicate)), [collection(c_transitivebinarypredicate)] 23: [isa(c_transitivebinarypredicate,c_collection)], ~(collection(c_transitivebinarypredicate)) 24: ~(isa(c_transitivebinarypredicate,c_collection)), [thing(c_transitivebinarypredicate)] SZS status Unsatisfiable