%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [mtvisible(c_tptpgeo_spindlecollectormt)] Gamma_1: (extend-no-conflict) 0: [mtvisible(c_tptpgeo_spindlecollectormt)] 1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)] Gamma_2: (extend-no-conflict) 0: [mtvisible(c_tptpgeo_spindlecollectormt)] 1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)] 2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [mtvisible( c_tptpgeo_member5_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt)) Gamma_3: (extend-no-conflict) 0: [mtvisible(c_tptpgeo_spindlecollectormt)] 1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)] 2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [mtvisible( c_tptpgeo_member5_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt)) 3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_spindlecollectormt)] Gamma_4: (extend-no-conflict) 0: [mtvisible(c_tptpgeo_spindlecollectormt)] 1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)] 2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [mtvisible( c_tptpgeo_member5_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt)) 3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_spindlecollectormt)] 4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_member5_mt)] Gamma_5: (extend-no-conflict) 0: [mtvisible(c_tptpgeo_spindlecollectormt)] 1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)] 2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [mtvisible( c_tptpgeo_member5_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt)) 3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_spindlecollectormt)] 4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_member5_mt)] 5: [genlmt(c_tptpgeo_member5_mt,c_tptpgeo_member5_mt)], ~(microtheory(c_tptpgeo_member5_mt)) Gamma_6: (extend-no-conflict) 0: [mtvisible(c_tptpgeo_spindlecollectormt)] 1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)] 2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [mtvisible( c_tptpgeo_member5_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt)) 3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_spindlecollectormt)] 4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_member5_mt)] 5: [genlmt(c_tptpgeo_member5_mt,c_tptpgeo_member5_mt)], ~(microtheory(c_tptpgeo_member5_mt)) 6: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~( microtheory(c_tptpgeo_spindlecollectormt)) Gamma_7: (extend-no-conflict) 0: [mtvisible(c_tptpgeo_spindlecollectormt)] 1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)] 2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [mtvisible( c_tptpgeo_member5_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt)) 3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_spindlecollectormt)] 4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_member5_mt)] 5: [genlmt(c_tptpgeo_member5_mt,c_tptpgeo_member5_mt)], ~(microtheory(c_tptpgeo_member5_mt)) 6: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~( microtheory(c_tptpgeo_spindlecollectormt)) 7: [borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47)], ~(mtvisible(c_tptpgeo_member5_mt)) Gamma_8: (extend-no-conflict) 0: [mtvisible(c_tptpgeo_spindlecollectormt)] 1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)] 2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [mtvisible( c_tptpgeo_member5_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt)) 3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_spindlecollectormt)] 4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_member5_mt)] 5: [genlmt(c_tptpgeo_member5_mt,c_tptpgeo_member5_mt)], ~(microtheory(c_tptpgeo_member5_mt)) 6: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~( microtheory(c_tptpgeo_spindlecollectormt)) 7: [borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47)], ~(mtvisible(c_tptpgeo_member5_mt)) 8: ~(borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47)), [borderson( c_georegion_l4_x57_y47,c_georegion_l4_x56_y47)] Gamma_9: (extend-conflict) 0: [mtvisible(c_tptpgeo_spindlecollectormt)] 1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)] 2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [mtvisible( c_tptpgeo_member5_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt)) 3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_spindlecollectormt)] 4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_member5_mt)] 5: [genlmt(c_tptpgeo_member5_mt,c_tptpgeo_member5_mt)], ~(microtheory(c_tptpgeo_member5_mt)) 6: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~( microtheory(c_tptpgeo_spindlecollectormt)) 7: [borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47)], ~(mtvisible(c_tptpgeo_member5_mt)) 8: ~(borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47)), [borderson( c_georegion_l4_x57_y47,c_georegion_l4_x56_y47)] 9: [~(borderson(c_georegion_l4_x57_y47,c_georegion_l4_x56_y47))] Gamma_10: (move) 0: [mtvisible(c_tptpgeo_spindlecollectormt)] 1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)] 2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [mtvisible( c_tptpgeo_member5_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt)) 3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_spindlecollectormt)] 4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_member5_mt)] 5: [genlmt(c_tptpgeo_member5_mt,c_tptpgeo_member5_mt)], ~(microtheory(c_tptpgeo_member5_mt)) 6: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~( microtheory(c_tptpgeo_spindlecollectormt)) 7: [borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47)], ~(mtvisible(c_tptpgeo_member5_mt)) 8: [~(borderson(c_georegion_l4_x57_y47,c_georegion_l4_x56_y47))] 9: ~(borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47)), [borderson( c_georegion_l4_x57_y47,c_georegion_l4_x56_y47)] Gamma_11: (resolve) 0: [mtvisible(c_tptpgeo_spindlecollectormt)] 1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)] 2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [mtvisible( c_tptpgeo_member5_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt)) 3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_spindlecollectormt)] 4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_member5_mt)] 5: [genlmt(c_tptpgeo_member5_mt,c_tptpgeo_member5_mt)], ~(microtheory(c_tptpgeo_member5_mt)) 6: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~( microtheory(c_tptpgeo_spindlecollectormt)) 7: [borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47)], ~(mtvisible(c_tptpgeo_member5_mt)) 8: [~(borderson(c_georegion_l4_x57_y47,c_georegion_l4_x56_y47))] 9: [~(borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47))] Gamma_12: (extend-conflict) 0: [mtvisible(c_tptpgeo_spindlecollectormt)] 1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)] 2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [mtvisible( c_tptpgeo_member5_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt)) 3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_spindlecollectormt)] 4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_member5_mt)] 5: [genlmt(c_tptpgeo_member5_mt,c_tptpgeo_member5_mt)], ~(microtheory(c_tptpgeo_member5_mt)) 6: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~( microtheory(c_tptpgeo_spindlecollectormt)) 7: [borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47)], ~(mtvisible(c_tptpgeo_member5_mt)) 8: [~(borderson(c_georegion_l4_x57_y47,c_georegion_l4_x56_y47))] 9: [~(borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47))] Gamma_13: (move) 0: [mtvisible(c_tptpgeo_spindlecollectormt)] 1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)] 2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [mtvisible( c_tptpgeo_member5_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt)) 3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_spindlecollectormt)] 4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_member5_mt)] 5: [genlmt(c_tptpgeo_member5_mt,c_tptpgeo_member5_mt)], ~(microtheory(c_tptpgeo_member5_mt)) 6: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~( microtheory(c_tptpgeo_spindlecollectormt)) 7: [~(borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47))] 8: [borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47)], ~(mtvisible(c_tptpgeo_member5_mt)) 9: [~(borderson(c_georegion_l4_x57_y47,c_georegion_l4_x56_y47))] Gamma_14: (resolve) 0: [mtvisible(c_tptpgeo_spindlecollectormt)] 1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)] 2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [mtvisible( c_tptpgeo_member5_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt)) 3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_spindlecollectormt)] 4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_member5_mt)] 5: [genlmt(c_tptpgeo_member5_mt,c_tptpgeo_member5_mt)], ~(microtheory(c_tptpgeo_member5_mt)) 6: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~( microtheory(c_tptpgeo_spindlecollectormt)) 7: [~(borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47))] 8: [~(mtvisible(c_tptpgeo_member5_mt))] 9: [~(borderson(c_georegion_l4_x57_y47,c_georegion_l4_x56_y47))] Gamma_15: (extend-conflict) 0: [mtvisible(c_tptpgeo_spindlecollectormt)] 1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)] 2: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [mtvisible( c_tptpgeo_member5_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt)) 3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_spindlecollectormt)] 4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_member5_mt)] 5: [genlmt(c_tptpgeo_member5_mt,c_tptpgeo_member5_mt)], ~(microtheory(c_tptpgeo_member5_mt)) 6: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~( microtheory(c_tptpgeo_spindlecollectormt)) 7: [~(borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47))] 8: [~(mtvisible(c_tptpgeo_member5_mt))] 9: [~(borderson(c_georegion_l4_x57_y47,c_georegion_l4_x56_y47))] Gamma_16: (move) 0: [mtvisible(c_tptpgeo_spindlecollectormt)] 1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)] 2: [~(mtvisible(c_tptpgeo_member5_mt))] 3: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [mtvisible( c_tptpgeo_member5_mt)], ~(mtvisible(c_tptpgeo_spindlecollectormt)) 4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_spindlecollectormt)] 5: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_member5_mt)] 6: [genlmt(c_tptpgeo_member5_mt,c_tptpgeo_member5_mt)], ~(microtheory(c_tptpgeo_member5_mt)) 7: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~( microtheory(c_tptpgeo_spindlecollectormt)) 8: [~(borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47))] 9: [~(borderson(c_georegion_l4_x57_y47,c_georegion_l4_x56_y47))] Gamma_17: (resolve) 0: [mtvisible(c_tptpgeo_spindlecollectormt)] 1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)] 2: [~(mtvisible(c_tptpgeo_member5_mt))] 3: [~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt))], ~( mtvisible(c_tptpgeo_spindlecollectormt)) 4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_spindlecollectormt)] 5: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_member5_mt)] 6: [genlmt(c_tptpgeo_member5_mt,c_tptpgeo_member5_mt)], ~(microtheory(c_tptpgeo_member5_mt)) 7: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~( microtheory(c_tptpgeo_spindlecollectormt)) 8: [~(borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47))] 9: [~(borderson(c_georegion_l4_x57_y47,c_georegion_l4_x56_y47))] Gamma_18: (extend-conflict) 0: [mtvisible(c_tptpgeo_spindlecollectormt)] 1: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)] 2: [~(mtvisible(c_tptpgeo_member5_mt))] 3: [~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt))], ~( mtvisible(c_tptpgeo_spindlecollectormt)) 4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_spindlecollectormt)] 5: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_member5_mt)] 6: [genlmt(c_tptpgeo_member5_mt,c_tptpgeo_member5_mt)], ~(microtheory(c_tptpgeo_member5_mt)) 7: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~( microtheory(c_tptpgeo_spindlecollectormt)) 8: [~(borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47))] 9: [~(borderson(c_georegion_l4_x57_y47,c_georegion_l4_x56_y47))] Gamma_19: (move) 0: [mtvisible(c_tptpgeo_spindlecollectormt)] 1: [~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt))], ~( mtvisible(c_tptpgeo_spindlecollectormt)) 2: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)] 3: [~(mtvisible(c_tptpgeo_member5_mt))] 4: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_spindlecollectormt)] 5: ~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt)), [microtheory( c_tptpgeo_member5_mt)] 6: [genlmt(c_tptpgeo_member5_mt,c_tptpgeo_member5_mt)], ~(microtheory(c_tptpgeo_member5_mt)) 7: [genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_spindlecollectormt)], ~( microtheory(c_tptpgeo_spindlecollectormt)) 8: [~(borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47))] 9: [~(borderson(c_georegion_l4_x57_y47,c_georegion_l4_x56_y47))] Gamma_20: (resolve) 0: [mtvisible(c_tptpgeo_spindlecollectormt)] 1: [~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt))], ~( mtvisible(c_tptpgeo_spindlecollectormt)) 2: [~(mtvisible(c_tptpgeo_spindlecollectormt))] 3: [~(mtvisible(c_tptpgeo_member5_mt))] 4: [~(borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47))] 5: [~(borderson(c_georegion_l4_x57_y47,c_georegion_l4_x56_y47))] Gamma_21: (extend-conflict) 0: [mtvisible(c_tptpgeo_spindlecollectormt)] 1: [~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt))], ~( mtvisible(c_tptpgeo_spindlecollectormt)) 2: [~(mtvisible(c_tptpgeo_spindlecollectormt))] 3: [~(mtvisible(c_tptpgeo_member5_mt))] 4: [~(borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47))] 5: [~(borderson(c_georegion_l4_x57_y47,c_georegion_l4_x56_y47))] Gamma_22: (move) 0: [~(mtvisible(c_tptpgeo_spindlecollectormt))] 1: [mtvisible(c_tptpgeo_spindlecollectormt)] 2: [~(genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member5_mt))], ~( mtvisible(c_tptpgeo_spindlecollectormt)) 3: [~(mtvisible(c_tptpgeo_member5_mt))] 4: [~(borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47))] 5: [~(borderson(c_georegion_l4_x57_y47,c_georegion_l4_x56_y47))] Gamma_23: (resolve) 0: [~(mtvisible(c_tptpgeo_spindlecollectormt))] 1: [] 2: [~(mtvisible(c_tptpgeo_member5_mt))] 3: [~(borderson(c_georegion_l4_x56_y47,c_georegion_l4_x57_y47))] 4: [~(borderson(c_georegion_l4_x57_y47,c_georegion_l4_x56_y47))] SZS status Unsatisfiable