let rec isConsistent :Prop list*Prop list -> bool = function
    |[],auxlist              -> true //Base case
    |Neg(A(p))::pp,auxlist   -> if List.exists(fun y -> y = A(p)) auxlist then
                                                                            false
                                                                          else
                                                                            isConsistent(pp,A(p)::auxlist)
    |A(p)::pp,auxlist        -> if List.exists(fun y -> y = A(p)) auxlist then
                                                                            false
                                                                          else
                                                                            isConsistent(pp,A(p)::auxlist)