aus(B,V,F):-write(B),write(V),write(F).
din(B,F):-write('Bedingung: '),readln(B),write('Folgerung: '),readln(F).
ein:-din(B,F),not(clause(dat(B,F),true)),asserta(dat(B,F)),aus(B,'=>',F),nl,
     write('Fortsetzung(j/n) '),readln(A),nl,A=[j],ein.
dimp(B,F):-clause(dat(A,F),true,X),erase(X),asserta(dat(A,F)),aus(F,'<=',''),
           dimp(B,A).
dimp(B,_):-write(B).
impl:-din(B,F),dimp(B,F).