%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : ITP303_1 : TPTP v9.3.1. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:49:24 PM UTC 2026
% Result : Theorem 9.12s 2.40s
% Output : CNFRefutation 9.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : ITP303_1 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.19/0.46 % Computer : n005.cluster.edu
% 0.19/0.46 % Model : x86_64 x86_64
% 0.19/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.46 % Memory : 8046.5625MB
% 0.19/0.46 % OS : Linux 6.8.0-71-generic
% 0.19/0.46 % CPULimit : 300
% 0.19/0.46 % WCLimit : 300
% 0.19/0.46 % DateTime : Wed Sep 23 18:21:18 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.46 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.23/0.53 Running first-order theorem proving
% 0.23/0.53 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.23/0.54
% 0.23/0.54 % ======== iProver multi-core TPTP/SMT =========
% 0.23/0.54
% 0.23/0.55 % Detected problem language: tptp
% 0.23/0.56 % Proving...
% 9.12/2.39 % SZS status Started for theBenchmark.p
% 9.12/2.39 ERROR - "ProverProcess:heur/409474:1.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 9.12/2.39 Fatal error: exception Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 9.12/2.39 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref "[]" --abstr_ref_under "[]" --comb_inst_mult 3 --comb_mode clause_based --comb_res_mult 4 --comb_sup_deep_mult 2 --comb_sup_mult 0 --conj_cone_tolerance 3. --demod_completeness_check fast --demod_use_ground true --eq_ax_congr_red true --extra_neg_conj none --inst_activity_threshold 500 --inst_dismatching true --inst_eager_unprocessed_to_passive true --inst_eq_res_simp false --inst_learning_factor 2 --inst_learning_loop_flag true --inst_learning_start 3000 --inst_lit_activity_flag true --inst_lit_sel "[+prop;+sign;+ground;-num_var;-num_symb]" --inst_lit_sel_side num_symb --inst_orphan_elimination true --inst_passive_queue_type priority_queues --inst_passive_queues "[[-conj_dist;+conj_symb;-num_var];[+age;-num_symb]]" --inst_passive_queues_freq "[25;2]" --inst_prop_sim_given true --inst_prop_sim_new false --inst_restr_to_given false --inst_sel_renew solver --inst_solver_calls_frac 1. --inst_solver_per_active 1400 --inst_sos_flag false --inst_start_prop_sim_after_learn 3 --inst_subs_given false --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd true --prep_def_merge_prop_impl false --prep_def_merge_tr_cl false --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim true --prep_sem_filter exhaustive --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten true --prep_upred true --preprocessing_flag true --prolific_symb_bound 256 --prop_solver_per_cl 1024 --pure_diseq_elim true --res_backward_subs full --res_backward_subs_resolution false --res_forward_subs subset_subsumption --res_forward_subs_resolution true --res_lit_sel pos_max --res_lit_sel_side num_var --res_ordering kbo_pred --res_passive_queue_type priority_queues --res_passive_queues "[[-num_lits];[-conj_symb;-num_symb;+num_symb]]" --res_passive_queues_freq "[15;3]" --res_prop_simpl_given false --res_prop_simpl_new true --res_sim_input true --res_time_limit 202.80 --res_to_prop_solver passive --resolution_flag true --schedule none --share_sel_clauses true --smt_ac_axioms fast --smt_preprocessing true --splitting_cvd false --splitting_cvd_svl false --splitting_grd true --splitting_mode input --splitting_nvd 32 --stats_out none --sub_typing true --subs_bck_mult 8 --sup_full_bw "[]" --sup_full_fw "[]" --sup_full_triv "[PropSubs]" --sup_fun_splitting false --sup_immed_bw_immed "[]" --sup_immed_bw_main "[]" --sup_immed_fw_immed "[ACNormalisation]" --sup_immed_fw_main "[]" --sup_immed_triv "[]" --sup_indices_passive "[]" --sup_input_bw "[]" --sup_input_fw "[ACNormalisation]" --sup_input_triv "[Unflattening]" --sup_iter_deepening 2 --sup_passive_queue_type priority_queues --sup_passive_queues "[[-conj_dist;-num_symb];[+age;-num_symb];[+score;-num_symb]]" --sup_passive_queues_freq "[8;4;4]" --sup_prop_simpl_given true --sup_prop_simpl_new true --sup_restarts_mult 2 --sup_score sim_d_gen --sup_share_max_num_cl 500 --sup_share_score_frac 0.2 --sup_smt_interval 10000 --sup_symb_ordering invfreq --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.1 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode tclausify -t 0.33 --show_fool true" --time_out_real 1.00 /export/starexec/sandbox/benchmark/theBenchmark.p 1>> /export/starexec/sandbox/tmp/iprover_out_agfz4iki/hhhyv478 2>> /export/starexec/sandbox/tmp/iprover_out_agfz4iki/hhhyv478_error
% 9.12/2.39 ERROR - "ProverProcess:heur/469571:1.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 9.12/2.39 Fatal error: exception Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 9.12/2.39 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref "[]" --abstr_ref_under "[]" --comb_inst_mult 6 --comb_mode clause_based --comb_res_mult 1 --comb_sup_deep_mult 2 --comb_sup_mult 0 --conj_cone_tolerance 3.0 --demod_completeness_check fast --demod_use_ground true --eq_ax_congr_red true --extra_neg_conj none --inst_activity_threshold 32 --inst_dismatching false --inst_eager_unprocessed_to_passive false --inst_eq_res_simp false --inst_learning_factor 10 --inst_learning_loop_flag true --inst_learning_start 256 --inst_lit_activity_flag true --inst_lit_sel "[+sign;-ground;-non_prol_conj_symb;-num_var]" --inst_lit_sel_side num_lit --inst_orphan_elimination true --inst_passive_queue_type list --inst_passive_queues "[[-ground;-epr]]" --inst_passive_queues_freq "[2]" --inst_prop_sim_given false --inst_prop_sim_new false --inst_restr_to_given true --inst_sel_renew solver --inst_solver_calls_frac 0.6939020527068606 --inst_solver_per_active 8 --inst_sos_flag false --inst_start_prop_sim_after_learn 9 --inst_subs_given false --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd true --prep_def_merge_prop_impl false --prep_def_merge_tr_cl false --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim true --prep_sem_filter exhaustive --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten true --prep_upred true --preprocessing_flag true --prolific_symb_bound 2048 --prop_solver_per_cl 128 --pure_diseq_elim true --res_backward_subs full --res_backward_subs_resolution true --res_forward_subs full --res_forward_subs_resolution true --res_lit_sel adaptive --res_lit_sel_side none --res_ordering kbo --res_passive_queue_type priority_queues --res_passive_queues "[[-conj_dist;+conj_symb;-num_symb];[+age;-num_symb]]" --res_passive_queues_freq "[15;5]" --res_prop_simpl_given true --res_prop_simpl_new false --res_sim_input true --res_time_limit 300.00 --res_to_prop_solver active --resolution_flag true --schedule none --share_sel_clauses true --smt_ac_axioms fast --smt_preprocessing true --splitting_cvd false --splitting_cvd_svl false --splitting_grd true --splitting_mode input --splitting_nvd 32 --stats_out none --sub_typing true --subs_bck_mult 8 --sup_full_bw "[]" --sup_full_fw "[]" --sup_full_triv "[PropSubs]" --sup_fun_splitting false --sup_immed_bw_immed "[]" --sup_immed_bw_main "[]" --sup_immed_fw_immed "[ACNormalisation]" --sup_immed_fw_main "[]" --sup_immed_triv "[]" --sup_indices_passive "[]" --sup_input_bw "[]" --sup_input_fw "[DemodLightNormLoopTriv;ACNormalisation]" --sup_input_triv "[Unflattening]" --sup_iter_deepening 2 --sup_passive_queue_type priority_queues --sup_passive_queues "[[-conj_dist;-num_symb];[+age;-num_symb];[+score;-num_symb]]" --sup_passive_queues_freq "[8;4;4]" --sup_prop_simpl_given true --sup_prop_simpl_new true --sup_restarts_mult 2 --sup_score sim_d_gen --sup_share_max_num_cl 640 --sup_share_score_frac 0.1 --sup_smt_interval 10000 --sup_symb_ordering invfreq --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.1 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode tclausify -t 0.33 --show_fool true" --time_out_real 1.00 /export/starexec/sandbox/benchmark/theBenchmark.p 1>> /export/starexec/sandbox/tmp/iprover_out_agfz4iki/373m3x36 2>> /export/starexec/sandbox/tmp/iprover_out_agfz4iki/373m3x36_error
% 9.12/2.39 ERROR - "ProverProcess:heur/381325:1.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 9.12/2.39 Fatal error: exception Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 9.12/2.39 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref "[]" --abstr_ref_under "[]" --comb_inst_mult 3 --comb_mode clause_based --comb_res_mult 1 --comb_sup_deep_mult 1 --comb_sup_mult 3 --conj_cone_tolerance 3. --demod_completeness_check full --demod_use_ground true --eq_ax_congr_red true --extra_neg_conj none --inst_activity_threshold 500 --inst_dismatching true --inst_eager_unprocessed_to_passive true --inst_eq_res_simp false --inst_learning_factor 2 --inst_learning_loop_flag true --inst_learning_start 3000 --inst_lit_activity_flag true --inst_lit_sel "[+prop;+sign;+ground;-num_var;-num_symb]" --inst_lit_sel_side num_symb --inst_orphan_elimination true --inst_passive_queue_type priority_queues --inst_passive_queues "[[-conj_dist;+conj_symb;-num_var];[+age;-num_symb]]" --inst_passive_queues_freq "[25;2]" --inst_prop_sim_given true --inst_prop_sim_new false --inst_restr_to_given false --inst_sel_renew solver --inst_solver_calls_frac 1. --inst_solver_per_active 1400 --inst_sos_flag false --inst_start_prop_sim_after_learn 3 --inst_subs_given false --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd true --prep_def_merge_prop_impl false --prep_def_merge_tr_cl false --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim true --prep_sem_filter exhaustive --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten true --prep_upred true --preprocessing_flag true --prolific_symb_bound 256 --prop_solver_per_cl 1024 --pure_diseq_elim true --res_backward_subs full --res_backward_subs_resolution true --res_forward_subs full --res_forward_subs_resolution true --res_lit_sel adaptive --res_lit_sel_side none --res_ordering kbo --res_passive_queue_type priority_queues --res_passive_queues "[[-conj_dist;+conj_symb;-num_symb];[+age;-num_symb]]" --res_passive_queues_freq "[15;5]" --res_prop_simpl_given true --res_prop_simpl_new false --res_sim_input true --res_time_limit 300.00 --res_to_prop_solver active --resolution_flag true --schedule none --share_sel_clauses true --smt_ac_axioms fast --smt_preprocessing true --splitting_cvd false --splitting_cvd_svl false --splitting_grd true --splitting_mode input --splitting_nvd 32 --stats_out none --sub_typing true --subs_bck_mult 8 --sup_full_bw "[]" --sup_full_fw "[Demod;DemodLoopTriv;LightNorm;ACNormalisation]" --sup_full_triv "[]" --sup_fun_splitting true --sup_immed_bw_immed "[]" --sup_immed_bw_main "[SubsumptionRes;UnitSubsAndRes]" --sup_immed_fw_immed "[Subsumption;UnitSubsAndRes;Demod;DemodLoopTriv;LightNorm;DemodLightNormLoopTriv]" --sup_immed_fw_main "[Subsumption;SubsumptionRes;LightNorm;DemodLightNormLoopTriv]" --sup_immed_triv "[PropSubs]" --sup_indices_passive "[UnitSubsumption;NonunitSubsumption;FwDemod]" --sup_input_bw "[UnitSubsAndRes]" --sup_input_fw "[]" --sup_input_triv "[PropSubs]" --sup_iter_deepening 0 --sup_passive_queue_type priority_queues --sup_passive_queues "[[-conj_symb;-max_atom_input_occur];[+horn];[+bc_imp_inh;+ground;-conj_dist]]" --sup_passive_queues_freq "[3;1;25]" --sup_prop_simpl_given true --sup_prop_simpl_new false --sup_restarts_mult 8 --sup_score sim_d_gen --sup_share_max_num_cl 40 --sup_share_score_frac 0.1 --sup_smt_interval 10000 --sup_symb_ordering arity_random --sup_to_prop_solver active --superposition_flag true --time_out_prep_mult 0.1 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode tclausify -t 0.33 --show_fool true" --time_out_real 1.00 /export/starexec/sandbox/benchmark/theBenchmark.p 1>> /export/starexec/sandbox/tmp/iprover_out_agfz4iki/ro462b6n 2>> /export/starexec/sandbox/tmp/iprover_out_agfz4iki/ro462b6n_error
% 9.12/2.39 ERROR - "ProverProcess:heur/346297:1.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 9.12/2.39 Fatal error: exception Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 9.12/2.39 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref_under "[]" --comb_inst_mult 3 --comb_mode time_based --comb_sup_deep_mult 6 --comb_sup_mult 32 --conj_cone_tolerance 2.7380125131254 --demod_completeness_check full --demod_use_ground true --eq_ax_congr_red false --extra_neg_conj none --inst_activity_threshold 16 --inst_dismatching false --inst_eager_unprocessed_to_passive false --inst_eq_res_simp true --inst_learning_factor 6 --inst_learning_loop_flag true --inst_learning_start 1024 --inst_lit_activity_flag true --inst_lit_sel "[+depth;+sign;+num_symb;-split;-eq]" --inst_lit_sel_side cnt --inst_orphan_elimination true --inst_passive_queue_type list --inst_passive_queues "[[-num_lits];[-max_atom_input_occur;-ground]]" --inst_passive_queues_freq "[8;50]" --inst_prop_sim_given false --inst_prop_sim_new false --inst_restr_to_given false --inst_sel_renew solver --inst_solver_calls_frac 0.21724605765256222 --inst_solver_per_active 256 --inst_sos_flag true --inst_sos_phase true --inst_sos_sth_lit_sel "[-depth;+non_prol_conj_symb;-split;-ground;+num_var]" --inst_start_prop_sim_after_learn 8 --inst_subs_given false --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd false --prep_def_merge_prop_impl true --prep_def_merge_tr_cl true --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim false --prep_sem_filter none --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten false --prep_upred true --preprocessing_flag true --prolific_symb_bound 2048 --prop_solver_per_cl 32 --pure_diseq_elim false --resolution_flag false --schedule none --share_sel_clauses false --smt_ac_axioms full --smt_preprocessing true --splitting_cvd true --splitting_cvd_svl false --splitting_grd true --splitting_mode full --splitting_nvd 128 --stats_out none --sub_typing true --subs_bck_mult 0 --sup_full_bw "[Demod]" --sup_full_fw "[Subsumption;SubsumptionRes;UnitSubsAndRes;DemodLoopTriv;DemodLightNormLoopTriv;ACJoinability;ACNormalisation]" --sup_full_triv "[PropSubs;Unflattening]" --sup_fun_splitting false --sup_immed_bw_immed "[]" --sup_immed_bw_main "[]" --sup_immed_fw_immed "[Subsumption;SubsumptionRes;UnitSubsAndRes;Demod;ACJoinability]" --sup_immed_fw_main "[SubsumptionRes;DemodLoopTriv;DemodLightNormLoopTriv;ACJoinability;ACNormalisation]" --sup_immed_triv "[]" --sup_indices_passive "[UnitSubsumption;NonunitSubsumption;Subsumption;FwDemod;BwDemod;LightNorm]" --sup_input_bw "[]" --sup_input_fw "[]" --sup_input_triv "[PropSubs;Unflattening]" --sup_iter_deepening 4 --sup_passive_queue_type queue --sup_passive_queues "[[+num_symb]]" --sup_passive_queues_freq "[5]" --sup_prop_simpl_given true --sup_prop_simpl_new false --sup_restarts_mult 4 --sup_smt_interval 10000 --sup_symb_ordering arity_random --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.4432297345384799 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode tclausify -t 0.33 --show_fool true" --time_out_real 1.00 /export/starexec/sandbox/benchmark/theBenchmark.p 1>> /export/starexec/sandbox/tmp/iprover_out_agfz4iki/1l3qynqe 2>> /export/starexec/sandbox/tmp/iprover_out_agfz4iki/1l3qynqe_error
% 9.12/2.40 ERROR - "ProverProcess:heur/397442:1.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 9.12/2.40 Fatal error: exception Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 9.12/2.40 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref "[]" --abstr_ref_under "[]" --comb_inst_mult 64 --comb_mode clause_based --comb_res_mult 1 --comb_sup_deep_mult 2 --comb_sup_mult 0 --conj_cone_tolerance 3. --demod_completeness_check fast --demod_use_ground true --eq_ax_congr_red true --extra_neg_conj none --inst_activity_threshold 4 --inst_dismatching true --inst_eager_unprocessed_to_passive true --inst_eq_res_simp true --inst_learning_factor 8 --inst_learning_loop_flag true --inst_learning_start 2 --inst_lit_activity_flag false --inst_lit_sel "[-split]" --inst_lit_sel_side num_lit --inst_orphan_elimination false --inst_passive_queue_type priority_queues --inst_passive_queues "[[+conj_symb]]" --inst_passive_queues_freq "[50]" --inst_prop_sim_given true --inst_prop_sim_new false --inst_restr_to_given false --inst_sel_renew solver --inst_solver_calls_frac 0.8199321230744955 --inst_solver_per_active 4 --inst_sos_flag false --inst_start_prop_sim_after_learn 7 --inst_subs_given false --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd true --prep_def_merge_prop_impl false --prep_def_merge_tr_cl false --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim true --prep_sem_filter exhaustive --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten true --prep_upred true --preprocessing_flag true --prolific_symb_bound 256 --prop_solver_per_cl 1024 --pure_diseq_elim true --res_backward_subs full --res_backward_subs_resolution true --res_forward_subs full --res_forward_subs_resolution true --res_lit_sel adaptive --res_lit_sel_side none --res_ordering kbo --res_passive_queue_type priority_queues --res_passive_queues "[[-conj_dist;+conj_symb;-num_symb];[+age;-num_symb]]" --res_passive_queues_freq "[15;5]" --res_prop_simpl_given true --res_prop_simpl_new false --res_sim_input true --res_time_limit 300.00 --res_to_prop_solver active --resolution_flag true --schedule none --share_sel_clauses true --smt_ac_axioms fast --smt_preprocessing true --splitting_cvd false --splitting_cvd_svl false --splitting_grd true --splitting_mode input --splitting_nvd 32 --stats_out none --sub_typing true --subs_bck_mult 8 --sup_full_bw "[]" --sup_full_fw "[]" --sup_full_triv "[PropSubs]" --sup_fun_splitting false --sup_immed_bw_immed "[]" --sup_immed_bw_main "[]" --sup_immed_fw_immed "[ACNormalisation]" --sup_immed_fw_main "[]" --sup_immed_triv "[]" --sup_indices_passive "[]" --sup_input_bw "[]" --sup_input_fw "[ACNormalisation]" --sup_input_triv "[Unflattening]" --sup_iter_deepening 2 --sup_passive_queue_type priority_queues --sup_passive_queues "[[-conj_dist;-num_symb];[+age;-num_symb];[+score;-num_symb]]" --sup_passive_queues_freq "[8;4;4]" --sup_prop_simpl_given true --sup_prop_simpl_new true --sup_restarts_mult 2 --sup_score sim_d_gen --sup_share_max_num_cl 500 --sup_share_score_frac 0.2 --sup_smt_interval 10000 --sup_symb_ordering invfreq --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.1 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode tclausify -t 0.33 --show_fool true" --time_out_real 1.00 /export/starexec/sandbox/benchmark/theBenchmark.p 1>> /export/starexec/sandbox/tmp/iprover_out_agfz4iki/m1f64p9w 2>> /export/starexec/sandbox/tmp/iprover_out_agfz4iki/m1f64p9w_error
% 9.12/2.40 % SZS status Theorem for theBenchmark.p
% 9.12/2.40
% 9.12/2.40 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 9.12/2.40
% 9.12/2.40 % ------ iProver source info
% 9.12/2.40
% 9.12/2.40 % git: date: 2026-07-19 20:42:38 +0200
% 9.12/2.40 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 9.12/2.40 % git: non_committed_changes: false
% 9.12/2.40
% 9.12/2.40 % ------ Parsing...
% 9.12/2.40 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 9.12/2.40 %
% 9.12/2.40
% 9.12/2.40 % ------ Preprocessing... sup_sim: 1 pe_s pe:1:0s pe_e sup_sim: 0 pe_s pe_e %
% 9.12/2.40
% 9.12/2.40 % ------ Preprocessing...% ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 9.12/2.40 gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e % ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 9.12/2.40 %
% 9.12/2.40
% 9.12/2.40 % ------ Preprocessing...
% 9.12/2.40 % ------ Proving...
% 9.12/2.40 % ------ Problem Properties
% 9.12/2.40
% 9.12/2.40 %
% 9.12/2.40 % clauses 144
% 9.12/2.40 % conjectures 1
% 9.12/2.40 % EPR 6
% 9.12/2.40 % Horn 132
% 9.12/2.40 % unary 24
% 9.12/2.40 % binary 53
% 9.12/2.40 % lits 398
% 9.12/2.40 % lits eq 115
% 9.12/2.40 % fd_pure 0
% 9.12/2.40 % fd_pseudo 0
% 9.12/2.40 % fd_cond 0
% 9.12/2.40 % fd_pseudo_cond 15
% 9.12/2.40 % AC symbols 0
% 9.12/2.40
% 9.12/2.40 % ------ Schedule dynamic 5 is on
% 9.12/2.40
% 9.12/2.40 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 9.12/2.40
% 9.12/2.40
% 9.12/2.40 % ------
% 9.12/2.40 % Current options:
% 9.12/2.40 % ------
% 9.12/2.40
% 9.12/2.40
% 9.12/2.40 %
% 9.12/2.40
% 9.12/2.40 % ------ Proving...
% 9.12/2.40 %
% 9.12/2.40
% 9.12/2.40 % SZS status Theorem for theBenchmark.p
% 9.12/2.40
% 9.12/2.40 % SZS output start CNFRefutation for theBenchmark.p
% 9.12/2.40
% 9.12/2.40 tff(func_def_0, type, 'functorComp$a': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.12/2.40 tff(pred_def_1, type, 'member$j': ('ZF_ZF_fun$' * 'ZF_ZF_fun_set$') > $o).
% 9.12/2.40 tff(pred_def_2, type, 'member$n': ('B_b_prod_b_fun$' * 'B_b_prod_b_fun_set$') > $o).
% 9.12/2.40 tff(pred_def_3, type, 'fun_app$e': ('B_ZF_fun_bool_fun$' * 'B_ZF_fun$') > $o).
% 9.12/2.40 tff(pred_def_4, type, 'extCategory$': 'A_b_b_c_LSCategory_ext_Category_ext$' > $o).
% 9.12/2.40 tff(pred_def_5, type, 'functor_comp_def$c': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$') > $o).
% 9.12/2.40 tff(pred_def_6, type, 'lSCategory$': 'A_b_b_c_LSCategory_ext_Category_ext$' > $o).
% 9.12/2.40 tff(pred_def_7, type, 'fun_app$a': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$') > $o).
% 9.12/2.40 tff(pred_def_8, type, 'member$f': ('A_ZF_fun$' * 'A_ZF_fun_set$') > $o).
% 9.12/2.40 tff(pred_def_9, type, 'functor_comp_def$b': ('ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$') > $o).
% 9.12/2.40 tff(pred_def_10, type, 'natTransP$f': 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > $o).
% 9.12/2.40 tff(pred_def_11, type, 'fun_app$q': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$') > $o).
% 9.12/2.40 tff(pred_def_12, type, 'fun_app$b': ('ZF_ZF_prod_bool_fun$' * 'ZF_ZF_prod$') > $o).
% 9.12/2.40 tff(pred_def_13, type, 'category$a': 'ZF_ZF_unit_Category_ext$' > $o).
% 9.12/2.40 tff(pred_def_14, type, 'functor_comp_def$a': ('ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' * 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$') > $o).
% 9.12/2.40 tff(pred_def_15, type, 'category$b': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' > $o).
% 9.12/2.40 tff(pred_def_16, type, 'functorM_axioms$': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > $o).
% 9.12/2.40 tff(pred_def_17, type, 'functorExt$': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > $o).
% 9.12/2.40 tff(pred_def_18, type, 'category$': 'A_b_b_c_LSCategory_ext_Category_ext$' > $o).
% 9.12/2.40 tff(pred_def_19, type, 'nTCompDefined$': ('ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$') > $o).
% 9.12/2.40 tff(pred_def_20, type, 'equivalence$': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > $o).
% 9.12/2.40 tff(pred_def_21, type, 'member$m': ('ZF_ZF_prod_ZF_fun$' * 'ZF_ZF_prod_ZF_fun_set$') > $o).
% 9.12/2.40 tff(pred_def_22, type, 'natTrans$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > $o).
% 9.12/2.40 tff(pred_def_23, type, 'fun_app$d': ('ZF_bool_fun$' * 'ZF$') > $o).
% 9.12/2.40 tff(pred_def_24, type, 'natTransP$e': 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$' > $o).
% 9.12/2.40 tff(pred_def_25, type, 'nTCompDefined$b': ('ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' * 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$') > $o).
% 9.12/2.40 tff(pred_def_26, type, 'member$c': ('ZF$' * 'ZF_set$') > $o).
% 9.12/2.40 tff(pred_def_27, type, 'member$g': ('A_b_fun$' * 'A_b_fun_set$') > $o).
% 9.12/2.40 tff(pred_def_28, type, 'compDefined$c': ('Unit_unit_unit_Category_ext$' * 'Unit$' * 'Unit$') > $o).
% 9.12/2.40 tff(pred_def_29, type, 'natTransP$b': 'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$' > $o).
% 9.12/2.40 tff(pred_def_30, type, 'functor_comp_def$': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$') > $o).
% 9.12/2.40 tff(pred_def_31, type, 'functor$d': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' > $o).
% 9.12/2.40 tff(pred_def_32, type, 'functor$f': 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > $o).
% 9.12/2.40 tff(pred_def_33, type, 'category_axioms$b': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' > $o).
% 9.12/2.40 tff(pred_def_34, type, 'lSCategory_axioms$': 'A_b_b_c_LSCategory_ext_Category_ext$' > $o).
% 9.12/2.40 tff(pred_def_35, type, 'member$e': ('B_a_fun$' * 'B_a_fun_set$') > $o).
% 9.12/2.40 tff(pred_def_36, type, 'nTCompDefined$e': ('A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' * 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$') > $o).
% 9.12/2.40 tff(pred_def_37, type, 'fun_app$c': ('B_b_prod_bool_fun$' * 'B_b_prod$') > $o).
% 9.12/2.40 tff(pred_def_38, type, 'natTrans$e': 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$' > $o).
% 9.12/2.40 tff(pred_def_39, type, 'functor_abbrev$b': ('ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' * 'ZF_ZF_unit_Category_ext$' * 'ZF_ZF_unit_Category_ext$') > $o).
% 9.12/2.40 tff(pred_def_40, type, 'nt_abbrev$b': ('ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' * 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' * 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$') > $o).
% 9.12/2.40 tff(pred_def_41, type, 'fun_app$g': ('A_ZF_fun_bool_fun$' * 'A_ZF_fun$') > $o).
% 9.12/2.40 tff(pred_def_42, type, 'extCategory$a': 'ZF_ZF_unit_Category_ext$' > $o).
% 9.12/2.40 tff(pred_def_43, type, 'category_axioms$': 'A_b_b_c_LSCategory_ext_Category_ext$' > $o).
% 9.12/2.40 tff(pred_def_44, type, 'functor_abbrev$': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A_b_b_c_LSCategory_ext_Category_ext$' * 'ZF_ZF_unit_Category_ext$') > $o).
% 9.12/2.40 tff(pred_def_45, type, 'natTransExt$': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > $o).
% 9.12/2.40 tff(pred_def_46, type, 'functorM$': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > $o).
% 9.12/2.40 tff(pred_def_47, type, 'natTransP$d': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > $o).
% 9.12/2.40 tff(pred_def_48, type, 'natTrans$b': 'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$' > $o).
% 9.12/2.40 tff(pred_def_49, type, 'mapsTo$c': ('Unit_unit_unit_Category_ext$' * 'Unit$' * 'Unit$' * 'Unit$') > $o).
% 9.12/2.40 tff(pred_def_50, type, 'natTrans$c': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > $o).
% 9.12/2.40 tff(pred_def_51, type, 'fun_app$j': ('A_bool_fun$' * 'A$') > $o).
% 9.12/2.40 tff(pred_def_52, type, 'functor$b': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > $o).
% 9.12/2.40 tff(pred_def_53, type, 'compDefined$b': ('ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$') > $o).
% 9.12/2.40 tff(pred_def_54, type, 'functor_abbrev$a': ('ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$' * 'ZF_ZF_unit_Category_ext$' * 'Unit_unit_unit_Category_ext$') > $o).
% 9.12/2.40 tff(pred_def_55, type, 'functor$e': 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' > $o).
% 9.12/2.40 tff(pred_def_56, type, 'natTrans$d': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > $o).
% 9.12/2.40 tff(pred_def_57, type, 'member$h': ('B$' * 'B_set$') > $o).
% 9.12/2.40 tff(pred_def_58, type, 'member$a': ('ZF_ZF_prod$' * 'ZF_ZF_prod_set$') > $o).
% 9.12/2.40 tff(pred_def_59, type, 'member$i': ('A$' * 'A_set$') > $o).
% 9.12/2.40 tff(pred_def_60, type, 'natTrans$f': 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > $o).
% 9.12/2.40 tff(pred_def_61, type, 'nTCompDefined$c': ('ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$' * 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$') > $o).
% 9.12/2.40 tff(pred_def_62, type, 'natTransP$c': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > $o).
% 9.12/2.40 tff(pred_def_63, type, 'nTCompDefined$d': ('A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' * 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$') > $o).
% 9.12/2.40 tff(pred_def_64, type, 'fun_app$f': ('B_a_fun_bool_fun$' * 'B_a_fun$') > $o).
% 9.12/2.40 tff(pred_def_65, type, 'category_axioms$a': 'ZF_ZF_unit_Category_ext$' > $o).
% 9.12/2.40 tff(pred_def_66, type, 'nt_abbrev$c': ('A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' * 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' * 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$') > $o).
% 9.12/2.40 tff(pred_def_67, type, 'preFunctor$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > $o).
% 9.12/2.40 tff(pred_def_68, type, 'member$b': ('B_b_prod$' * 'B_b_prod_set$') > $o).
% 9.12/2.40 tff(pred_def_69, type, 'fun_app$i': ('B_bool_fun$' * 'B$') > $o).
% 9.12/2.40 tff(pred_def_70, type, 'member$': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$') > $o).
% 9.12/2.40 tff(pred_def_71, type, 'mapsTo$b': ('ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$') > $o).
% 9.12/2.40 tff(pred_def_72, type, 'fun_app$h': ('A_b_fun_bool_fun$' * 'A_b_fun$') > $o).
% 9.12/2.40 tff(pred_def_73, type, 'member$k': ('Unit$' * 'Unit_set$') > $o).
% 9.12/2.40 tff(pred_def_74, type, 'natTransP$': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > $o).
% 9.12/2.40 tff(pred_def_75, type, 'nt_abbrev$': ('ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$') > $o).
% 9.12/2.40 tff(pred_def_76, type, 'member$d': ('B_ZF_fun$' * 'B_ZF_fun_set$') > $o).
% 9.12/2.40 tff(pred_def_77, type, 'functor$a': 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$' > $o).
% 9.12/2.40 tff(pred_def_78, type, 'functor$c': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' > $o).
% 9.12/2.40 tff(pred_def_79, type, 'member$l': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$') > $o).
% 9.12/2.40 tff(pred_def_80, type, 'member$o': ('ZF_set$' * 'ZF_set_set$') > $o).
% 9.12/2.40 tff(pred_def_81, type, sP0: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > $o).
% 9.12/2.40 tff(func_def_82, type, 'uuy$': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_prod_bool_fun$').
% 9.12/2.40 tff(func_def_83, type, 'natTransComp$': ('ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$') > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_84, type, 'fun_app$l': ('B_b_fun$' * 'B$') > 'B$').
% 9.12/2.40 tff(func_def_85, type, 'mor2ZF$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_ZF_fun$').
% 9.12/2.40 tff(func_def_86, type, 'idNatTrans$b': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_87, type, 'natTransMap$c': ('ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$' * 'ZF$') > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_88, type, 'catDom$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A_b_b_c_LSCategory_ext_Category_ext$').
% 9.12/2.40 tff(func_def_89, type, 'zFfun$': ('ZF$' * 'ZF$' * 'ZF_ZF_fun$') > 'ZF$').
% 9.12/2.40 tff(func_def_90, type, 'catDom_update$': 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$').
% 9.12/2.40 tff(func_def_91, type, 'inverse_rel$': ('ZF_ZF_unit_Category_ext$' * 'ZF$') > 'ZF_bool_fun$').
% 9.12/2.40 tff(func_def_92, type, 'extensional$b': 'B_set$' > 'B_ZF_fun_set$').
% 9.12/2.40 tff(func_def_93, type, 'fun_app$p': ('A_b_fun$' * 'A$') > 'B$').
% 9.12/2.40 tff(func_def_94, type, 'idNatTrans$': 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$' > 'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_95, type, 'idNatTrans$c': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_96, type, 'more$a': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'Unit$').
% 9.12/2.40 tff(func_def_97, type, 'more$': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > 'Unit$').
% 9.12/2.40 tff(func_def_98, type, 'nTCatCod$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'ZF_ZF_unit_Category_ext$').
% 9.12/2.40 tff(func_def_99, type, 'nTCod$f': 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_100, type, 'mapM$e': ('ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' * 'ZF$') > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_101, type, 'nTCatCod$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > 'ZF_ZF_unit_Category_ext$').
% 9.12/2.40 tff(func_def_102, type, 'fun_app$ac': ('ZF_ZF_fun_ZF_ZF_fun_fun$' * 'ZF_ZF_fun$') > 'ZF_ZF_fun$').
% 9.12/2.40 tff(func_def_103, type, 'natTransMap$e': ('A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' * 'A$') > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_104, type, 'zFfunCod$': 'ZF_ZF_fun$').
% 9.12/2.40 tff(func_def_105, type, 'natTransMap$b': ('ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' * 'ZF$') > 'B$').
% 9.12/2.40 tff(func_def_106, type, 'fun_app$k': ('ZF_ZF_ZF_fun_fun$' * 'ZF$') > 'ZF_ZF_fun$').
% 9.12/2.40 tff(func_def_107, type, 'homFtor$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'A$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_108, type, 'category_ext$': ('A_set$' * 'B_set$' * 'B_a_fun$' * 'B_a_fun$' * 'A_b_fun$' * 'B_b_b_fun_fun$' * 'B_c_LSCategory_ext$') > 'A_b_b_c_LSCategory_ext_Category_ext$').
% 9.12/2.40 tff(func_def_109, type, 'catDom$b': 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$' > 'ZF_ZF_unit_Category_ext$').
% 9.12/2.40 tff(func_def_110, type, 'nTDom$e': 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$' > 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_111, type, 'nTDom$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$').
% 9.12/2.40 tff(func_def_112, type, 'more$e': 'ZF_ZF_unit_Category_ext$' > 'Unit$').
% 9.12/2.40 tff(func_def_113, type, 'catDom$f': 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A_b_b_c_LSCategory_ext_Category_ext$').
% 9.12/2.40 tff(func_def_114, type, 'set$a': 'ZF_ZF_unit_Category_ext$').
% 9.12/2.40 tff(func_def_115, type, 'idNatTrans$e': 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$' > 'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_116, type, 'nTDom$c': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_117, type, 'compDefined$': ('ZF_ZF_unit_Category_ext$' * 'ZF$') > 'ZF_bool_fun$').
% 9.12/2.40 tff(func_def_118, type, 'makeCat$c': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$').
% 9.12/2.40 tff(func_def_119, type, 'extensional$f': 'B_b_prod_set$' > 'B_b_prod_b_fun_set$').
% 9.12/2.40 tff(func_def_120, type, 'restrict$d': ('B_a_fun$' * 'B_set$') > 'B_a_fun$').
% 9.12/2.40 tff(func_def_121, type, 'mapM$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'B_ZF_fun$').
% 9.12/2.40 tff(func_def_122, type, 'collect$d': 'A_bool_fun$' > 'A_set$').
% 9.12/2.40 tff(func_def_123, type, 'equivalence$a': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$').
% 9.12/2.40 tff(func_def_124, type, 'natTrans_ext$': ('ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' * 'ZF_ZF_fun$' * 'Unit$') > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_125, type, 'catExp$a': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'ZF_ZF_unit_Category_ext$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$').
% 9.12/2.40 tff(func_def_126, type, 'dom$b': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_127, type, 'fun_app$m': ('B_b_b_fun_fun$' * 'B$') > 'B_b_fun$').
% 9.12/2.40 tff(func_def_128, type, 'nTCod_update$a': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_129, type, 'catCod$c': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' > 'A_b_b_c_LSCategory_ext_Category_ext$').
% 9.12/2.40 tff(func_def_130, type, 'restrict$f': ('ZF_ZF_fun$' * 'ZF_set$') > 'ZF_ZF_fun$').
% 9.12/2.40 tff(func_def_131, type, 'natTransMap$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A_ZF_fun$').
% 9.12/2.40 tff(func_def_132, type, 'natTransMap$f': ('ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$' * 'ZF$') > 'Unit$').
% 9.12/2.40 tff(func_def_133, type, 'oppositeCategory$a': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$').
% 9.12/2.40 tff(func_def_134, type, 'functor_ext$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'ZF_ZF_unit_Category_ext$' * 'B_ZF_fun$' * 'Unit$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_135, type, 'homFtorContra$a': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'A$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_136, type, 'homFtorContra$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'A$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_137, type, 'nTCod$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_138, type, 'extensional$e': 'A_set$' > 'A_b_fun_set$').
% 9.12/2.40 tff(func_def_139, type, 'collect$b': 'B_bool_fun$' > 'B_set$').
% 9.12/2.40 tff(func_def_140, type, 'cod$b': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_141, type, 'zFfunComp$': 'ZF_ZF_ZF_fun_fun$').
% 9.12/2.40 tff(func_def_142, type, 'compDefined$a': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'B$') > 'B_bool_fun$').
% 9.12/2.40 tff(func_def_143, type, 'inverse_rel$a': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'B$') > 'B_bool_fun$').
% 9.12/2.40 tff(func_def_144, type, 'the$': 'ZF_bool_fun$' > 'ZF$').
% 9.12/2.40 tff(func_def_145, type, 'nTCatDom$c': 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$' > 'ZF_ZF_unit_Category_ext$').
% 9.12/2.40 tff(func_def_146, type, 'catCod$e': 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$').
% 9.12/2.40 tff(func_def_147, type, 'catCod$b': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > 'ZF_ZF_unit_Category_ext$').
% 9.12/2.40 tff(func_def_148, type, 'constFunctor$a': ('ZF_ZF_unit_Category_ext$' * 'ZF_ZF_unit_Category_ext$' * 'ZF$') > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_149, type, 'uuf$': 'A_b_fun_set$' > 'A_b_fun_bool_fun$').
% 9.12/2.40 tff(func_def_150, type, 'nTDom_update$': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_151, type, 'catCod$f': 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$').
% 9.12/2.40 tff(func_def_152, type, 'objIso$': ('ZF_ZF_unit_Category_ext$' * 'ZF$') > 'ZF_bool_fun$').
% 9.12/2.40 tff(func_def_153, type, 'oppositeCategory$c': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$').
% 9.12/2.40 tff(func_def_154, type, 'cod_update$': 'ZF_ZF_fun_ZF_ZF_fun_fun$' > 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$').
% 9.12/2.40 tff(func_def_155, type, 'lSCategory_ext$': ('B_ZF_fun$' * 'C$') > 'B_c_LSCategory_ext$').
% 9.12/2.40 tff(func_def_156, type, 'identityFunctor$a': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_157, type, 'collect$h': 'A_b_fun_bool_fun$' > 'A_b_fun_set$').
% 9.12/2.40 tff(func_def_158, type, 'natTransComp$b': ('ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$') > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_159, type, 'comp$b': ('ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$') > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_160, type, 'functor$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$').
% 9.12/2.40 tff(func_def_161, type, 'mor_update$': 'ZF_set_ZF_set_fun$' > 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$').
% 9.12/2.40 tff(func_def_162, type, 'catCod$a': 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$' > 'Unit_unit_unit_Category_ext$').
% 9.12/2.40 tff(func_def_163, type, 'natTransMap$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > 'ZF_ZF_fun$').
% 9.12/2.40 tff(func_def_164, type, 'cod$a': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_a_fun$').
% 9.12/2.40 tff(func_def_165, type, 'makeFtor$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$').
% 9.12/2.40 tff(func_def_166, type, 'functor_ext$a': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' * 'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' * 'Unit$') > 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_167, type, 'natTransExt$a': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$').
% 9.12/2.40 tff(func_def_168, type, 'nTCatCod$e': 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$').
% 9.12/2.40 tff(func_def_169, type, 'fun_app$w': ('ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$' * 'ZF_ZF_unit_Category_ext$') > 'ZF_ZF_unit_Category_ext$').
% 9.12/2.40 tff(func_def_170, type, 'mapO$': ('ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' * 'ZF$') > 'A$').
% 9.12/2.40 tff(func_def_171, type, 'nTDom$b': 'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$' > 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_172, type, 'nTCod$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$').
% 9.12/2.40 tff(func_def_173, type, 'uul$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'A$') > 'B_ZF_fun$').
% 9.12/2.40 tff(func_def_174, type, 'identityFunctor$': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_175, type, 'restrict$e': ('A_b_fun$' * 'A_set$') > 'A_b_fun$').
% 9.12/2.40 tff(func_def_176, type, 'category_ext$a': ('ZF_set$' * 'ZF_set$' * 'ZF_ZF_fun$' * 'ZF_ZF_fun$' * 'ZF_ZF_fun$' * 'ZF_ZF_ZF_fun_fun$' * 'Unit$') > 'ZF_ZF_unit_Category_ext$').
% 9.12/2.40 tff(func_def_177, type, 'constFunctor$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'ZF_ZF_unit_Category_ext$' * 'ZF$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_178, type, 'homFtorMap$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'A$') > 'B_ZF_fun$').
% 9.12/2.40 tff(func_def_179, type, 'collect$f': 'B_a_fun_bool_fun$' > 'B_a_fun_set$').
% 9.12/2.40 tff(func_def_180, type, 'makeNT$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_181, type, 'inverse$': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_fun$').
% 9.12/2.40 tff(func_def_182, type, 'uuv$': 'ZF_ZF_fun$').
% 9.12/2.40 tff(func_def_183, type, 'restrict$': ('ZF_ZF_prod_ZF_fun$' * 'ZF_ZF_prod_set$' * 'ZF_ZF_prod$') > 'ZF$').
% 9.12/2.40 tff(func_def_184, type, 'fun_app$t': ('B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' * 'B$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_185, type, 'extensional$a': 'A_set$' > 'A_ZF_fun_set$').
% 9.12/2.40 tff(func_def_186, type, 'functorExt$a': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$').
% 9.12/2.40 tff(func_def_187, type, 'nTCatDom$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > 'ZF_ZF_unit_Category_ext$').
% 9.12/2.40 tff(func_def_188, type, 'zF2mor$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'ZF$') > 'B$').
% 9.12/2.40 tff(func_def_189, type, 'fun_app$x': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_190, type, 'collect$j': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$').
% 9.12/2.40 tff(func_def_191, type, 'uub$': 'A_set$' > 'A_bool_fun$').
% 9.12/2.40 tff(func_def_192, type, 'fun_app$af': ('ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$' * 'ZF_ZF_ZF_fun_fun$') > 'ZF_ZF_ZF_fun_fun$').
% 9.12/2.40 tff(func_def_193, type, 'uux$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_b_b_fun_fun$').
% 9.12/2.40 tff(func_def_194, type, 'uui$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$').
% 9.12/2.40 tff(func_def_195, type, 'category_ext$b': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$' * 'Unit$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$').
% 9.12/2.40 tff(func_def_196, type, 'dom$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_a_fun$').
% 9.12/2.40 tff(func_def_197, type, 'more$d': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_c_LSCategory_ext$').
% 9.12/2.40 tff(func_def_198, type, 'zFfunDom$': 'ZF_ZF_fun$').
% 9.12/2.40 tff(func_def_199, type, 'natTransP$a': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$').
% 9.12/2.40 tff(func_def_200, type, 'zFfunApp$': 'ZF_ZF_ZF_fun_fun$').
% 9.12/2.40 tff(func_def_201, type, 'collect$c': 'ZF_bool_fun$' > 'ZF_set$').
% 9.12/2.40 tff(func_def_202, type, 'fun_app$ae': ('B_set_b_set_fun$' * 'B_set$') > 'B_set$').
% 9.12/2.40 tff(func_def_203, type, 'mapM$f': ('A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'B$') > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_204, type, 'isomorphism$a': 'ZF_ZF_unit_Category_ext$' > 'ZF_bool_fun$').
% 9.12/2.40 tff(func_def_205, type, 'nTCod_update$': ('ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$') > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_206, type, 'hOMCollection$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'A$' * 'A$') > 'ZF_set$').
% 9.12/2.40 tff(func_def_207, type, 'uuw$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_b_prod_bool_fun$').
% 9.12/2.40 tff(func_def_208, type, 'uuh$': 'B_b_prod_set$' > 'B_b_prod_bool_fun$').
% 9.12/2.40 tff(func_def_209, type, 'functorM_axioms$a': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$').
% 9.12/2.40 tff(func_def_210, type, 'comp$': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_ZF_fun_fun$').
% 9.12/2.40 tff(func_def_211, type, 'isomorphism$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_bool_fun$').
% 9.12/2.40 tff(func_def_212, type, 'makeNT$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_213, type, 'fun_app$o': ('B_ZF_fun$' * 'B$') > 'ZF$').
% 9.12/2.40 tff(func_def_214, type, 'catDom$e': 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' > 'ZF_ZF_unit_Category_ext$').
% 9.12/2.40 tff(func_def_215, type, 'inverse$a': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'B$') > 'B$').
% 9.12/2.40 tff(func_def_216, type, 'mapM$b': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > 'ZF_ZF_fun$').
% 9.12/2.40 tff(func_def_217, type, 'fun_app$ad': ('ZF_set_ZF_set_fun$' * 'ZF_set$') > 'ZF_set$').
% 9.12/2.40 tff(func_def_218, type, 'fun_app$aa': ('Unit_unit_fun$' * 'Unit$') > 'Unit$').
% 9.12/2.40 tff(func_def_219, type, 'obj$': 'ZF_ZF_unit_Category_ext$' > 'ZF_set$').
% 9.12/2.40 tff(func_def_220, type, 'homFtorMapContra$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'B$') > 'A_ZF_fun$').
% 9.12/2.40 tff(func_def_221, type, 'elem$': 'ZF$' > 'ZF_bool_fun$').
% 9.12/2.40 tff(func_def_222, type, 'comp$a': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_b_b_fun_fun$').
% 9.12/2.40 tff(func_def_223, type, 'yFtorNT$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'B$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_224, type, 'nTCatCod$f': 'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$' > 'Unit_unit_unit_Category_ext$').
% 9.12/2.40 tff(func_def_225, type, 'fun_app$v': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_226, type, 'nTDom$d': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_227, type, 'catExp$b': ('ZF_ZF_unit_Category_ext$' * 'ZF_ZF_unit_Category_ext$') > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$').
% 9.12/2.40 tff(func_def_228, type, 'more_update$a': 'Unit_unit_fun$' > 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$').
% 9.12/2.40 tff(func_def_229, type, 'catDom$d': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' > 'A_b_b_c_LSCategory_ext_Category_ext$').
% 9.12/2.40 tff(func_def_230, type, 'fun_app$': ('ZF_ZF_fun$' * 'ZF$') > 'ZF$').
% 9.12/2.40 tff(func_def_231, type, 'comp$d': 'ZF_ZF_fun$' > 'ZF_ZF_fun_ZF_ZF_fun_fun$').
% 9.12/2.40 tff(func_def_232, type, 'mapO$c': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A_ZF_fun$').
% 9.12/2.40 tff(func_def_233, type, 'constFunctor$b': ('ZF_ZF_unit_Category_ext$' * 'ZF_ZF_unit_Category_ext$' * 'ZF$') > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_234, type, 'collect$i': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$').
% 9.12/2.40 tff(func_def_235, type, 'yFtorNT$a': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$').
% 9.12/2.40 tff(func_def_236, type, 'mapsTo$a': ('ZF_ZF_unit_Category_ext$' * 'ZF$' * 'ZF$') > 'ZF_bool_fun$').
% 9.12/2.40 tff(func_def_237, type, 'makeCat$': 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$').
% 9.12/2.40 tff(func_def_238, type, 'mapM$c': ('ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' * 'ZF$') > 'B$').
% 9.12/2.40 tff(func_def_239, type, 'mor$a': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$').
% 9.12/2.40 tff(func_def_240, type, 'extensional$': 'ZF_set$' > 'ZF_ZF_fun_set$').
% 9.12/2.40 tff(func_def_241, type, 'uuu$': 'ZF_ZF_fun$').
% 9.12/2.40 tff(func_def_242, type, 'natTransComp$a': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_243, type, 'uug$': 'ZF_ZF_prod_set$' > 'ZF_ZF_prod_bool_fun$').
% 9.12/2.40 tff(func_def_244, type, 'id$a': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_fun$').
% 9.12/2.40 tff(func_def_245, type, 'image$': ('ZF_ZF_set_fun$' * 'ZF_set$') > 'ZF_set_set$').
% 9.12/2.40 tff(func_def_246, type, 'restrict$b': ('B_ZF_fun$' * 'B_set$') > 'B_ZF_fun$').
% 9.12/2.40 tff(func_def_247, type, 'uuj$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_b_b_fun_fun$').
% 9.12/2.40 tff(func_def_248, type, 'id_update$': 'ZF_ZF_fun_ZF_ZF_fun_fun$' > 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$').
% 9.12/2.40 tff(func_def_249, type, 'yFtor$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_250, type, 'homFtor$a': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'A$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_251, type, 'preFunctor$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$').
% 9.12/2.40 tff(func_def_252, type, 'idNatTrans$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_253, type, 'cod$': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_fun$').
% 9.12/2.40 tff(func_def_254, type, 'pair$': ('ZF$' * 'ZF$') > 'ZF_ZF_prod$').
% 9.12/2.40 tff(func_def_255, type, 'nTCod$d': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_256, type, 'makeCat$b': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$').
% 9.12/2.40 tff(func_def_257, type, 'nTCod$b': 'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$' > 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_258, type, 'homSet$': ('A_b_b_c_LSCategory_ext_Category_ext$' * 'A$') > 'A_ZF_fun$').
% 9.12/2.40 tff(func_def_259, type, 'uue$': 'A_ZF_fun_set$' > 'A_ZF_fun_bool_fun$').
% 9.12/2.40 tff(func_def_260, type, 'collect$g': 'A_ZF_fun_bool_fun$' > 'A_ZF_fun_set$').
% 9.12/2.40 tff(func_def_261, type, 'nTCatDom$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A_b_b_c_LSCategory_ext_Category_ext$').
% 9.12/2.40 tff(func_def_262, type, 'explode$': 'ZF_ZF_set_fun$').
% 9.12/2.40 tff(func_def_263, type, 'isZFfun$': 'ZF_bool_fun$').
% 9.12/2.40 tff(func_def_264, type, 'fun_app$y': ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$') > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_265, type, 'mapO$d': ('ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$' * 'ZF$') > 'Unit$').
% 9.12/2.40 tff(func_def_266, type, 'mor$b': 'ZF_ZF_unit_Category_ext$' > 'ZF_set$').
% 9.12/2.40 tff(func_def_267, type, 'nTCatCod$c': 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$').
% 9.12/2.40 tff(func_def_268, type, 'natTransComp$e': ('A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' * 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$') > 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$').
% 9.12/2.40 tff(func_def_269, type, 'uuc$': 'B_ZF_fun_set$' > 'B_ZF_fun_bool_fun$').
% 9.12/2.40 tff(func_def_270, type, 'nTCatCod$b': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'A_b_b_c_LSCategory_ext_Category_ext$').
% 9.12/2.40 tff(func_def_271, type, 'dom$a': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_fun$').
% 9.12/2.40 tff(func_def_272, type, 'nTCatDom$e': 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A_b_b_c_LSCategory_ext_Category_ext$').
% 9.12/2.40 tff(func_def_273, type, 'comp$c': ('Unit_unit_unit_Category_ext$' * 'Unit$') > 'Unit_unit_fun$').
% 9.12/2.40 tff(func_def_274, type, 'natTransComp$c': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$').
% 9.12/2.40 tff(func_def_275, type, 'mapO$a': ('A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' * 'A$') > 'A$').
% 9.12/2.40 tff(func_def_276, type, 'mapO$e': ('ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' * 'ZF$') > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$').
% 9.12/2.40 tff(func_def_277, type, 'mor$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_set$').
% 9.12/2.40 tff(func_def_278, type, sK1: ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$') > 'A$').
% 9.12/2.40 tff(func_def_279, type, sK2: ('ZF_ZF_unit_Category_ext$' * 'ZF$') > 'ZF$').
% 9.12/2.40 tff(func_def_280, type, sK3: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A$').
% 9.12/2.40 tff(func_def_281, type, sK4: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'B$').
% 9.12/2.40 tff(func_def_282, type, sK5: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A$').
% 9.12/2.40 tff(func_def_283, type, sK6: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A$').
% 9.12/2.40 tff(func_def_284, type, sK7: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A$').
% 9.12/2.40 tff(func_def_285, type, sK8: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'B$').
% 9.12/2.40 tff(func_def_286, type, sK9: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A$').
% 9.12/2.40 tff(func_def_287, type, sK10: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A$').
% 9.12/2.40 tff(func_def_288, type, sK11: ('ZF$' * 'ZF$') > 'ZF$').
% 9.12/2.40 tff(func_def_289, type, sK12: ('ZF$' * 'ZF_ZF_fun$' * 'ZF$') > 'ZF$').
% 9.12/2.40 tff(func_def_290, type, sK13: ('ZF$' * 'ZF_ZF_fun$' * 'ZF_ZF_fun$') > 'ZF$').
% 9.12/2.40 tff(func_def_291, type, sK14: ('A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$') > 'A$').
% 9.12/2.40 tff(f28,conjecture,(
% 9.12/2.40 'nTCatDom$'('yFtorNT$'('c$','f$')) = 'catDom$'('fun_app$r'('nTCod$','yFtorNT$'('c$','f$')))),
% 9.12/2.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture27)).
% 9.12/2.40
% 9.12/2.40 tff(f29,negated_conjecture,(
% 9.12/2.40 ~ 'nTCatDom$'('yFtorNT$'('c$','f$')) = 'catDom$'('fun_app$r'('nTCod$','yFtorNT$'('c$','f$')))),
% 9.12/2.40 inference(negated_conjecture,[status(cth)],[f28])).
% 9.12/2.40
% 9.12/2.40 tff(f34,axiom,(
% 9.12/2.40 'functor_abbrev$'('fun_app$r'('nTCod$','yFtorNT$'('c$','f$')),'fun_app$s'('oppositeCategory$','c$'),'set$')),
% 9.12/2.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom32)).
% 9.12/2.40
% 9.12/2.40 tff(f38,axiom,(
% 9.12/2.40 ! [X0 : 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'] : 'nTCatDom$'(X0) = 'catDom$'('fun_app$r'('nTDom$',X0))),
% 9.12/2.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom36)).
% 9.12/2.40
% 9.12/2.40 tff(f39,axiom,(
% 9.12/2.40 'functor_abbrev$'('fun_app$r'('nTDom$','yFtorNT$'('c$','f$')),'fun_app$s'('oppositeCategory$','c$'),'set$')),
% 9.12/2.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom37)).
% 9.12/2.40
% 9.12/2.40 tff(f74,axiom,(
% 9.12/2.40 ! [X0 : 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$',X1 : 'A_b_b_c_LSCategory_ext_Category_ext$',X2 : 'ZF_ZF_unit_Category_ext$'] : (('functor_abbrev$'(X0,X1,X2) & (('fun_app$a'('functor$',X0) & 'catDom$'(X0) = X1 & 'catCod$'(X0) = X2) => $false)) => $false)),
% 9.12/2.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom72)).
% 9.12/2.40
% 9.12/2.40 tff(f591,plain,(
% 9.12/2.40 'nTCatDom$'('yFtorNT$'('c$','f$')) != 'catDom$'('fun_app$r'('nTCod$','yFtorNT$'('c$','f$')))),
% 9.12/2.40 inference(flattening,[],[f29])).
% 9.12/2.40
% 9.12/2.40 tff(f592,plain,(
% 9.12/2.40 ! [X0 : 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$',X1 : 'A_b_b_c_LSCategory_ext_Category_ext$',X2 : 'ZF_ZF_unit_Category_ext$'] : ~('functor_abbrev$'(X0,X1,X2) & ~('fun_app$a'('functor$',X0) & 'catDom$'(X0) = X1 & 'catCod$'(X0) = X2))),
% 9.12/2.40 inference(true_and_false_elimination,[],[f74])).
% 9.12/2.40
% 9.12/2.40 tff(f618,plain,(
% 9.12/2.40 ! [X0 : 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$',X1 : 'A_b_b_c_LSCategory_ext_Category_ext$',X2 : 'ZF_ZF_unit_Category_ext$'] : (~'functor_abbrev$'(X0,X1,X2) | ('fun_app$a'('functor$',X0) & 'catDom$'(X0) = X1 & 'catCod$'(X0) = X2))),
% 9.12/2.40 inference(ennf_transformation,[],[f592])).
% 9.12/2.40
% 9.12/2.40 tff(f806,plain,(
% 9.12/2.40 'nTCatDom$'('yFtorNT$'('c$','f$')) != 'catDom$'('fun_app$r'('nTCod$','yFtorNT$'('c$','f$')))),
% 9.12/2.40 inference(cnf_transformation,[],[f591])).
% 9.12/2.40
% 9.12/2.40 tff(f807,plain,(
% 9.12/2.40 'functor_abbrev$'('fun_app$r'('nTDom$','yFtorNT$'('c$','f$')),'fun_app$s'('oppositeCategory$','c$'),'set$')),
% 9.12/2.40 inference(cnf_transformation,[],[f39])).
% 9.12/2.40
% 9.12/2.40 tff(f808,plain,(
% 9.12/2.40 'functor_abbrev$'('fun_app$r'('nTCod$','yFtorNT$'('c$','f$')),'fun_app$s'('oppositeCategory$','c$'),'set$')),
% 9.12/2.40 inference(cnf_transformation,[],[f34])).
% 9.12/2.40
% 9.12/2.40 tff(f813,plain,(
% 9.12/2.40 ( ! [X0 : 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'] : ('nTCatDom$'(X0) = 'catDom$'('fun_app$r'('nTDom$',X0))) )),
% 9.12/2.40 inference(cnf_transformation,[],[f38])).
% 9.12/2.40
% 9.12/2.40 tff(f837,plain,(
% 9.12/2.40 ( ! [X2 : 'ZF_ZF_unit_Category_ext$',X0 : 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$',X1 : 'A_b_b_c_LSCategory_ext_Category_ext$'] : (~'functor_abbrev$'(X0,X1,X2) | 'catDom$'(X0) = X1) )),
% 9.12/2.40 inference(cnf_transformation,[],[f618])).
% 9.12/2.40
% 9.12/2.40 tff(f993,plain,(
% 9.12/2.40 'catDom$'('fun_app$r'('nTCod$','yFtorNT$'('c$','f$'))) != 'catDom$'('fun_app$r'('nTDom$','yFtorNT$'('c$','f$')))),
% 9.12/2.40 inference(definition_unfolding,[],[f806,f813])).
% 9.12/2.40
% 9.12/2.40 tcf(c_49,negated_conjecture,
% 9.12/2.40 ('catDom$'('fun_app$r'('nTDom$','yFtorNT$'('c$','f$'))) != 'catDom$'('fun_app$r'('nTCod$','yFtorNT$'('c$','f$')))),
% 9.12/2.40 inference(cnf_transformation,[],[f993])).
% 9.12/2.40
% 9.12/2.40 tcf(c_50,plain,
% 9.12/2.40 ('functor_abbrev$'('fun_app$r'('nTDom$','yFtorNT$'('c$','f$')),'fun_app$s'('oppositeCategory$','c$'),'set$')),
% 9.12/2.40 inference(cnf_transformation,[],[f807])).
% 9.12/2.40
% 9.12/2.40 tcf(c_51,plain,
% 9.12/2.40 ('functor_abbrev$'('fun_app$r'('nTCod$','yFtorNT$'('c$','f$')),'fun_app$s'('oppositeCategory$','c$'),'set$')),
% 9.12/2.40 inference(cnf_transformation,[],[f808])).
% 9.12/2.40
% 9.12/2.40 tcf(c_79,plain,![X0_'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext':'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$',X0_'A_b_b_c_LSCategory_ext_Category_ext':'A_b_b_c_LSCategory_ext_Category_ext$',X0_'ZF_ZF_unit_Category_ext':'ZF_ZF_unit_Category_ext$']:
% 9.12/2.40 (~'functor_abbrev$'(X0_'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext',X0_'A_b_b_c_LSCategory_ext_Category_ext',X0_'ZF_ZF_unit_Category_ext')|
% 9.12/2.40 'catDom$'(X0_'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext') = X0_'A_b_b_c_LSCategory_ext_Category_ext'),
% 9.12/2.40 inference(cnf_transformation,[],[f837])).
% 9.12/2.40
% 9.12/2.40 tcf(c_9779,plain,
% 9.12/2.40 ('catDom$'('fun_app$r'('nTDom$','yFtorNT$'('c$','f$'))) = 'fun_app$s'('oppositeCategory$','c$')),
% 9.12/2.40 inference(superposition,[status(thm)],[c_50,c_79])).
% 9.12/2.40
% 9.12/2.40 tcf(c_9780,plain,
% 9.12/2.40 ('catDom$'('fun_app$r'('nTCod$','yFtorNT$'('c$','f$'))) = 'fun_app$s'('oppositeCategory$','c$')),
% 9.12/2.40 inference(superposition,[status(thm)],[c_51,c_79])).
% 9.12/2.40
% 9.12/2.40 tcf(c_9782,plain,
% 9.12/2.40 ('catDom$'('fun_app$r'('nTCod$','yFtorNT$'('c$','f$'))) != 'fun_app$s'('oppositeCategory$','c$')),
% 9.12/2.40 inference(demodulation,[status(thm)],[c_49,c_9779])).
% 9.12/2.40
% 9.12/2.40 tcf(c_9783,plain,
% 9.12/2.40 ($false),
% 9.12/2.40 inference(forward_subsumption_resolution,[status(thm)],[c_9782,c_9780])).
% 9.12/2.40
% 9.12/2.40
% 9.12/2.40 % SZS output end CNFRefutation for theBenchmark.p
% 9.12/2.40
% 9.12/2.40
%------------------------------------------------------------------------------