Väike võrdusloogika näide listidega

set(prolog_style_variables).
set(tptp_eq).

list(sos).

  mem(X,cons(X,L)).
  -mem(X,L) | mem(X,cons(Y,L)). 


  equal(m(X,cons(X,L)),true).
  equal(m(X,cons(Y,L)),if(m(X,L),true,eqf(X,Y))).

  equal(if(true,X,Y),X).
  equal(if(false,X,Y),Y).
  equal(if(X,Y,Y),Y).

  equal(X,conc(nil,X)).  
  equal(cons(Z,conc(L,Y)),conc(cons(Z,L),Y)).

  -equal(m(c,cons(b,cons(a,nil))),false).

  %-mem(a,   conc( cons(d,cons(d,nil)), cons(b,cons(a,cons(c,nil))) )).

end_of_list.