?-op(140,fy,neg).
?-op(160, xfx, [and, or, imp, revimp, nand, nor, notimp, notrevimp]).

member(X,[X|_]).
member(X,[_|Xs]) :- member(X,Xs).

remove(_X,[],[]).
remove(X,[X|Xs],Ys) :-
	remove(X,Xs,Ys).
remove(X,[Y|Xs],[Y|Ys]) :-
	X \= Y,
	remove(X,Xs,Ys).

append([],Xs,Xs).
append([X|Xs],Ys,[X|Zs]) :-
	append(Xs,Ys,Zs).

is_unary(neg neg _X).
is_unary(neg true).
is_unary(neg false).

is_conjunctive(_X and _Y).
is_conjunctive(neg(_X or _Y)).
is_conjunctive(neg(_X imp _Y)).
is_conjunctive(neg(_X revimp _Y)).
is_conjunctive(neg(_X nand _Y)).
is_conjunctive(_X nor _Y).
is_conjunctive(_X notimp _Y).
is_conjunctive(_X notrevimp _Y).

is_disjunctive(neg(_X and _Y)).
is_disjunctive(_X or _Y).
is_disjunctive(_X imp _Y).
is_disjunctive(_X revimp _Y).
is_disjunctive(_X nand _Y).
is_disjunctive(neg(_X nor _Y)).
is_disjunctive(neg(_X notimp _Y)).
is_disjunctive(neg(_X notrevimp _Y)).

component(neg neg X, X).
component(neg true, false).
component(neg false, true).

components(X and Y, X,Y).
components(neg(X and Y), neg X, neg Y).
components(X or Y,X,Y).
components(neg(X or Y), neg X, neg Y).
components(X imp Y, neg X, Y).
components(neg(X imp Y), X, neg Y).
components(X revimp Y, X, neg Y).
components(neg(X revimp Y), neg X, Y).
components(X nand Y, neg X, neg Y).
components(neg (X nand Y), X,Y).
components(X nor Y,neg X, neg Y).
components(neg(X nor Y), X,Y).
components(X notimp Y, X, neg Y).
components(neg(X notimp Y), neg X, Y).
components(X notrevimp Y, neg X, Y).
components(neg(X notrevimp Y), X, neg Y). 

stepCNF([C|Cs],NCs) :-
	member(Formula,C),
	is_unary(Formula),
	component(Formula,Newformula),
	remove(Formula,C,NC0),
	append(NC0,[Newformula],NC),
	append(Cs,[NC],NCs).
stepCNF([C|Cs],NCs) :-
	member(Beta,C),
	is_disjunctive(Beta),
	components(Beta,Beta1,Beta2),
	remove(Beta,C,NC0),
	append(NC0,[Beta1,Beta2],NC),
	append(Cs,[NC],NCs).
stepCNF([C|Cs],NCs) :-
	member(Alpha,C),
	is_conjunctive(Alpha),
	components(Alpha,Alpha1,Alpha2),
	remove(Alpha,C,NC0),
	append(NC0,[Alpha1],NC1),
	append(NC0,[Alpha2],NC2),
	append(Cs,[NC1,NC2],NCs).	
stepCNF([C|Cs],[C|NCs]) :-
	stepCNF(Cs,NCs).

% tests
:-stepCNF([[neg neg p]],[[p]]).
:-stepCNF([[p or q]],[[p,q]]).
:-stepCNF([[p and q]],[[p],[q]]).
:-stepCNF([[(p imp (q imp r)) imp ((p imp q) imp (p imp r))]],X).

expand1(Cs,Cs).
expand1(Cs,NCs) :-
	stepCNF(Cs,Cs0),
	expand1(Cs0,NCs).

expand2(Cs,NCs) :-
	stepCNF(Cs,Cs0),
	expand2(Cs0,NCs).
expand2(Cs,Cs).

towards_CNF(X,Y) :- expand1([[X]],Y).

clauseform(X,Y) :- expand2([[X]],Y).

% tests
:-towards_CNF((p imp (q imp r)) imp ((p imp q) imp (p imp r)),X).