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 true ------ Proving... WATCH: 2.97 CPU 3.02 WC WATCH: 5.97 CPU 6.03 WC WATCH: 8.98 CPU 9.04 WC WATCH: 11.98 CPU 12.05 WC WATCH: 14.98 CPU 15.06 WC WATCH: 17.99 CPU 18.07 WC WATCH: 20.99 CPU 21.08 WC WATCH: 24.00 CPU 24.08 WC WATCH: 27.01 CPU 27.09 WC WATCH: 30.01 CPU 30.10 WC WATCH: 33.01 CPU 33.11 WC WATCH: 36.02 CPU 36.12 WC WATCH: 39.02 CPU 39.13 WC WATCH: 42.03 CPU 42.14 WC WATCH: 45.04 CPU 45.15 WC WATCH: 48.03 CPU 48.16 WC WATCH: 51.04 CPU 51.17 WC WATCH: 54.04 CPU 54.18 WC WATCH: 57.05 CPU 57.19 WC WATCH: 60.05 CPU 60.20 WC WATCH: 63.05 CPU 63.21 WC WATCH: 66.06 CPU 66.22 WC WATCH: 69.07 CPU 69.23 WC WATCH: 72.07 CPU 72.24 WC WATCH: 75.08 CPU 75.25 WC WATCH: 78.09 CPU 78.27 WC WATCH: 81.09 CPU 81.28 WC WATCH: 84.09 CPU 84.29 WC WATCH: 87.10 CPU 87.30 WC WATCH: 90.11 CPU 90.31 WC WATCH: 93.11 CPU 93.32 WC WATCH: 96.12 CPU 96.33 WC WATCH: 99.12 CPU 99.34 WC WATCH: 102.13 CPU 102.35 WC WATCH: 105.13 CPU 105.35 WC WATCH: 108.13 CPU 108.36 WC WATCH: 111.14 CPU 111.37 WC WATCH: 114.14 CPU 114.38 WC WATCH: 117.15 CPU 117.39 WC WATCH: 120.15 CPU 120.40 WC WATCH: 123.15 CPU 123.41 WC WATCH: 126.16 CPU 126.42 WC WATCH: 129.17 CPU 129.43 WC WATCH: 132.17 CPU 132.44 WC WATCH: 135.17 CPU 135.45 WC WATCH: 138.18 CPU 138.46 WC WATCH: 141.18 CPU 141.47 WC WATCH: 144.19 CPU 144.48 WC WATCH: 147.19 CPU 147.49 WC WATCH: 150.20 CPU 150.50 WC WATCH: 153.21 CPU 153.51 WC WATCH: 156.21 CPU 156.52 WC WATCH: 159.21 CPU 159.53 WC WATCH: 162.22 CPU 162.54 WC WATCH: 165.22 CPU 165.55 WC WATCH: 168.23 CPU 168.56 WC WATCH: 171.23 CPU 171.57 WC WATCH: 174.24 CPU 174.58 WC WATCH: 177.24 CPU 177.59 WC WATCH: 180.25 CPU 180.60 WC WATCH: 183.25 CPU 183.61 WC WATCH: 186.26 CPU 186.62 WC WATCH: 189.26 CPU 189.63 WC WATCH: 192.26 CPU 192.64 WC WATCH: 195.27 CPU 195.65 WC WATCH: 198.27 CPU 198.66 WC WATCH: 201.28 CPU 201.67 WC WATCH: 204.28 CPU 204.68 WC WATCH: 207.28 CPU 207.69 WC WATCH: 210.29 CPU 210.70 WC WATCH: 213.29 CPU 213.71 WC WATCH: 216.30 CPU 216.72 WC WATCH: 219.30 CPU 219.73 WC WATCH: 222.31 CPU 222.74 WC WATCH: 225.31 CPU 225.74 WC WATCH: 228.31 CPU 228.75 WC WATCH: 231.32 CPU 231.76 WC WATCH: 234.33 CPU 234.77 WC WATCH: 237.33 CPU 237.78 WC WATCH: 240.34 CPU 240.79 WC WATCH: 243.34 CPU 243.80 WC WATCH: 246.35 CPU 246.81 WC WATCH: 249.35 CPU 249.82 WC WATCH: 252.36 CPU 252.83 WC WATCH: 255.35 CPU 255.84 WC WATCH: 258.36 CPU 258.85 WC WATCH: 261.36 CPU 261.86 WC WATCH: 264.37 CPU 264.87 WC WATCH: 267.37 CPU 267.88 WC WATCH: 270.37 CPU 270.89 WC WATCH: 273.38 CPU 273.90 WC WATCH: 276.38 CPU 276.91 WC WATCH: 279.39 CPU 279.92 WC WATCH: 282.40 CPU 282.94 WC WATCH: 285.41 CPU 285.95 WC WATCH: 288.42 CPU 288.96 WC WATCH: 291.42 CPU 291.97 WC WATCH: 294.43 CPU 294.98 WC WATCH: 297.43 CPU 297.99 WC WATCH: 300.44 CPU 301.00 WC FINAL WATCH: 300.44 CPU 301.18 WC