function CNF = BR_s2CNF(s)
% BR_s2CNF - convert general logical expression to CNF
%   fully parenthesized using ~,v,^,>,=
% On input:
%     s (string): logical string
% On output:
%     CNF (string): conjunction of disjunctions
%       not is pushed into the atoms as -<int> (no negations left)
% Call:
%     s1 = '((((2)v(3))>(1))=(4)))';
%     C1 = BR_s2CNF(s1)
%        =
%   '(((((2)v(3))v(4))^((-1)v(4)))^(((-4)v((-2)v(1)))^((-4)v((-3)v(1))))))'
% Author:
%     T. Henderson
%     UU
%     Fall 2018
%

s1 = BR_remove_eq(s);
s2 = BR_remove_implies(s1);
s3 = BR_move_not_in(s2);
v = BR_max_var_in_s(s3);
CNF = BR_switch_vars(s3,v);
