simple_example.p

% /home/dklbreitling/.isabelle/contrib/zipperposition-2.1-1/x86_64-linux/zipperposition --input tptp --output tptp --timeout 30.000 --mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=1 --ho-unif-max-depth=1 --ho-max-elims=0 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --boolean-reasoning=bool-hoist --bool-hoist-simpl=true --bool-select=LI --recognize-injectivity=true --ext-rules=ext-family --ext-rules-max-depth=1 --ho-choice-inst=true --ho-prim-enum=none --ho-elim-leibniz=0 --interpret-bool-funs=true --try-e="$E_HOME/eprover" --tmp-dir="$ISABELLE_TMP_PREFIX" --ho-unif-level=pragmatic-framework --select=bb+e-selection2 --post-cnf-lambda-lifting=true -q "4|prefer-sos|pnrefined(2,1,1,1,2,2,2)" -q "6|prefer-processed|conjecture-relative-struct(1.5,3.5,2,3)" -q "1|const|fifo" -q "4|prefer-ground|orient-lmax(2,1,2,1,1)" -q "4|defer-sos|conjecture-relative-struct(1,5,2,3)" --avatar=off --recognize-injectivity=true --ho-neg-ext=true --e-timeout=2 --ho-pattern-decider=true --ho-fixpoint-decider=true --e-max-derived=50 --ignore-orphans=true --e-auto=true --presaturate=true --e-call-point=0.1 /home/dklbreitling/.isabelle/prob_zipperposition_1.p
% This file was generated by Isabelle (most likely Sledgehammer)
% 2023-04-24 14:57:28.031

% Could-be-implicit typings (2)
thf(ty_n_tf__a, type,
    a : $tType).

% Explicit typings (3)
thf(f_a_type, type,
    f_a : a > a).
thf(sy_v_a, type,
    a2 : a).
thf(sy_v_b, type,
    b : a).

% Relevant facts (4)
thf(fact_0_f_a, axiom,
    ((![X : a]: ((f_a @ X) = (X)))), [], [isabelle_simp, isabelle_rank(900)]). % f_a

% Conjectures (1)
thf(conj_0, conjecture,
    ((f_a @ (f_a @ a2 )) = (a2))).