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 SatSolverExchange.add_clause: SAT solver returned unsatisfiable. ------ Statistics ------ General num_of_input_clauses: 202 num_of_input_neg_conjectures: 4 num_of_splits: 0 num_of_split_atoms: 0 forced_gc_time: 0 num_of_symbols: 118 num_of_terms: 3893 ------ Propositional Solver prop_solver_calls: 0 prop_fast_solver_calls: 0 prop_num_of_clauses: 811 prop_preprocess_simplified: 233 prop_fo_subsumed: 177 prop_solver_time_sum: 0.00116562843323 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: 331 inst_num_in_passive: 8 inst_num_in_active: 272 inst_num_in_unprocessed: 51 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: 24 inst_lit_activity: 63 inst_lit_activity_moves: 0 inst_num_tautologies: 0 inst_num_prop_implied: 0 inst_num_existing_simplified: 0 inst_num_child_elim: 0 inst_num_of_dismatching_blockings: 0 inst_num_of_non_proper_insts: 171 inst_num_of_duplicates: 0 inst_inst_num_from_inst_to_res: 0 ------ Resolution res_num_of_clauses: 307 res_num_in_passive: 131 res_num_in_passive_sim: 0 res_num_in_active: 175 res_num_of_loops: 313 res_forward_subset_subsumed: 147 res_backward_subset_subsumed: 12 res_forward_subsumed: 0 res_backward_subsumed: 41 res_forward_subsumption_resolution: 0 res_backward_subsumption_resolution: 0 res_clause_to_clause_subsumption: 687 res_orphan_elimination: 1 res_tautology_del: 13 res_num_sel_changes: 400 res_moves_from_active_to_pass: 70 inst_dismatching_checking_time: 6.46114349365e-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: 296 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.49 CPU 0.56 WC FINAL WATCH: 0.49 CPU 0.56 WC