/*
problem-set/pelletier/p46.clauses

description:

Full Predicate Logic (without Identities and Functions)..
(Ax)(Fx & (Ay)[Fy & Hyx -> Gy] -> Gx).
{(Ex)(Fx & -Gx) ->.
 (Ex)(Fx & -Gx & (Ay)(Fy & -Gy -> Jxy)}.
(Ax)(Ay)(Fx & Fy & Hxy -> -Jyx).
--------------------------------.
(Ax)(Fx -> Gx).


premises
(all x ((F(x) & (all y ((F(y) & H(y,x)) -> G(y)))) -> G(x))).
((exists x (F(x) & -G(x))) -> 
	(exists x (F(x) & (-G(x) & (all y ((F(y) & -G(y)) -> J(x,y))))))).
(all x all y ((F(x) & (F(y) & H(x,y))) -> -J(y,x))).

denial of conclusion
-(all x (F(x) -> G(x))).
*/


first_predicate_precedence( [f, g, h, j] ).
precedence( [f1,c1, c2] ).
predicates( [f,g,h,j] ).


axiom( [ [f(X)], [f(f1(X)), g(X)] ] ).
axiom( [ [f(X)], [ h(f1(X),X), g(X)] ] ).
axiom( [ [f(X), g(f1(X))], [g(X)] ] ).
axiom( [ [f(X)], [g(X), f(c1)] ] ).
axiom( [ [f(X), g(c1)], [g(X)] ] ).
axiom( [ [f(X), f(Y) ], [g(X),g(Y),j(c1,Y)] ] ).
axiom( [ [f(X), f(Y), h(X,Y),j(Y,X)], [] ] ).
axiom( [ [], [f(c2)] ] ).
axiom( [ [g(c2)], [] ] ).