%---------------- iProver v0.9 (CASC-23 2011) ----------------% ------ Input Options --out_options all --tptp_safe_out false --problem_path "" --include_path "" --clausifier "" --clausifier_options "" --stdin false ------ General Options --fof false --time_out_real 300. --time_out_virtual -1. --schedule default --ground_splitting input --non_eq_to_eq false --prep_prop_sim true --symbol_type_check false --clausify_out false --large_theory_mode true --prep_sem_filter false --prep_sem_filter_out false --brand_transform false --prolific_symb_bound 500 --lt_threshold 2000 ------ SAT Options --sat_mode false --sat_gr_def false --sat_finite_models false --sat_out_model small ------ Instantiation Options --instantiation_flag true --inst_lit_sel [+sign;+ground;-num_var;-num_symb] --inst_solver_per_active 750 --inst_solver_per_clauses 5000 --inst_pass_queue1 [-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_learning_loop_flag true --inst_learning_start 3000 --inst_learning_factor 2 --inst_start_prop_sim_after_learn 3 --inst_sel_renew model --inst_lit_activity_flag true ------ 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_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. ------ Combination Options --comb_res_mult 300 --comb_inst_mult 1000 ------ ------ Parsing... WATCH: 0.00 CPU 0.01 WC ------ Clausification by vclausify_rel & Parsing by iProver... ------ Problem Properties EPR false Horn true Has equality true ------ Proving... ------ Schedule dynamic 5 is on ------ Input Options "--resolution_flag false" Time Limit: 10. ------ Input Options --out_options all --tptp_safe_out false --problem_path "" --include_path "" --clausifier "" --clausifier_options "" --stdin false ------ General Options --fof false --time_out_real 300. --time_out_virtual -1. --schedule default --ground_splitting input --non_eq_to_eq false --prep_prop_sim true --symbol_type_check false --clausify_out false --large_theory_mode true --prep_sem_filter false --prep_sem_filter_out false --brand_transform false --prolific_symb_bound 500 --lt_threshold 2000 ------ SAT Options --sat_mode false --sat_gr_def false --sat_finite_models false --sat_out_model small ------ Instantiation Options --instantiation_flag true --inst_lit_sel [+sign;+ground;-num_var;-num_symb] --inst_solver_per_active 750 --inst_solver_per_clauses 5000 --inst_pass_queue1 [-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_learning_loop_flag true --inst_learning_start 3000 --inst_learning_factor 2 --inst_start_prop_sim_after_learn 3 --inst_sel_renew model --inst_lit_activity_flag true ------ Resolution Options --resolution_flag false --res_lit_sel adaptive --res_to_prop_solver active --res_prop_simpl_new false --res_prop_simpl_given true --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. ------ Combination Options --comb_res_mult 300 --comb_inst_mult 1000 ------ ------ Proving... WATCH: 2.99 CPU 3.02 WC WATCH: 5.99 CPU 6.03 WC WATCH: 9.00 CPU 9.04 WC Time Out after: 8983 full_loop iterations ------ Input Options Time Limit: 25. ------ Input Options --out_options all --tptp_safe_out false --problem_path "" --include_path "" --clausifier "" --clausifier_options "" --stdin false ------ General Options --fof false --time_out_real 300. --time_out_virtual -1. --schedule default --ground_splitting input --non_eq_to_eq false --prep_prop_sim true --symbol_type_check false --clausify_out false --large_theory_mode true --prep_sem_filter false --prep_sem_filter_out false --brand_transform false --prolific_symb_bound 500 --lt_threshold 2000 ------ SAT Options --sat_mode false --sat_gr_def false --sat_finite_models false --sat_out_model small ------ Instantiation Options --instantiation_flag true --inst_lit_sel [+sign;+ground;-num_var;-num_symb] --inst_solver_per_active 750 --inst_solver_per_clauses 5000 --inst_pass_queue1 [-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_learning_loop_flag true --inst_learning_start 3000 --inst_learning_factor 2 --inst_start_prop_sim_after_learn 3 --inst_sel_renew model --inst_lit_activity_flag true ------ 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_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. ------ Combination Options --comb_res_mult 300 --comb_inst_mult 1000 ------ ------ Proving... WATCH: 12.00 CPU 12.05 WC WATCH: 15.01 CPU 15.06 WC WATCH: 18.01 CPU 18.07 WC WATCH: 21.02 CPU 21.08 WC WATCH: 24.02 CPU 24.09 WC WATCH: 27.02 CPU 27.10 WC WATCH: 30.02 CPU 30.11 WC WATCH: 33.04 CPU 33.12 WC Time Out after: 5383 full_loop iterations ------ Option_1: Negative Selections Time Limit: 15. ------ Input Options --out_options all --tptp_safe_out false --problem_path "" --include_path "" --clausifier "" --clausifier_options "" --stdin false ------ General Options --fof false --time_out_real -1. --time_out_virtual -1. --schedule default --ground_splitting input --non_eq_to_eq false --prep_prop_sim true --symbol_type_check false --clausify_out false --large_theory_mode true --prep_sem_filter false --prep_sem_filter_out false --brand_transform false --prolific_symb_bound 500 --lt_threshold 2000 ------ SAT Options --sat_mode false --sat_gr_def false --sat_finite_models false --sat_out_model small ------ Instantiation Options --instantiation_flag true --inst_lit_sel [-sign;-num_var;+num_symb] --inst_solver_per_active 750 --inst_solver_per_clauses 5000 --inst_pass_queue1 [-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_learning_loop_flag true --inst_learning_start 3000 --inst_learning_factor 2 --inst_start_prop_sim_after_learn 3 --inst_sel_renew model --inst_lit_activity_flag true ------ Resolution Options --resolution_flag true --res_lit_sel neg_max --res_to_prop_solver active --res_prop_simpl_new false --res_prop_simpl_given true --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 subset_subsumption --res_forward_subs_resolution true --res_backward_subs_resolution false --res_orphan_elimination false --res_time_limit 2. ------ Combination Options --comb_res_mult 300 --comb_inst_mult 1000 ------ ------ Proving... WATCH: 36.04 CPU 36.13 WC WATCH: 39.04 CPU 39.14 WC WATCH: 42.05 CPU 42.15 WC WATCH: 45.05 CPU 45.16 WC WATCH: 48.05 CPU 48.17 WC Time Out after: 9154 full_loop iterations ------ Option_2: Max Selections Time Limit: 15. ------ Input Options --out_options all --tptp_safe_out false --problem_path "" --include_path "" --clausifier "" --clausifier_options "" --stdin false ------ General Options --fof false --time_out_real -1. --time_out_virtual -1. --schedule default --ground_splitting input --non_eq_to_eq false --prep_prop_sim true --symbol_type_check false --clausify_out false --large_theory_mode true --prep_sem_filter false --prep_sem_filter_out false --brand_transform false --prolific_symb_bound 500 --lt_threshold 2000 ------ SAT Options --sat_mode false --sat_gr_def false --sat_finite_models false --sat_out_model small ------ Instantiation Options --instantiation_flag true --inst_lit_sel [-sign;-num_var;-num_symb] --inst_solver_per_active 750 --inst_solver_per_clauses 5000 --inst_pass_queue1 [-num_symb;-num_var;-conj_dist;+conj_symb] --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_learning_loop_flag true --inst_learning_start 3000 --inst_learning_factor 2 --inst_start_prop_sim_after_learn 3 --inst_sel_renew model --inst_lit_activity_flag true ------ Resolution Options --resolution_flag true --res_lit_sel kbo_max --res_to_prop_solver active --res_prop_simpl_new false --res_prop_simpl_given true --res_passive_queue_flag true --res_pass_queue1 [-num_symb;+conj_symb] --res_pass_queue2 [+age;-num_symb] --res_pass_queue1_mult 15 --res_pass_queue2_mult 5 --res_forward_subs full --res_backward_subs subset_subsumption --res_forward_subs_resolution true --res_backward_subs_resolution false --res_orphan_elimination false --res_time_limit 2. ------ Combination Options --comb_res_mult 300 --comb_inst_mult 1000 ------ ------ Proving... WATCH: 51.06 CPU 51.18 WC WATCH: 54.06 CPU 54.19 WC WATCH: 57.07 CPU 57.20 WC WATCH: 60.07 CPU 60.21 WC WATCH: 63.07 CPU 63.22 WC Time Out after: 13309 full_loop iterations ------ Option_3: Min Selections Time Limit: 15. ------ Input Options --out_options all --tptp_safe_out false --problem_path "" --include_path "" --clausifier "" --clausifier_options "" --stdin false ------ General Options --fof false --time_out_real -1. --time_out_virtual -1. --schedule default --ground_splitting input --non_eq_to_eq false --prep_prop_sim true --symbol_type_check false --clausify_out false --large_theory_mode true --prep_sem_filter false --prep_sem_filter_out false --brand_transform false --prolific_symb_bound 500 --lt_threshold 2000 ------ SAT Options --sat_mode false --sat_gr_def false --sat_finite_models false --sat_out_model small ------ Instantiation Options --instantiation_flag true --inst_lit_sel [-sign;-num_symb] --inst_solver_per_active 750 --inst_solver_per_clauses 5000 --inst_pass_queue1 [-num_symb;-conj_dist;+conj_symb] --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_learning_loop_flag true --inst_learning_start 3000 --inst_learning_factor 2 --inst_start_prop_sim_after_learn 3 --inst_sel_renew model --inst_lit_activity_flag true ------ Resolution Options --resolution_flag true --res_lit_sel neg_min --res_to_prop_solver active --res_prop_simpl_new false --res_prop_simpl_given true --res_passive_queue_flag true --res_pass_queue1 [-num_symb;+conj_symb] --res_pass_queue2 [+age;-num_symb] --res_pass_queue1_mult 15 --res_pass_queue2_mult 5 --res_forward_subs full --res_backward_subs subset_subsumption --res_forward_subs_resolution true --res_backward_subs_resolution false --res_orphan_elimination false --res_time_limit 2. ------ Combination Options --comb_res_mult 300 --comb_inst_mult 1000 ------ ------ Proving... WATCH: 66.08 CPU 66.23 WC WATCH: 69.09 CPU 69.24 WC WATCH: 72.09 CPU 72.25 WC WATCH: 75.10 CPU 75.26 WC WATCH: 78.10 CPU 78.27 WC Time Out after: 14102 full_loop iterations ------ Input Options Time Limit: Unbounded ------ Input Options --out_options all --tptp_safe_out false --problem_path "" --include_path "" --clausifier "" --clausifier_options "" --stdin false ------ General Options --fof false --time_out_real 300. --time_out_virtual -1. --schedule default --ground_splitting input --non_eq_to_eq false --prep_prop_sim true --symbol_type_check false --clausify_out false --large_theory_mode true --prep_sem_filter false --prep_sem_filter_out false --brand_transform false --prolific_symb_bound 500 --lt_threshold 2000 ------ SAT Options --sat_mode false --sat_gr_def false --sat_finite_models false --sat_out_model small ------ Instantiation Options --instantiation_flag true --inst_lit_sel [+sign;+ground;-num_var;-num_symb] --inst_solver_per_active 750 --inst_solver_per_clauses 5000 --inst_pass_queue1 [-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_learning_loop_flag true --inst_learning_start 3000 --inst_learning_factor 2 --inst_start_prop_sim_after_learn 3 --inst_sel_renew model --inst_lit_activity_flag true ------ 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_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. ------ Combination Options --comb_res_mult 300 --comb_inst_mult 1000 ------ ------ Proving... WATCH: 81.11 CPU 81.28 WC WATCH: 84.12 CPU 84.30 WC WATCH: 87.13 CPU 87.31 WC WATCH: 90.14 CPU 90.33 WC WATCH: 93.15 CPU 93.34 WC WATCH: 96.16 CPU 96.36 WC WATCH: 99.16 CPU 99.37 WC WATCH: 102.17 CPU 102.38 WC WATCH: 105.18 CPU 105.40 WC WATCH: 108.19 CPU 108.41 WC WATCH: 111.20 CPU 111.42 WC WATCH: 114.20 CPU 114.43 WC WATCH: 117.21 CPU 117.44 WC WATCH: 120.22 CPU 120.46 WC WATCH: 123.22 CPU 123.47 WC WATCH: 126.23 CPU 126.48 WC WATCH: 129.23 CPU 129.49 WC WATCH: 132.24 CPU 132.50 WC WATCH: 135.24 CPU 135.51 WC WATCH: 138.25 CPU 138.52 WC WATCH: 141.25 CPU 141.53 WC WATCH: 144.26 CPU 144.54 WC WATCH: 147.27 CPU 147.55 WC WATCH: 150.27 CPU 150.56 WC WATCH: 153.27 CPU 153.57 WC WATCH: 156.28 CPU 156.58 WC WATCH: 159.29 CPU 159.59 WC WATCH: 162.29 CPU 162.60 WC WATCH: 165.29 CPU 165.61 WC WATCH: 168.29 CPU 168.62 WC WATCH: 171.31 CPU 171.64 WC WATCH: 174.31 CPU 174.65 WC WATCH: 177.31 CPU 177.66 WC WATCH: 180.32 CPU 180.67 WC WATCH: 183.32 CPU 183.68 WC WATCH: 186.33 CPU 186.69 WC WATCH: 189.33 CPU 189.70 WC WATCH: 192.34 CPU 192.71 WC WATCH: 195.35 CPU 195.72 WC WATCH: 198.35 CPU 198.73 WC WATCH: 201.36 CPU 201.74 WC WATCH: 204.36 CPU 204.75 WC WATCH: 207.37 CPU 207.76 WC WATCH: 210.38 CPU 210.77 WC WATCH: 213.38 CPU 213.78 WC WATCH: 216.38 CPU 216.79 WC WATCH: 219.39 CPU 219.80 WC WATCH: 222.39 CPU 222.81 WC WATCH: 225.40 CPU 225.82 WC WATCH: 228.40 CPU 228.83 WC WATCH: 231.41 CPU 231.84 WC WATCH: 234.41 CPU 234.85 WC WATCH: 237.42 CPU 237.86 WC WATCH: 240.42 CPU 240.87 WC WATCH: 243.42 CPU 243.88 WC WATCH: 246.43 CPU 246.89 WC WATCH: 249.44 CPU 249.90 WC WATCH: 252.44 CPU 252.91 WC WATCH: 255.45 CPU 255.92 WC WATCH: 258.45 CPU 258.93 WC WATCH: 261.46 CPU 261.94 WC WATCH: 264.46 CPU 264.95 WC WATCH: 267.47 CPU 267.96 WC WATCH: 270.47 CPU 270.98 WC WATCH: 273.48 CPU 273.99 WC WATCH: 276.49 CPU 277.00 WC WATCH: 279.50 CPU 280.01 WC WATCH: 282.50 CPU 283.02 WC WATCH: 285.50 CPU 286.03 WC WATCH: 288.51 CPU 289.04 WC WATCH: 291.52 CPU 292.05 WC WATCH: 294.52 CPU 295.06 WC WATCH: 297.52 CPU 298.07 WC % SZS status Unknown Time Out Real ------ Statistics ------ General num_of_input_clauses: 20 num_of_input_neg_conjectures: 3 num_of_splits: 0 num_of_split_atoms: 0 forced_gc_time: 0 total_time: 300.724 parsing_time: 0.017 num_of_symbols: 34 num_of_terms: 2441942 ------ Propositional Solver prop_solver_calls: 237 prop_fast_solver_calls: 795456 prop_num_of_clauses: 468834 prop_preprocess_simplified: 988358 prop_fo_subsumed: 300910 prop_solver_time: 1.205 prop_fast_solver_time: 10.786 ------ Instantiation inst_num_of_clauses: 201498 inst_num_in_passive: 36595 inst_num_in_active: 5941 inst_num_in_unprocessed: 95 inst_num_in_simple_passive: 0 inst_num_of_loops: 5998 inst_num_of_learning_restarts: 9 inst_num_moves_active_passive: 30 inst_lit_activity: 3165 inst_lit_activity_moves: 1 inst_num_tautologies: 19 inst_num_prop_implied: 0 inst_num_existing_simplified: 140994 inst_num_child_elim: 0 inst_num_of_dismatching_blockings: 12566 inst_num_of_non_proper_insts: 174321 inst_num_of_duplicates: 34959 inst_inst_num_from_inst_to_res: 0 inst_dismatching_checking_time: 11.61 ------ Resolution res_num_of_clauses: 1034907 res_num_in_passive: 1030761 res_num_in_passive_sim: 0 res_num_in_active: 4144 res_num_of_loops: 4719 res_forward_subset_subsumed: 35532 res_backward_subset_subsumed: 0 res_forward_subsumed: 211 res_backward_subsumed: 65 res_forward_subsumption_resolution: 7 res_backward_subsumption_resolution: 0 res_clause_to_clause_subsumption: 101099 res_orphan_elimination: 54 res_tautology_del: 173 res_num_sel_changes: 5246 res_moves_from_active_to_pass: 43 WATCH: 300.25 CPU 300.81 WC FINAL WATCH: 300.25 CPU 300.81 WC