Add TPTP function composition example

Interestingly neither LEO nor Zipperp'n can solve this within 60s timeout.
However, the MMT based prover can solve this. Maybe the handwritten example is not ideally formatted, or maybe MMTs internal solver helps here.

source/casestudies/2023-cade/function-composition-dhol-example-problem.p

+tff(dhol, logic, $$dhol == []).
+thf(set, type, set: $tType).
+thf(funcAppl, type, funcAppl: !> [A:set]: !> [B:set]: !> [F:set]: !> [X:set]: set).
+thf(functionHood, axiom, ! [A:set]: ! [B:set]: ! [F:set]: ! [X:set]: ! [Y:set]: ((X = Y) => ((funcAppl @ A @ B @ F @ X) = (funcAppl @ A @ B @ F @ Y))) ).
+thf(functExt, axiom, ! [A:set]: ! [B:set]: ! [F:set]: ! [G:set]: ! [X:set]: (((funcAppl @ A @ B @ F @ X) = (funcAppl @ A @ B @ G @ X)) => (F = G))).
+thf(concat, type, concat: !> [A:set]: !> [B:set]: !> [C:set]: !> [F:set]: !> [G:set]: set).
+thf(concatAppl, axiom, ! [A:set]: ! [B:set]: ! [C:set]: ! [F:set]: ! [G:set]: ! [X:set]: (funcAppl @ A @ C @ (concat @ A @ B @ C @ F @ G) @ X) = (funcAppl @ B @ C @ F @ (funcAppl @ A @ B @ G @ X)) ).
+thf(conj,conjecture, ! [A:set]: ! [B:set]: ! [C:set]: ! [D:set]: ! [F:set]: ! [G:set]: ! [H:set]: ((concat @ A @ C @ D @ F @ (concat @ A @ B @ C @ G @ H)) = (concat @ A @ B @ D @ (concat @ B @ C @ D @ F @ G) @ H))).

source/casestudies/2023-cade/function-composition-example-translated.p

+%%% This output was generated by embedproblem, version 1.7.7 (library version 1.8).
+%%% Generated on Wed Apr 19 00:13:08 CEST 2023
+%%% using '$$dhol' embedding, version 1.0.
+%%% Logic specification used:
+%%% tff(dhol, logic, ($$dhol) == ([])).
+
+thf(set, type, set: $tType).
+thf(set_rel, type, set_rel: (set > (set > $o))).
+thf(set_rel_sym, axiom, (! [RX:set,RY:set]: ((((set_rel @ RX) @ RY) = ((set_rel @ RY) @ RX))))).
+thf(set_rel_trans, axiom, (! [RX:set,RY:set,RZ:set]: ((((set_rel @ RX) @ RY) => (((set_rel @ RY) @ RZ) => ((set_rel @ RX) @ RZ)))))).
+thf(set_rel_reduce, axiom, (! [RX:set,RY:set]: ((((set_rel @ RY) @ RY) => (((set_rel @ RX) @ RY) = (RX = RY)))))).
+thf(funcAppl, type, funcAppl: (set > (set > (set > (set > set))))).
+thf(funcAppl_tp_ax, axiom, (! [A:set,A_prime:set]: ((((set_rel @ A) @ A_prime) => (! [B:set,B_prime:set]: ((((set_rel @ B) @ B_prime) => (! [F:set,F_prime:set]: ((((set_rel @ F) @ F_prime) => (! [X:set,X_prime:set]: ((((set_rel @ X) @ X_prime) => ((set_rel @ ((((funcAppl @ A) @ B) @ F) @ X)) @ ((((funcAppl @ A) @ B) @ F) @ X))))))))))))))).
+thf(concat, type, concat: (set > (set > (set > (set > (set > set)))))).
+thf(concat_tp_ax, axiom, (! [A:set,A_prime:set]: ((((set_rel @ A) @ A_prime) => (! [B:set,B_prime:set]: ((((set_rel @ B) @ B_prime) => (! [C:set,C_prime:set]: ((((set_rel @ C) @ C_prime) => (! [F:set,F_prime:set]: ((((set_rel @ F) @ F_prime) => (! [G:set,G_prime:set]: ((((set_rel @ G) @ G_prime) => ((set_rel @ (((((concat @ A) @ B) @ C) @ F) @ G)) @ (((((concat @ A) @ B) @ C) @ F) @ G)))))))))))))))))).
+thf(functionHood, axiom, (! [A:set]: ((((set_rel @ A) @ A) => (! [B:set]: ((((set_rel @ B) @ B) => (! [F:set]: ((((set_rel @ F) @ F) => (! [X:set]: ((((set_rel @ X) @ X) => (! [Y:set]: ((((set_rel @ Y) @ Y) => (((set_rel @ X) @ Y) => ((set_rel @ ((((funcAppl @ A) @ B) @ F) @ X)) @ ((((funcAppl @ A) @ B) @ F) @ Y))))))))))))))))))).
+thf(functExt, axiom, (! [A:set]: ((((set_rel @ A) @ A) => (! [B:set]: ((((set_rel @ B) @ B) => (! [F:set]: ((((set_rel @ F) @ F) => (! [G:set]: ((((set_rel @ G) @ G) => (! [X:set]: ((((set_rel @ X) @ X) => (((set_rel @ ((((funcAppl @ A) @ B) @ F) @ X)) @ ((((funcAppl @ A) @ B) @ G) @ X)) => ((set_rel @ F) @ G)))))))))))))))))).
+thf(concatAppl, axiom, (! [A:set]: ((((set_rel @ A) @ A) => (! [B:set]: ((((set_rel @ B) @ B) => (! [C:set]: ((((set_rel @ C) @ C) => (! [F:set]: ((((set_rel @ F) @ F) => (! [G:set]: ((((set_rel @ G) @ G) => (! [X:set]: ((((set_rel @ X) @ X) => ((set_rel @ ((((funcAppl @ A) @ C) @ (((((concat @ A) @ B) @ C) @ F) @ G)) @ X)) @ ((((funcAppl @ B) @ C) @ F) @ ((((funcAppl @ A) @ B) @ G) @ X)))))))))))))))))))))).
+thf(conj, conjecture, (! [A:set]: ((((set_rel @ A) @ A) => (! [B:set]: ((((set_rel @ B) @ B) => (! [C:set]: ((((set_rel @ C) @ C) => (! [D:set]: ((((set_rel @ D) @ D) => (! [F:set]: ((((set_rel @ F) @ F) => (! [G:set]: ((((set_rel @ G) @ G) => (! [H:set]: ((((set_rel @ H) @ H) => ((set_rel @ (((((concat @ A) @ C) @ D) @ F) @ (((((concat @ A) @ B) @ C) @ G) @ H))) @ (((((concat @ A) @ B) @ D) @ (((((concat @ B) @ C) @ D) @ F) @ G)) @ H)))))))))))))))))))))))).