%% File generated by tme2X utility.
%% Hope you have a nice proof!

?- -(neg_p(a, b)).
false :- q(c, d).
% q_symmetry, hypothesis.
false :- neg_q(b, c), q(c, b).
q(c, b); neg_q(b, c).
q(B_559, A_560) :- unequal(q(B_559, A_560), q(b, c)), q(A_560, B_559), unequal(q(A_560, B_559), q(b, c)).
% q_transitivity, hypothesis.
neg_q(b, c) :- neg_q(b, c), q(c, c).
neg_q(b, c) :- neg_q(b, c), q(b, b).
false :- neg_q(b, c), q(b, B_914), unequal(q(b, B_914), q(b, c)), q(B_914, c), unequal(q(B_914, c), q(b, c)).
q(b, C_1024); neg_q(b, c) :- unequal(q(b, C_1024), q(b, c)), q(c, C_1024).
q(A_1134, c); neg_q(b, c) :- unequal(q(A_1134, c), q(b, c)), q(A_1134, b).
q(A_1244, C_1245) :- unequal(q(A_1244, C_1245), q(b, c)), q(A_1244, B_1266), unequal(q(A_1244, B_1266), q(b, c)), q(B_1266, C_1245), unequal(q(B_1266, C_1245), q(b, c)).
% p_transitivity, hypothesis.
neg_p(a, b) :- neg_p(a, b), p(b, b).
neg_p(a, b) :- neg_p(a, b), p(a, a).
false :- neg_p(a, b), p(a, B_1644), unequal(p(a, B_1644), p(a, b)), p(B_1644, b), unequal(p(B_1644, b), p(a, b)).
p(a, C_1754); neg_p(a, b) :- unequal(p(a, C_1754), p(a, b)), p(b, C_1754).
p(A_1864, b); neg_p(a, b) :- unequal(p(A_1864, b), p(a, b)), p(A_1864, a).
p(A_1974, C_1975) :- unequal(p(A_1974, C_1975), p(a, b)), p(A_1974, B_1996), unequal(p(A_1974, B_1996), p(a, b)), p(B_1996, C_1975), unequal(p(B_1996, C_1975), p(a, b)).
% all_related, hypothesis.
q(a, b) :- neg_p(a, b).
p(b, c) :- neg_q(b, c).
p(A_2323, B_2324); q(A_2323, B_2324) :- unequal(p(A_2323, B_2324), p(a, b)), unequal(q(A_2323, B_2324), q(b, c)).
%----------------------------------------------------------------------