function clause = CS_unsat_clause(model,KB)
% CS_unsat_clause - return random clause not satisfied by modelS

m = length(KB);
indexes = [];
for c = 1:m
    if CS_sat(KB(c).clauses,model)==0
        indexes = [indexes,c];
    end
end
num_indexes = length(indexes);
k = randi(num_indexes);
clause = KB(indexes(k)).clauses;
