% COMMAND-LINE: --uf-ho
% EXPECT: % SZS status GaveUp for bound_var_bug

% TIMEFORMAT='%3R'; { time (exec 2>&1; /Users/blanchette/misc/leo --foatp e --atp e="$E_HOME"/eprover --atp epclextract="$E_HOME"/epclextract --proofoutput 1 --timeout 30 /Users/blanchette/hgs/afp_mining/tools/judgment_day_2017/data_afp/leo2-mepo/Call_Arity_SestoftGC_data/prob_308__3244432_1 ) ; }
% This file was generated by Isabelle (most likely Sledgehammer)
% 2017-07-27 17:26:12.634

% Could-be-implicit typings (91)

thf(ty_n_t__Product____Type__Oprod_It__List__Olist_It__Product____Type__Oprod_It__Vars__Ovar_Mt__Terms__Oexp_J_J_Mt__Product____Type__Oprod_It__Terms__Oexp_Mt__List__Olist_It__SestoftConf__Ostack____elem_J_J_J, type,
    produc1516857811k_elem : $tType).


thf(ty_n_t__Vars__Ovar, type,
    var : $tType).

thf(sy_c_Transitive__Closure_Ortranclp_001t__Product____Type__Oprod_It__List__Olist_It__Product____Type__Oprod_It__Vars__Ovar_Mt__Terms__Oexp_J_J_Mt__Product____Type__Oprod_It__Terms__Oexp_Mt__List__Olist_It__SestoftConf__Ostack____elem_J_J_J, type,
    transi803447880k_elem : (produc1516857811k_elem > produc1516857811k_elem > $o) > produc1516857811k_elem > produc1516857811k_elem > $o).

% Relevant facts (1094)

thf(fact_233_rtranclp__idemp, axiom,
    ((![R : produc1516857811k_elem > produc1516857811k_elem > $o]: ((transi803447880k_elem @ (transi803447880k_elem @ R)) = (transi803447880k_elem @ R))))). % rtranclp_idemp

thf(fact_293_rtranclp_Osimps, axiom,
    ((transi803447880k_elem = (^[R4 : produc1516857811k_elem > produc1516857811k_elem > $o]: (^[A12 : produc1516857811k_elem]: (^[A23 : produc1516857811k_elem]: (((?[A5 : produc1516857811k_elem]: (((A12 = A5)) & ((A23 = A5))))) | ((?[A5 : produc1516857811k_elem]: (?[B4 : produc1516857811k_elem]: (?[C5 : produc1516857811k_elem]: (((A12 = A5)) & ((((A23 = C5)) & ((((transi803447880k_elem @ R4 @ A5 @ B4)) & ((R4 @ B4 @ C5)))))))))))))))))). % rtranclp.simps