WATCH: 0.00 CPU 0.01 WC ---------------- iProver-Eq CASC-23 --------------- ------ Input Options --out_options all --problem_path "" --include_path "" --clausifier "" --clausifier_options "" --stdin false ------ General Options --fof true --ground_splitting input --prep_prop_sim false --prop_fast_solve true --prop_gnd_by_bot false --time_out_real 0. --time_out_virtual 300. --schedule none --non_eq_to_eq true --gnd_solver auto --sim_gnd_solver EUF --dismatching_constr index --dismatching_index_min_size 10 --large_theory_mode true --prolific_symb_bound 500 --lt_threshold 2000 --sat_mode false --sat_gr_def false --sat_finite_models false --sat_out_model small ------ Instantiation Options --instantiation_flag true --inst_loop lazy_with_renewal --inst_run_solver_lit false --inst_lit_sel [+fun_pred;-var_eq;-gnd_taut;-sign;+ground;-num_var;-num_symb] --inst_solver_per_active 750 --inst_solver_per_clauses 5000 --inst_pass_queue1 [+pos_ueq;-conj_dist;+conj_symb;-num_var] --inst_pass_queue2 [+age;-num_symb] --inst_pass_queue1_mult 25 --inst_pass_queue2_mult 2 --inst_dismatching true --inst_eager_unprocessed_to_passive true --inst_prop_sim_given false --inst_prop_sim_new true --inst_prop_sim_max_len 0 --inst_learning_loop_flag false --inst_learning_start 3000 --inst_learning_factor 2 --inst_start_prop_sim_after_learn 3 --inst_out_prop_clauses false ------ Resolution Options --resolution_flag true --res_lit_sel adaptive --res_to_prop_solver active --res_prop_simpl_new false --res_prop_simpl_given true --res_prop_simpl_max_len 0 --res_passive_queue_flag true --res_pass_queue1 [-conj_dist;+conj_symb;-num_symb] --res_pass_queue2 [+age;-num_symb] --res_pass_queue1_mult 15 --res_pass_queue2_mult 5 --res_forward_subs full --res_backward_subs full --res_forward_subs_resolution true --res_backward_subs_resolution true --res_orphan_elimination true --res_time_limit 2. ------ Unit Paramodulation Options --ueq_only auto --unitparamod_flag true --up_dismatching true --up_dismatch_given true --up_pass_queue1 [+unit;-sign;+ground;-num_var;-num_symb] --up_pass_queue2 [+age;-num_symb] --up_pass_queue1_mult 20 --up_pass_queue2_mult 10 --up_orient_after_subst true --up_superposition true --up_use_demod true --up_demod_inst_eager false --up_demod_inst_to_solver_only true --up_demod_proper true --up_demod_with_all false --up_demod_both_sides true --up_demod_clauses true --up_demod_given true --up_demod_active true --up_demod_concl true --up_demod_concl_cached false --up_demod_eager_from_concl true --up_demod_from_inst true --up_unit_not_neg false --up_pure_lit_proof true --up_dism_for_unit_literals true --up_dism_check_equation true --up_literal_labels tree_active --up_literal_age parent --up_label_to_passive_minus_active false --up_check_inference_label_subsumption true --ueq_check_with_solver false --up_lit_activity_threshold 200 --up_unselect_var_eq true ------ Combination Options --comb_res_mult 100 --comb_inst_mult 100 --comb_up_mult 100 ------ ------ Parsing... ------ Clausification by vclausify_rel & Parsing by iProver... ------ Non-equational problem: switching off unit paramodulation, using only instantiation. ------ Non-equational problem: not translating non-equational predicates. ------ Omitting equality axioms ------ Problem Properties EPR false Horn false Has equality false Unit equational false ------ Proving... % SZS status Theorem Empty clause in resolution ------ Statistics ------ General num_of_input_clauses: 159 num_of_input_neg_conjectures: 8 num_of_splits: 14 num_of_split_atoms: 14 forced_gc_time: 0 num_of_symbols: 160 num_of_terms: 674 ------ Propositional Solver prop_solver_calls: 0 prop_fast_solver_calls: 0 prop_num_of_clauses: 557 prop_preprocess_simplified: 223 prop_fo_subsumed: 112 prop_solver_time_sum: 0.00114560127258 prop_solver_time_lit_val: 0. prop_solver_time_solve: 0. prop_solver_time_solve_assumptions: 0. prop_solver_time_fast_solve: 0. prop_solver_time_find_consistent_assumptions: 0. check_constr_norm_list_time: 0. ------ Instantiation inst_num_of_clauses: 208 inst_num_in_passive: 7 inst_num_in_active: 197 inst_num_in_unprocessed: 0 inst_num_in_simple_passive: 0 inst_num_of_loops: 300 inst_num_of_selection_renewals: 0 inst_num_of_learning_restarts: 0 inst_num_moves_active_passive: 89 inst_lit_activity: 9 inst_lit_activity_moves: 0 inst_num_tautologies: 0 inst_num_prop_implied: 0 inst_num_existing_simplified: 1 inst_num_child_elim: 0 inst_num_of_dismatching_blockings: 0 inst_num_of_non_proper_insts: 31 inst_num_of_duplicates: 0 inst_inst_num_from_inst_to_res: 0 ------ Resolution res_num_of_clauses: 63 res_num_in_passive: 2 res_num_in_passive_sim: 0 res_num_in_active: 61 res_num_of_loops: 373 res_forward_subset_subsumed: 19 res_backward_subset_subsumed: 91 res_forward_subsumed: 1 res_backward_subsumed: 141 res_forward_subsumption_resolution: 24 res_backward_subsumption_resolution: 62 res_clause_to_clause_subsumption: 498 res_orphan_elimination: 30 res_tautology_del: 14 res_num_sel_changes: 176 res_moves_from_active_to_pass: 60 inst_dismatching_checking_time: 2.28881835938e-05 ------ Unit Paramodulation up_num_in_passive: 0 up_num_of_literals: 0 up_closures_in_bdd_labels: 0 up_nodes_in_bdd_labels: 2 up_labels_htree_table_len: undef up_labels_htree_num_entries: undef up_num_of_loops: 0 up_num_in_active: 0 up_num_in_unprocessed: 286 up_num_of_new_demodulators: 0 up_sel_not_oriented: 0 up_eliminated_active_passive_inter: 0 up_eliminated_closures_in_label: 0 up_dismatched_literals: 0 up_clauses_demodulated: 0 up_given_demodulated: 0 up_active_demodulated: 0 up_conclusions_demodulated: 0 up_demodulators_demodulated: 0 up_input_demodulated: 0 up_demod_inst_eager: 0 up_unit_inst_eager: 0 up_given_simpl_after_demod_clauses: 0 up_active_simpl_after_demod_clauses: 0 up_inferences: 0 up_inferences_unit_lit: 0 up_dismatched_inferences: 0 up_dismatched_unit_premises: 0 up_eq_orient_after_subst: 0 up_lit_orient_after_subst: 0 up_tautologies: 0 up_inference_label_subsumed: 0 up_cycles: 0 up_contradictions: 0 up_gnd_lemmas: 0 up_proof_size_0: 0 up_proof_size_1: 0 up_proof_size_2: 0 up_proof_size_3: 0 up_proof_size_4: 0 up_proof_size_5: 0 up_proof_size_greater: 0 up_dismatched_contradictions: 0 up_duplicate_conclusions: 0 up_duplicate_unit_conclusions: 0 up_duplicate_insts: 0 up_non_proper_insts: 0 up_dismatched_proofs: 0 up_active_literals: 0 up_active_clauses: 0 up_unselected_var_eqs: 0 up_var_eq_lemmas: 0 WATCH: 0.70 CPU 0.74 WC FINAL WATCH: 0.70 CPU 0.74 WC