% Intuitionistic Logic:  Prove {H334, HIF4, HIF5}
%
% Reference: http://www.aarinc.org/Newsletters/091-2011-04.html

clear(auto_inference).
set(hyper_resolution).

formulas(sos).

% condensed detachment
-P(x) | -P(i(x,y)) | P(y).

P(i(x,i(y,x)))                        # label("A1").
P(i(i(x,i(y,z)),i(i(x,y),i(x,z))))    # label("A2").
P(i(k(x,y),x))                        # label("A3").
P(i(k(x,y),y))                        # label("A4").
P(i(i(x,y),i(i(x,z),i(x,k(y,z)))))    # label("A5").
P(i(x,a(x,y)))                        # label("A6").
P(i(x,a(y,x)))                        # label("A7").
P(i(i(x,y),i(i(z,y),i(a(x,z),y))))    # label("A8").
P(i(i(x,n(y)),i(y,n(x))))             # label("A9").
P(i(n(x),i(x,y)))                     # label("A10").

end_of_list.

formulas(goals).

P(i(i(x,y),i(a(x,z),a(y,z)))) # label("H334").

P(k(i(a(k(x,y),z),k(a(x,z),a(y,z))),i(k(a(x,z),a(y,z)),a(k(x,y),z))))
   # label("HIF4").

P(k(i(n(a(x,y)),k(n(x),n(y))),i(k(n(x),n(y)),n(a(x,y))))) # label("HIF5").

end_of_list.

%
% Hints extracted from previously found proofs.
%

formulas(hints).

P(k(i(n(a(x,y)),k(n(x),n(y))),i(k(n(x),n(y)),n(a(x,y))))).
P(i(x,i(y,x))).
P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))).
P(i(k(x,y),x)).
P(i(k(x,y),y)).
P(i(i(x,y),i(i(x,z),i(x,k(y,z))))).
P(i(x,a(x,y))).
P(i(x,a(y,x))).
P(i(i(x,y),i(i(z,y),i(a(x,z),y)))).
P(i(i(x,n(y)),i(y,n(x)))).
P(i(n(x),i(x,y))).
P(i(x,i(y,i(z,y)))).
P(i(i(i(x,i(y,z)),i(x,y)),i(i(x,i(y,z)),i(x,z)))).
P(i(x,i(i(y,i(z,u)),i(i(y,z),i(y,u))))).
P(i(x,i(k(y,z),y))).
P(i(i(k(x,i(y,z)),y),i(k(x,i(y,z)),z))).
P(i(x,i(k(y,z),z))).
P(i(i(x,y),i(x,k(i(z,x),y)))).
P(i(x,i(y,a(y,z)))).
P(i(x,i(y,a(z,y)))).
P(i(x,i(i(y,n(z)),i(z,n(y))))).
P(i(x,i(n(y),i(y,z)))).
P(i(i(x,y),i(x,i(z,y)))).
P(i(i(x,y),i(x,a(y,z)))).
P(i(i(x,y),i(x,a(z,y)))).
P(i(i(x,n(y)),i(x,i(y,z)))).
P(i(x,a(a(y,x),z))).
P(i(x,a(a(x,y),z))).
P(i(x,a(y,i(z,x)))).
P(i(i(x,i(y,i(z,u))),i(a(i(y,n(z)),x),i(y,i(z,u))))).
P(i(x,k(i(y,x),i(z,x)))).
P(i(i(x,i(y,n(z))),i(x,i(z,n(y))))).
P(i(i(x,i(y,i(z,u))),i(x,i(i(y,z),i(y,u))))).
P(i(k(x,i(x,y)),y)).
P(i(x,i(k(y,i(y,z)),z))).
P(i(i(x,k(y,i(y,z))),i(x,z))).
P(i(x,x)).
P(i(x,n(n(x)))).
P(i(i(x,y),i(x,k(x,y)))).
P(i(x,i(n(x),y))).
P(i(i(x,i(n(y),z)),i(a(y,x),i(n(y),z)))).
P(i(a(x,y),i(n(x),y))).
P(i(x,i(a(y,z),i(n(y),z)))).
P(i(i(x,a(y,z)),i(x,i(n(y),z)))).
P(i(x,i(n(a(x,y)),z))).
P(i(x,i(n(a(y,x)),z))).
P(i(x,i(y,n(n(a(x,z)))))).
P(i(x,i(y,i(n(a(z,x)),u)))).
P(i(i(x,y),i(x,n(n(a(x,z)))))).
P(i(i(x,y),i(n(a(x,z)),n(x)))).
P(i(n(a(x,y)),n(x))).
P(i(i(n(a(x,y)),z),i(n(a(x,y)),k(n(x),z)))).
P(i(i(x,y),i(i(z,x),i(z,y)))).
P(i(i(x,y),i(x,n(n(y))))).
P(i(x,n(n(a(y,x))))).
P(i(i(x,y),i(n(y),n(x)))).
P(i(n(a(x,y)),n(y))).
P(i(n(a(x,y)),k(n(x),n(y)))).
P(i(i(x,i(y,z)),i(x,i(n(z),n(y))))).
P(i(i(k(x,y),i(y,z)),i(k(x,y),z))).
P(i(i(k(x,y),i(x,z)),i(k(x,y),z))).
P(i(i(x,i(i(y,x),z)),i(x,z))).
P(a(x,i(y,i(i(z,i(i(u,z),w)),i(z,w))))).
P(i(x,i(i(k(y,z),i(y,u)),i(k(y,z),u)))).
P(i(i(x,y),i(k(x,z),y))).
P(i(a(i(x,n(y)),i(x,i(i(z,x),i(y,u)))),i(x,i(y,u)))).
P(i(i(i(x,y),z),i(y,z))).
P(i(x,i(y,k(y,x)))).
P(i(i(x,i(i(y,z),u)),i(x,i(z,u)))).
P(i(i(x,i(y,z)),i(y,i(x,z)))).
P(i(i(x,y),i(i(y,z),i(x,z)))).
P(i(n(x),i(a(x,y),y))).
P(i(n(x),i(n(y),n(a(x,y))))).
P(i(i(i(k(x,y),z),u),i(i(x,z),u))).
P(i(i(x,i(y,z)),i(k(x,y),z))).
P(i(k(n(x),n(y)),n(a(x,y)))).
P(i(x,k(x,i(k(n(y),n(z)),n(a(y,z)))))).
P(k(i(n(a(x,y)),k(n(x),n(y))),i(k(n(z),n(u)),n(a(z,u))))).
P(i(i(x,y),i(a(x,z),a(y,z)))).
P(i(i(x,a(y,z)),i(a(z,x),a(y,z)))).
P(i(a(x,y),a(y,x))).
P(i(i(a(x,y),z),i(a(y,x),z))).
P(i(i(i(x,a(y,z)),u),i(i(x,y),u))).
P(i(i(x,i(a(y,z),u)),i(x,i(a(z,y),u)))).
P(i(i(x,y),i(a(z,x),a(y,z)))).
P(k(i(a(k(x,y),z),k(a(x,z),a(y,z))),i(k(a(x,z),a(y,z)),a(k(x,y),z)))).
P(i(i(k(x,y),z),i(k(x,y),k(y,z)))).
P(i(i(k(x,y),z),i(k(x,y),k(x,z)))).
P(i(i(i(x,y),i(x,z)),i(i(x,y),i(x,k(y,z))))).
P(i(i(x,k(y,z)),i(x,y))).
P(i(i(x,k(y,z)),i(x,z))).
P(i(x,i(y,i(z,x)))).
P(i(k(x,k(y,z)),y)).
P(i(i(k(x,k(y,z)),u),i(k(x,k(y,z)),k(y,u)))).
P(i(k(x,k(y,z)),z)).
P(i(k(x,y),a(x,z))).
P(i(k(x,y),k(y,x))).
P(i(k(x,k(y,z)),k(x,z))).
P(i(a(x,k(y,z)),a(y,x))).
P(i(x,i(a(y,z),a(z,y)))).
P(i(i(x,a(y,z)),i(x,a(z,y)))).
P(i(k(x,k(y,i(x,z))),z)).
P(i(k(i(x,y),x),y)).
P(i(x,i(y,i(z,z)))).
P(i(x,i(y,y))).
P(i(k(i(x,y),x),k(x,y))).
P(i(i(x,y),i(x,k(y,x)))).
P(i(x,k(i(y,y),x))).
P(i(x,i(i(y,z),i(y,k(z,y))))).
P(i(i(i(x,x),y),y)).
P(i(k(x,k(y,i(x,z))),k(y,z))).
P(i(i(x,i(y,z)),i(x,i(i(u,y),i(u,z))))).
P(i(i(x,i(i(y,y),z)),i(x,z))).
P(i(i(x,k(i(y,z),y)),i(x,k(y,z)))).
P(i(i(x,k(y,z)),i(x,k(z,y)))).
P(i(i(x,i(x,y)),i(x,y))).
P(i(x,i(y,k(x,y)))).
P(i(x,i(i(y,z),i(y,k(x,z))))).
P(i(i(x,y),i(x,i(z,k(y,z))))).
P(i(i(x,y),i(x,k(i(z,i(u,i(w,w))),y)))).
P(i(x,i(i(k(y,z),i(z,u)),i(k(y,z),u)))).
P(i(a(x,k(y,z)),k(i(u,i(w,i(v5,v5))),a(y,x)))).
P(i(i(x,y),i(k(z,x),y))).
P(i(a(x,k(y,z)),k(a(y,x),i(u,i(w,w))))).
P(i(x,k(x,i(y,n(n(y)))))).
P(i(x,i(i(x,y),y))).
P(i(i(i(x,a(x,y)),z),z)).
P(i(i(x,i(i(y,a(y,z)),u)),i(x,u))).
P(i(i(i(x,k(x,y)),z),i(y,z))).
P(i(i(i(k(x,y),z),u),i(i(y,z),u))).
P(i(x,i(i(k(y,x),z),i(y,z)))).
P(i(i(k(x,y),z),i(y,i(x,z)))).
P(i(i(k(x,y),z),i(i(y,x),i(y,z)))).
P(i(i(x,a(y,z)),i(a(x,y),a(y,z)))).
P(i(i(x,i(k(x,y),z)),i(k(x,y),z))).
P(i(i(x,i(y,i(z,u))),i(x,i(k(y,z),u)))).
P(i(i(x,y),i(k(z,x),k(z,y)))).
P(i(k(x,i(y,i(z,u))),k(x,i(k(y,z),u)))).
P(i(k(x,i(y,i(i(z,a(z,u)),w))),k(x,i(y,w)))).
P(i(k(x,i(y,i(z,u))),k(x,i(z,i(y,u))))).
P(i(k(x,i(y,k(z,u))),k(x,i(y,k(u,z))))).
P(i(k(x,i(y,a(z,u))),k(x,i(y,a(u,z))))).
P(i(k(x,i(y,k(z,u))),k(x,i(y,z)))).
P(i(k(x,i(y,a(z,u))),k(x,i(a(u,y),a(z,u))))).
P(i(i(k(x,y),z),i(x,i(y,z)))).
P(i(x,i(y,a(z,k(x,y))))).
P(i(i(k(x,y),z),i(i(x,y),i(x,z)))).
P(i(x,k(x,i(y,i(z,a(u,k(y,z))))))).
P(i(i(x,i(y,a(z,u))),i(x,i(a(y,z),a(z,u))))).
P(i(k(x,i(y,i(k(y,z),u))),k(x,i(k(y,z),u)))).
P(i(i(x,k(y,i(x,z))),i(x,k(y,z)))).
P(i(i(x,y),i(x,k(y,i(z,i(u,a(w,k(z,u)))))))).
P(i(i(x,y),i(k(x,z),k(y,z)))).
P(i(k(i(a(x,y),z),u),k(i(a(y,x),z),u))).
P(i(i(x,k(y,i(z,i(u,w)))),i(x,k(y,i(k(z,u),w))))).
P(i(i(x,k(y,i(z,i(u,w)))),i(x,k(y,i(u,i(z,w)))))).
P(i(i(x,k(y,i(z,i(i(u,a(u,w)),v5)))),i(x,k(y,i(z,v5))))).
P(i(i(x,k(y,i(z,a(u,w)))),i(x,k(y,i(a(w,z),a(u,w)))))).
P(i(k(x,i(y,i(z,a(u,w)))),k(x,i(y,i(a(z,u),a(u,w)))))).
P(i(k(x,i(y,z)),k(x,i(y,k(z,i(u,i(w,a(v5,k(u,w))))))))).
P(i(k(x,i(y,k(z,i(u,i(w,v5))))),k(x,i(y,k(z,i(k(u,w),v5)))))).
P(i(k(x,i(y,k(z,i(u,i(w,v5))))),k(x,i(y,k(z,i(w,i(u,v5))))))).
P(i(a(x,k(y,z)),k(a(y,x),i(u,i(w,a(w,v5)))))).
P(i(a(x,k(y,z)),k(a(y,x),i(k(u,w),a(w,v5))))).
P(i(a(x,k(y,z)),k(a(y,x),i(a(u,k(w,v5)),a(v5,u))))).
P(i(a(x,k(y,z)),k(a(y,x),a(z,x)))).
P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,n(n(u))))).
P(i(i(x,k(y,i(z,i(u,a(w,v5))))),i(x,k(y,i(z,i(a(u,w),a(w,v5))))))).
P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(w,i(v5,a(v6,k(w,v5)))))))).
P(i(k(x,i(y,k(z,i(u,i(w,a(v5,v6)))))),k(x,i(y,k(z,i(u,i(a(w,v5),a(v5,v6)))))))).
P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(w,i(v5,a(v6,k(v5,w)))))))).
P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(w,i(a(v5,v6),a(v6,k(v5,w)))))))).
P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(a(w,v5),i(v6,a(v5,k(w,v6)))))))).
P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(a(w,v5),i(a(v6,v5),a(v5,k(w,v6)))))))).
P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(n(n(u)),i(k(a(w,v5),a(v6,v5)),a(v5,k(w,v6))))))).
P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,k(i(k(a(w,v5),a(v6,v5)),a(v5,k(w,v6))),n(n(u)))))).
P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(u,i(k(a(w,v5),a(v6,v5)),a(v5,k(w,v6)))))).
P(k(i(a(x,k(y,z)),k(a(y,x),a(z,x))),i(k(a(u,w),a(v5,w)),a(w,k(u,v5))))).
P(k(i(a(k(x,y),z),k(a(x,z),a(y,z))),i(k(a(u,w),a(v5,w)),a(w,k(u,v5))))).
P(k(i(a(k(x,y),z),k(a(x,z),a(y,z))),i(k(a(u,w),a(v5,w)),a(k(u,v5),w)))).

end_of_list.
