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 true Horn true Has equality false Unit equational false ------ Proving... WATCH: 2.98 CPU 3.02 WC WATCH: 5.99 CPU 6.03 WC WATCH: 9.00 CPU 9.05 WC WATCH: 12.01 CPU 12.06 WC WATCH: 15.01 CPU 15.07 WC WATCH: 18.02 CPU 18.08 WC WATCH: 21.03 CPU 21.09 WC WATCH: 24.03 CPU 24.10 WC WATCH: 27.04 CPU 27.11 WC WATCH: 30.03 CPU 30.12 WC WATCH: 33.04 CPU 33.13 WC WATCH: 36.05 CPU 36.14 WC WATCH: 39.05 CPU 39.15 WC WATCH: 42.05 CPU 42.16 WC WATCH: 45.06 CPU 45.17 WC WATCH: 48.07 CPU 48.18 WC WATCH: 51.07 CPU 51.19 WC WATCH: 54.08 CPU 54.20 WC WATCH: 57.08 CPU 57.21 WC WATCH: 60.08 CPU 60.22 WC WATCH: 63.09 CPU 63.23 WC WATCH: 66.09 CPU 66.24 WC WATCH: 69.09 CPU 69.25 WC WATCH: 72.10 CPU 72.26 WC WATCH: 75.10 CPU 75.27 WC WATCH: 78.11 CPU 78.28 WC WATCH: 81.12 CPU 81.29 WC WATCH: 84.12 CPU 84.30 WC WATCH: 87.13 CPU 87.31 WC WATCH: 90.13 CPU 90.32 WC WATCH: 93.14 CPU 93.33 WC WATCH: 96.14 CPU 96.34 WC WATCH: 99.15 CPU 99.35 WC WATCH: 102.15 CPU 102.36 WC WATCH: 105.15 CPU 105.37 WC WATCH: 108.16 CPU 108.38 WC WATCH: 111.16 CPU 111.39 WC WATCH: 114.16 CPU 114.40 WC WATCH: 117.17 CPU 117.41 WC WATCH: 120.18 CPU 120.42 WC WATCH: 123.18 CPU 123.43 WC WATCH: 126.18 CPU 126.44 WC WATCH: 129.19 CPU 129.45 WC WATCH: 132.19 CPU 132.46 WC WATCH: 135.20 CPU 135.47 WC WATCH: 138.20 CPU 138.47 WC WATCH: 141.21 CPU 141.48 WC WATCH: 144.21 CPU 144.49 WC WATCH: 147.22 CPU 147.50 WC WATCH: 150.23 CPU 150.51 WC WATCH: 153.23 CPU 153.52 WC WATCH: 156.23 CPU 156.53 WC WATCH: 159.23 CPU 159.54 WC WATCH: 162.24 CPU 162.55 WC WATCH: 165.24 CPU 165.56 WC WATCH: 168.24 CPU 168.57 WC WATCH: 171.25 CPU 171.58 WC WATCH: 174.26 CPU 174.59 WC WATCH: 177.26 CPU 177.60 WC WATCH: 180.27 CPU 180.61 WC WATCH: 183.27 CPU 183.62 WC WATCH: 186.28 CPU 186.63 WC WATCH: 189.28 CPU 189.64 WC WATCH: 192.29 CPU 192.65 WC WATCH: 195.29 CPU 195.66 WC WATCH: 198.30 CPU 198.67 WC WATCH: 201.30 CPU 201.68 WC WATCH: 204.31 CPU 204.69 WC WATCH: 207.31 CPU 207.70 WC WATCH: 210.31 CPU 210.71 WC WATCH: 213.32 CPU 213.72 WC WATCH: 216.32 CPU 216.73 WC WATCH: 219.32 CPU 219.74 WC WATCH: 222.33 CPU 222.75 WC WATCH: 225.33 CPU 225.76 WC WATCH: 228.35 CPU 228.77 WC WATCH: 231.35 CPU 231.78 WC WATCH: 234.36 CPU 234.80 WC WATCH: 237.37 CPU 237.81 WC WATCH: 240.38 CPU 240.82 WC WATCH: 243.39 CPU 243.84 WC WATCH: 246.39 CPU 246.85 WC WATCH: 249.40 CPU 249.86 WC WATCH: 252.40 CPU 252.88 WC WATCH: 255.41 CPU 255.89 WC WATCH: 258.42 CPU 258.90 WC WATCH: 261.42 CPU 261.91 WC WATCH: 264.43 CPU 264.93 WC WATCH: 267.44 CPU 267.94 WC WATCH: 270.45 CPU 270.95 WC WATCH: 273.46 CPU 273.97 WC WATCH: 276.47 CPU 276.98 WC WATCH: 279.47 CPU 279.99 WC WATCH: 282.48 CPU 283.01 WC WATCH: 285.49 CPU 286.02 WC WATCH: 288.50 CPU 289.03 WC WATCH: 291.51 CPU 292.05 WC WATCH: 294.52 CPU 295.06 WC WATCH: 297.52 CPU 298.07 WC % SZS status Unknown Time Out Virtual ------ Statistics ------ General num_of_input_clauses: 30 num_of_input_neg_conjectures: 1 num_of_splits: 0 num_of_split_atoms: 0 forced_gc_time: 0 num_of_symbols: 26 num_of_terms: 113628 ------ Propositional Solver prop_solver_calls: 0 prop_fast_solver_calls: 0 prop_num_of_clauses: 80543 prop_preprocess_simplified: 24547 prop_fo_subsumed: 4237 prop_solver_time_sum: 0.00126194953918 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: 24587 inst_num_in_passive: 2 inst_num_in_active: 20347 inst_num_in_unprocessed: 1 inst_num_in_simple_passive: 0 inst_num_of_loops: 27981 inst_num_of_selection_renewals: 0 inst_num_of_learning_restarts: 0 inst_num_moves_active_passive: 3429 inst_lit_activity: 8258 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: 3758 inst_num_of_non_proper_insts: 24071 inst_num_of_duplicates: 0 inst_inst_num_from_inst_to_res: 0 ------ Resolution res_num_of_clauses: 27979 res_num_in_passive: 1 res_num_in_passive_sim: 0 res_num_in_active: 27978 res_num_of_loops: 28000 res_forward_subset_subsumed: 0 res_backward_subset_subsumed: 0 res_forward_subsumed: 9 res_backward_subsumed: 0 res_forward_subsumption_resolution: 0 res_backward_subsumption_resolution: 0 res_clause_to_clause_subsumption: 118543385 res_orphan_elimination: 0 res_tautology_del: 0 res_num_sel_changes: 15 res_moves_from_active_to_pass: 13 inst_dismatching_checking_time: 128.625137329 ------ 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: 23776 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: 300.27 CPU 300.84 WC FINAL WATCH: 300.27 CPU 300.84 WC