Fresh Clauses :

    4(1) : eq(B,C),eq(cdr(B),D) -> eq(cdr(C),D)
    5(1) : eq(B,C),eq(car(B),D) -> eq(car(C),D)
    6(1) : eq(B,C),eq(D,E),eq(cons(B,D),F) -> eq(cons(C,E),F)
    7(1) : eq(cons(B,C),D) -> eq(car(D),B)
    8(1) : eq(cons(B,C),D) -> eq(cdr(D),C)
    9(1) : eq(cons(B,C),D),eq(car(E),B),eq(cdr(F),C),eq(E,F) -> eq(D,E)

Persisting Clauses:

    1(1) : eq(B,B)
    2(1) : eq(B,C) -> eq(C,B)
    3(1) : eq(B,C),eq(C,D) -> eq(B,D)

reflexive_relation_symbol(eq).
symmetric_relation_symbol(eq).