Test satisfaisability of the input formula --> Satisfiable ---------------------------------------- Model : % domain size is 1 y = !1 ---------------------------------------- Negative model : % domain size is 2 p(!1) <=> $true p(!2) <=> $false y = !1 ----------------------------------------