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... ------ Equational problem: using EUF ground solver ------ Equational problem: Switching off instantiation, using only unit paramodulation. ------ Omitting equality axioms ------ Problem Properties EPR false Horn true Has equality true Unit equational false ------ Proving... WATCH: 2.96 CPU 3.02 WC WATCH: 5.96 CPU 6.03 WC WATCH: 8.96 CPU 9.04 WC WATCH: 11.97 CPU 12.05 WC WATCH: 14.97 CPU 15.06 WC WATCH: 17.98 CPU 18.07 WC WATCH: 20.99 CPU 21.08 WC WATCH: 23.99 CPU 24.09 WC WATCH: 27.00 CPU 27.10 WC WATCH: 30.00 CPU 30.11 WC WATCH: 33.00 CPU 33.12 WC WATCH: 36.01 CPU 36.13 WC WATCH: 39.01 CPU 39.14 WC WATCH: 42.02 CPU 42.15 WC WATCH: 45.03 CPU 45.16 WC WATCH: 48.03 CPU 48.17 WC WATCH: 51.04 CPU 51.18 WC WATCH: 54.04 CPU 54.19 WC WATCH: 57.04 CPU 57.20 WC WATCH: 60.04 CPU 60.21 WC WATCH: 63.04 CPU 63.22 WC WATCH: 66.05 CPU 66.22 WC WATCH: 69.06 CPU 69.23 WC WATCH: 72.07 CPU 72.24 WC WATCH: 75.07 CPU 75.25 WC WATCH: 78.08 CPU 78.26 WC WATCH: 81.08 CPU 81.27 WC WATCH: 84.08 CPU 84.28 WC WATCH: 87.09 CPU 87.29 WC WATCH: 90.09 CPU 90.30 WC WATCH: 93.10 CPU 93.31 WC WATCH: 96.10 CPU 96.33 WC WATCH: 99.11 CPU 99.34 WC WATCH: 102.12 CPU 102.35 WC WATCH: 105.12 CPU 105.36 WC WATCH: 108.13 CPU 108.38 WC WATCH: 111.14 CPU 111.39 WC WATCH: 114.14 CPU 114.40 WC WATCH: 117.15 CPU 117.42 WC WATCH: 120.16 CPU 120.43 WC WATCH: 123.16 CPU 123.44 WC WATCH: 126.17 CPU 126.45 WC WATCH: 129.18 CPU 129.46 WC WATCH: 132.18 CPU 132.47 WC WATCH: 135.18 CPU 135.48 WC WATCH: 138.19 CPU 138.49 WC WATCH: 141.19 CPU 141.50 WC WATCH: 144.20 CPU 144.51 WC WATCH: 147.20 CPU 147.51 WC WATCH: 150.21 CPU 150.52 WC WATCH: 153.22 CPU 153.54 WC WATCH: 156.23 CPU 156.56 WC WATCH: 159.24 CPU 159.57 WC WATCH: 162.24 CPU 162.58 WC WATCH: 165.25 CPU 165.59 WC WATCH: 168.25 CPU 168.60 WC WATCH: 171.26 CPU 171.61 WC WATCH: 174.26 CPU 174.62 WC WATCH: 177.27 CPU 177.63 WC WATCH: 180.27 CPU 180.64 WC WATCH: 183.28 CPU 183.65 WC WATCH: 186.28 CPU 186.66 WC WATCH: 189.29 CPU 189.67 WC WATCH: 192.29 CPU 192.68 WC WATCH: 195.30 CPU 195.69 WC WATCH: 198.30 CPU 198.70 WC WATCH: 201.30 CPU 201.71 WC WATCH: 204.31 CPU 204.72 WC WATCH: 207.31 CPU 207.73 WC WATCH: 210.32 CPU 210.74 WC WATCH: 213.32 CPU 213.75 WC WATCH: 216.33 CPU 216.76 WC WATCH: 219.33 CPU 219.77 WC WATCH: 222.34 CPU 222.78 WC WATCH: 225.34 CPU 225.79 WC WATCH: 228.34 CPU 228.80 WC WATCH: 231.35 CPU 231.81 WC WATCH: 234.35 CPU 234.82 WC WATCH: 237.36 CPU 237.83 WC WATCH: 240.36 CPU 240.84 WC WATCH: 243.36 CPU 243.85 WC WATCH: 246.38 CPU 246.86 WC WATCH: 249.38 CPU 249.87 WC WATCH: 252.38 CPU 252.88 WC WATCH: 255.38 CPU 255.89 WC WATCH: 258.39 CPU 258.90 WC WATCH: 261.39 CPU 261.91 WC WATCH: 264.39 CPU 264.92 WC WATCH: 267.40 CPU 267.93 WC WATCH: 270.40 CPU 270.94 WC WATCH: 273.41 CPU 273.94 WC WATCH: 276.41 CPU 276.95 WC WATCH: 279.42 CPU 279.96 WC WATCH: 282.43 CPU 282.97 WC WATCH: 285.43 CPU 285.98 WC WATCH: 288.44 CPU 288.99 WC WATCH: 291.44 CPU 292.00 WC WATCH: 294.45 CPU 295.01 WC WATCH: 297.45 CPU 298.02 WC % SZS status Unknown Time Out Virtual ------ Statistics ------ General num_of_input_clauses: 18 num_of_input_neg_conjectures: 1 num_of_splits: 0 num_of_split_atoms: 0 forced_gc_time: 0 num_of_symbols: 32 num_of_terms: 13751 ------ Propositional Solver prop_solver_calls: 30 prop_fast_solver_calls: 0 prop_num_of_clauses: 46 prop_preprocess_simplified: 4 prop_fo_subsumed: 0 prop_solver_time_sum: 0.0141150951385 prop_solver_time_lit_val: 0.000922441482544 prop_solver_time_solve: 0.00289487838745 prop_solver_time_solve_assumptions: 0.00252532958984 prop_solver_time_fast_solve: 0.00254464149475 prop_solver_time_find_consistent_assumptions: 0.00245904922485 check_constr_norm_list_time: 0. ------ Instantiation inst_num_of_clauses: 22 inst_num_in_passive: 0 inst_num_in_active: 18 inst_num_in_unprocessed: 3 inst_num_in_simple_passive: 0 inst_num_of_loops: 20 inst_num_of_selection_renewals: 0 inst_num_of_learning_restarts: 0 inst_num_moves_active_passive: 0 inst_lit_activity: 0 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: 0 inst_num_of_duplicates: 0 inst_inst_num_from_inst_to_res: 0 ------ Resolution res_num_of_clauses: 21 res_num_in_passive: 0 res_num_in_passive_sim: 0 res_num_in_active: 21 res_num_of_loops: 26 res_forward_subset_subsumed: 3 res_backward_subset_subsumed: 0 res_forward_subsumed: 1 res_backward_subsumed: 0 res_forward_subsumption_resolution: 0 res_backward_subsumption_resolution: 0 res_clause_to_clause_subsumption: 33 res_orphan_elimination: 0 res_tautology_del: 0 res_num_sel_changes: 5 res_moves_from_active_to_pass: 3 inst_dismatching_checking_time: 0. ------ Unit Paramodulation up_num_in_passive: 750 up_num_of_literals: 906 up_closures_in_bdd_labels: 0 up_nodes_in_bdd_labels: 2032825 up_labels_htree_table_len: undef up_labels_htree_num_entries: undef up_num_of_loops: 46 up_num_in_active: 42 up_num_in_unprocessed: 0 up_num_of_new_demodulators: 0 up_sel_not_oriented: 1 up_eliminated_active_passive_inter: 0 up_eliminated_closures_in_label: 0 up_dismatched_literals: 0 up_clauses_demodulated: 0 up_given_demodulated: 409 up_active_demodulated: 7 up_conclusions_demodulated: 111 up_demodulators_demodulated: 1822 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: 795 up_inferences_unit_lit: 52 up_dismatched_inferences: 67 up_dismatched_unit_premises: 0 up_eq_orient_after_subst: 11 up_lit_orient_after_subst: 1 up_tautologies: 180 up_inference_label_subsumed: 0 up_cycles: 0 up_contradictions: 3 up_gnd_lemmas: 0 up_proof_size_0: 0 up_proof_size_1: 0 up_proof_size_2: 3 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: 3 up_dismatched_proofs: 0 up_active_literals: 0 up_active_clauses: 0 up_unselected_var_eqs: 0 up_var_eq_lemmas: 0 WATCH: 300.18 CPU 300.77 WC FINAL WATCH: 300.18 CPU 300.77 WC