wtrue(L):- tcall(L),get_residual(demo_t(L),[]).
wfalse(L):- tcall(L),\+ get_residual(demo_tu(L),_).
wund(L):- tcall(L),\+ get_residual(demo_t(L),[]),
	  get_residual(demo_tu(L),_).

tcall(L):- call(L),fail.
tcall(_).

demo(A):-  demo_t(A). 
demo(A):-  demo_tu(A).

:- table demo_t/1, demo_tu/1.  
demo_t(true):-!.
demo_tu(true):-!.
demo_t(','(A,B)):-!, demo_t(A),demo_t(B).
demo_tu(','(A,B)):-!, demo_tu(A),demo_tu(B).
demo_t(not A):-!, tnot(demo_tu(A)). 
demo_tu(not A):-!, tnot(demo_t(A)). 
demo_t(A):- clause(A,B), demo_t(B). 
demo_tu(A):- clause(A,B), demo_tu(B),
exchange(A,A_opp),demo_tu(not A_opp). 

exchange(-A,A):-!. 
exchange(A,-A).