%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWV909-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n012.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 03:24:27 PM UTC 2026
% Result : Unsatisfiable 226.52s 45.75s
% Output : CNFRefutation 226.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 7
% Syntax : Number of formulae : 27 ( 22 unt; 0 def)
% Number of atoms : 32 ( 13 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 12 ( 7 ~; 5 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 7 con; 0-4 aty)
% Number of variables : 60 ( 0 sgn 60 !; 0 ?; 43 :)
% Comments :
%------------------------------------------------------------------------------
fof(f305,axiom,
! [X0,X1] : c_Collect(X0,X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Collect__def_0) ).
fof(f631,axiom,
! [X0,X1] : c_Collect(hAPP(c_fequal(X0),X1),X0) = hAPP(c_Set_Oinsert(X1,X0),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_singleton__conv2_0) ).
fof(f632,plain,
! [X0,X1] : hAPP(c_Set_Oinsert(X1,X0),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))) = c_Collect(hAPP(c_fequal(X0),X1),X0),
inference(reorient_equations,[],[f631]) ).
fof(f682,axiom,
! [X2,X3,X0,X1] :
( hBOOL(hAPP(hAPP(X1,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(X0,X1,X3,X2)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(X0,X1,X3,X2)))
| c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_hoare__derivs_Ointros_I6_J_0) ).
fof(f697,axiom,
! [X0] : c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) = c_Collect(c_COMBK(c_False,tc_bool,X0),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty__def_0) ).
fof(f713,axiom,
! [X0,X1] : ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_bot1E_0) ).
fof(f727,negated_conjecture,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(c_COMBK(c_COMBK(c_False,tc_bool,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool),t_a),v_c,v_Q,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f766,axiom,
! [X2,X3,X0,X1] : hAPP(c_COMBK(X0,X1,X2),X3) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ATP__Linkup_OCOMBK__def_0) ).
tcf(c_971,plain,
! [X0: $i,X1: $i] : c_Collect(X0,X1) = X0,
inference(cnf_transformation,[],[f305]) ).
tcf(c_1235,plain,
! [X0: $i,X1: $i] : hAPP(c_Set_Oinsert(X0,X1),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))) = c_Collect(hAPP(c_fequal(X1),X0),X1),
inference(cnf_transformation,[],[f632]) ).
tcf(c_1272,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( hBOOL(hAPP(hAPP(X1,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(X0,X1,X3,X2)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(X0,X1,X3,X2)))
| c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
inference(cnf_transformation,[],[f682]) ).
tcf(c_1285,plain,
! [X0: $i] : c_Collect(c_COMBK(c_False,tc_bool,X0),X0) = c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),
inference(cnf_transformation,[],[f697]) ).
tcf(c_1300,plain,
! [X0: $i,X1: $i] : ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[],[f713]) ).
tcf(c_1311,negated_conjecture,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(c_COMBK(c_COMBK(c_False,tc_bool,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool),t_a),v_c,v_Q,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a),
inference(cnf_transformation,[],[f727]) ).
tcf(c_1350,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : hAPP(c_COMBK(X0,X1,X2),X3) = X0,
inference(cnf_transformation,[],[f766]) ).
tcf(c_2740,plain,
! [X0: $i] : c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) = c_COMBK(c_False,tc_bool,X0),
inference(demodulation,[status(thm)],[c_1285,c_971]) ).
tcf(c_4295,plain,
! [X0: $i,X1: $i] : hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) = c_False,
inference(superposition,[status(thm)],[c_2740,c_1350]) ).
tcf(c_23061,plain,
~ hBOOL(c_False),
inference(superposition,[status(thm)],[c_4295,c_1300]) ).
tcf(c_301159,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(c_COMBK(c_COMBK(c_False,tc_bool,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool),t_a),v_c,v_Q,t_a)),t_a),
inference(demodulation,[status(thm)],[c_1311,c_971,c_1235]) ).
tcf(c_301533,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_Hoare__Mirabelle_Ohoare__derivs(X1,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X0,X3,X2,t_a)),t_a)
| hBOOL(hAPP(hAPP(X0,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(X1,X0,X2,X3)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(X1,X0,X2,X3))) ),
inference(demodulation,[status(thm)],[c_1272,c_971,c_1235]) ).
tcf(c_302313,plain,
! [X0: $i] : c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) = c_COMBK(c_False,tc_bool,X0),
inference(demodulation,[status(thm)],[c_1285,c_971]) ).
tcf(c_302315,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(c_COMBK(c_Orderings_Obot__class_Obot(tc_fun(tc_Com_Ostate,tc_bool)),tc_fun(tc_Com_Ostate,tc_bool),t_a),v_c,v_Q,t_a)),t_a),
inference(superposition,[status(thm)],[c_302313,c_301159]) ).
tcf(c_303624,plain,
! [X0: $i,X1: $i] : hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) = c_False,
inference(superposition,[status(thm)],[c_302313,c_1350]) ).
tcf(c_303625,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( hBOOL(hAPP(X1,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(X0,c_COMBK(X1,X2,X3),X5,X4)))
| c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(c_COMBK(X1,X2,X3),X4,X5,t_a)),t_a) ),
inference(superposition,[status(thm)],[c_1350,c_301533]) ).
tcf(c_331405,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( hBOOL(c_False)
| c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(c_COMBK(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2,X3),X4,X5,t_a)),t_a) ),
inference(superposition,[status(thm)],[c_303624,c_303625]) ).
tcf(c_331439,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(c_COMBK(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2,X3),X4,X5,t_a)),t_a),
inference(global_subsumption_just,[status(thm)],[c_331405,c_23061,c_331405]) ).
tcf(c_331592,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[c_302315,c_331439]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWV909-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.04/15.33 % Computer : n012.cluster.edu
% 0.04/15.33 % Model : x86_64 x86_64
% 0.04/15.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/15.33 % Memory : 8046.5625MB
% 0.04/15.33 % OS : Linux 6.8.0-71-generic
% 0.04/15.33 % CPULimit : 300
% 0.04/15.33 % WCLimit : 300
% 0.04/15.33 % DateTime : Thu Sep 24 21:16:54 UTC 2026
% 0.04/15.33 % CPUTime :
% 0.04/15.33 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.04/15.35 Running first-order theorem proving
% 0.04/15.35 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.04/15.36
% 0.04/15.36 % ======== iProver multi-core TPTP/SMT =========
% 0.04/15.36
% 0.04/15.36 % Detected problem language: tptp
% 0.04/15.36 % Proving...
% 226.52/45.75 % SZS status Started for theBenchmark.p
% 226.52/45.75 ERROR - "ProverProcess:heur/330959:296.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clause.get_demod_eqs: not a demod/lightnorm conclusion ( ~c_Fun_Oinj__on(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),c_Orderings_Otop__class_Otop(tc_fun(X1,tc_bool)),X1,X2) | X3 = X4 )")
% 226.52/45.75 Fatal error: exception Failure("Clause.get_demod_eqs: not a demod/lightnorm conclusion ( ~c_Fun_Oinj__on(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),c_Orderings_Otop__class_Otop(tc_fun(X1,tc_bool)),X1,X2) | X3 = X4 )")
% 226.52/45.75 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref "[]" --abstr_ref_af_restrict_to_split_sk false --abstr_ref_prep false --abstr_ref_sig_restrict funpre --abstr_ref_under "[]" --abstr_ref_until_sat false --add_important_lit false --bc_imp_inh "[conj_cone]" --brand_transform false --clause_weak_htbl true --comb_inst_mult 3 --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 --gc_record_bc_elim false --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_sos_phase true --inst_sos_sth_lit_sel "[+prop;+non_prol_conj_symb;-eq;+ground;-num_var]" --inst_start_prop_sim_after_learn 3 --inst_subs_given false --inst_subs_new false --instantiation_flag true --large_theory_mode true --lt_threshold 2000 --min_unsat_core false --non_eq_to_eq false --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_sem_filter_out false --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten true --prep_upred true --preprocessed_out false --preprocessed_stats false --preprocessing_flag true --prolific_symb_bound 256 --prop_impl_unit "[]" --prop_impl_unit_size 0 --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_orphan_elimination true --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. --res_to_prop_solver active --reset_solvers false --resolution_flag true --schedule none --share_sel_clauses true --smt_ac_axioms fast --smt_preprocessing true --soft_assumptions false --soft_lemma_size 3 --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 "[BwDemod;BwUnitSubsAndRes]" --sup_full_fw "[FwDemodLightNormLoopTriv;FwUnitSubsAndRes;FwSubsumption;FwSubsumptionRes]" --sup_full_triv "[PropSubs]" --sup_fun_splitting false --sup_immed_bw_immed "[BwUnitSubsAndRes]" --sup_immed_bw_main "[BwUnitSubsAndRes]" --sup_immed_fw_immed "[ACNormalisation;FwDemodLightNormLoopTriv;FwUnitSubsAndRes]" --sup_immed_fw_main "[FwUnitSubsAndRes]" --sup_immed_triv "[]" --sup_indices_passive "[LightNormIndex;UnitSubsumptionIndex]" --sup_input_bw "[BwDemod;BwUnitSubsAndRes;BwSubsumption;BwSubsumptionRes]" --sup_input_fw "[ACNormalisation;FwDemodLightNormLoopTriv;FwUnitSubsAndRes;FwSubsumption;FwSubsumptionRes]" --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 --out_options none --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode clausify -t 98.67" --time_out_real 296.00 /export/starexec/sandbox/benchmark/theBenchmark.p 1>> /export/starexec/sandbox/tmp/iprover_out_pul87sl5/f4biti2b 2>> /export/starexec/sandbox/tmp/iprover_out_pul87sl5/f4biti2b_error
% 226.52/45.75 % SZS status Unsatisfiable for theBenchmark.p
% 226.52/45.75
% 226.52/45.75 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 226.52/45.75
% 226.52/45.75 % ------ iProver source info
% 226.52/45.75
% 226.52/45.75 % git: date: 2026-07-19 20:42:38 +0200
% 226.52/45.75 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 226.52/45.75 % git: non_committed_changes: false
% 226.52/45.75
% 226.52/45.75 % ------ Parsing...% successful
% 226.52/45.75
% 226.52/45.75
% 226.52/45.75 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 226.52/45.75
% 226.52/45.75 % ------ Preprocessing... sf_s rm: 7 0s sf_e sf_s rm: 3 0s sf_e %
% 226.52/45.75
% 226.52/45.75 % ------ Preprocessing...%
% 226.52/45.75
% 226.52/45.75 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 226.52/45.75 % ------ Proving...
% 226.52/45.75 % ------ Problem Properties
% 226.52/45.75
% 226.52/45.75 %
% 226.52/45.75 % clauses 540
% 226.52/45.75 % conjectures 1
% 226.52/45.75 % EPR 27
% 226.52/45.75 % Horn 475
% 226.52/45.75 % unary 150
% 226.52/45.75 % binary 200
% 226.52/45.75 % lits 1181
% 226.52/45.75 % lits eq 314
% 226.52/45.75 % fd_pure 0
% 226.52/45.75 % fd_pseudo 0
% 226.52/45.75 % fd_cond 0
% 226.52/45.75 % fd_pseudo_cond 60
% 226.52/45.75 % AC symbols 0
% 226.52/45.75
% 226.52/45.75 % ------ Input Options Time Limit: Unbounded
% 226.52/45.75
% 226.52/45.75
% 226.52/45.75 % ------
% 226.52/45.75 % Current options:
% 226.52/45.75 % ------
% 226.52/45.75
% 226.52/45.75
% 226.52/45.75 %
% 226.52/45.75
% 226.52/45.75 % ------ Proving...
% 226.52/45.75 %
% 226.52/45.75
% 226.52/45.75 % SZS status Unsatisfiable for theBenchmark.p
% 226.52/45.75
% 226.52/45.75 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 226.52/45.75
% 226.52/45.75
%------------------------------------------------------------------------------