/*

This is an example that was obtained from translating
some ALC specification into Maslov's class K.

We are interested in a finite saturation of such theories to be
able to read off the concept hierarchies.

Ordered resolution (with the right kind of ordering,
function symbols must be greater than predicates)
is a decision procedure for class K,
i.e., will always terminate if the usual simplifications
are carried out.

*/


predicates( [concept16,child,parent,grandparent,mother,male,father,fatherWithSonsOnly,concept17,man, woman,concept19,concept18,human,male,female] ).

axiom( [ [concept16(A),child(A,B)], [male(B)] ] ).
axiom( [ [], [child(A,f1(A)),concept16(A)] ] ).
axiom( [ [male(f1(A))], [concept16(A)] ] ).
axiom( [ [fatherWithSonsOnly(C)], [father(C)] ] ).
axiom( [ [fatherWithSonsOnly(C)], [concept16(C)] ] ).
axiom( [ [father(C),concept16(C)], [fatherWithSonsOnly(C)] ] ).
axiom( [ [concept17(D)], [child(D,f2(D))] ] ).
axiom( [ [concept17(D)], [parent(f2(D))] ] ).
axiom( [ [child(D,E),parent(E)], [concept17(D)] ] ).
axiom( [ [grandparent(F)], [parent(F)] ] ).
axiom( [ [grandparent(F)], [concept17(F)] ] ).
axiom( [ [parent(F),concept17(F)], [grandparent(F)] ] ).
axiom( [ [parent(G)], [mother(G),father(G)] ] ).
axiom( [ [mother(G)], [parent(G)] ] ).
axiom( [ [father(G)], [parent(G)] ] ).
axiom( [ [concept18(H)], [child(H,f3(H))] ] ).
axiom( [ [concept18(H)], [human(f3(H))] ] ).
axiom( [ [child(H,I),human(I)], [concept18(H)] ] ).
axiom( [ [father(J)], [man(J)] ] ).
axiom( [ [father(J)], [concept18(J)] ] ).
axiom( [ [man(J),concept18(J)], [father(J)] ] ).
axiom( [ [concept19(K)], [child(K,f4(K))] ] ).
axiom( [ [concept19(K)], [human(f4(K))] ] ).
axiom( [ [child(K,L),human(L)], [concept19(K)] ] ).
axiom( [ [mother(M)], [woman(M)] ] ).
axiom( [ [mother(M)], [concept19(M)] ] ).
axiom( [ [woman(M),concept19(M)], [mother(M)] ] ).
axiom( [ [woman(N)], [human(N)] ] ).
axiom( [ [woman(N)], [female(N)] ] ).
axiom( [ [human(N),female(N)], [woman(N)] ] ).
axiom( [ [man(O)], [human(O)] ] ).
axiom( [ [man(O)], [male(O)] ] ).
axiom( [ [human(O),male(O)], [man(O)] ] ).
axiom( [ [male(P),female(P)], [] ] ).
axiom( [ [female(Q),male(Q)], [] ] ).

%precedence([f4,f3,f2,f1,child,woman,parent,mother,man,male,human,grandparent,female,fatherWithSonsOnly,father,concept19,concept18,concept17,concept16]).


:-sama([]).
:-sarp([1,2,4,6]).