%---------------- iProver v0.9 (CASC-23 2011) ----------------% WATCH: 0.00 CPU 0.01 WC ------ 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... ------ 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.98 CPU 3.02 WC WATCH: 5.98 CPU 6.03 WC WATCH: 8.99 CPU 9.04 WC Time Out after: 13001 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: 11.99 CPU 12.05 WC WATCH: 15.00 CPU 15.06 WC WATCH: 18.00 CPU 18.07 WC WATCH: 21.00 CPU 21.07 WC WATCH: 24.01 CPU 24.08 WC WATCH: 27.01 CPU 27.09 WC WATCH: 30.01 CPU 30.10 WC WATCH: 33.02 CPU 33.11 WC Time Out after: 17150 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.02 CPU 36.12 WC WATCH: 39.03 CPU 39.13 WC WATCH: 42.03 CPU 42.14 WC WATCH: 45.04 CPU 45.15 WC WATCH: 48.05 CPU 48.16 WC Time Out after: 10552 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.05 CPU 51.17 WC WATCH: 54.06 CPU 54.18 WC WATCH: 57.06 CPU 57.19 WC WATCH: 60.06 CPU 60.20 WC WATCH: 63.07 CPU 63.21 WC Time Out after: 11250 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.07 CPU 66.22 WC WATCH: 69.08 CPU 69.23 WC WATCH: 72.09 CPU 72.25 WC WATCH: 75.09 CPU 75.26 WC WATCH: 78.09 CPU 78.27 WC Time Out after: 11278 full_loop iterations WATCH: 81.10 CPU 81.28 WC ------ 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: 84.11 CPU 84.29 WC WATCH: 87.11 CPU 87.30 WC WATCH: 90.12 CPU 90.31 WC WATCH: 93.12 CPU 93.32 WC WATCH: 96.13 CPU 96.33 WC WATCH: 99.13 CPU 99.33 WC WATCH: 102.14 CPU 102.34 WC WATCH: 105.14 CPU 105.35 WC WATCH: 108.14 CPU 108.36 WC WATCH: 111.14 CPU 111.37 WC WATCH: 114.15 CPU 114.38 WC WATCH: 117.15 CPU 117.39 WC WATCH: 120.16 CPU 120.40 WC WATCH: 123.16 CPU 123.41 WC WATCH: 126.17 CPU 126.42 WC WATCH: 129.18 CPU 129.43 WC WATCH: 132.18 CPU 132.44 WC WATCH: 135.18 CPU 135.45 WC WATCH: 138.18 CPU 138.46 WC WATCH: 141.19 CPU 141.47 WC WATCH: 144.20 CPU 144.48 WC WATCH: 147.20 CPU 147.49 WC WATCH: 150.20 CPU 150.50 WC ------ Switching off resolution: loop timeout WATCH: 153.21 CPU 153.51 WC WATCH: 156.21 CPU 156.52 WC WATCH: 159.22 CPU 159.53 WC WATCH: 162.22 CPU 162.54 WC WATCH: 165.23 CPU 165.55 WC WATCH: 168.23 CPU 168.56 WC WATCH: 171.24 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.28 CPU 198.66 WC WATCH: 201.28 CPU 201.67 WC WATCH: 204.29 CPU 204.68 WC WATCH: 207.29 CPU 207.69 WC WATCH: 210.29 CPU 210.70 WC WATCH: 213.29 CPU 213.71 WC WATCH: 216.31 CPU 216.71 WC WATCH: 219.31 CPU 219.73 WC WATCH: 222.32 CPU 222.74 WC WATCH: 225.32 CPU 225.75 WC WATCH: 228.34 CPU 228.77 WC WATCH: 231.35 CPU 231.78 WC WATCH: 234.35 CPU 234.79 WC WATCH: 237.36 CPU 237.81 WC WATCH: 240.37 CPU 240.82 WC WATCH: 243.38 CPU 243.83 WC WATCH: 246.38 CPU 246.85 WC WATCH: 249.39 CPU 249.86 WC WATCH: 252.40 CPU 252.87 WC WATCH: 255.41 CPU 255.88 WC WATCH: 258.41 CPU 258.90 WC WATCH: 261.42 CPU 261.91 WC WATCH: 264.43 CPU 264.92 WC WATCH: 267.43 CPU 267.93 WC WATCH: 270.44 CPU 270.94 WC WATCH: 273.44 CPU 273.95 WC WATCH: 276.45 CPU 276.96 WC WATCH: 279.45 CPU 279.97 WC WATCH: 282.46 CPU 282.98 WC WATCH: 285.46 CPU 285.99 WC WATCH: 288.47 CPU 289.00 WC WATCH: 291.47 CPU 292.01 WC WATCH: 294.48 CPU 295.02 WC WATCH: 297.48 CPU 298.03 WC % SZS status Unknown Time Out Real ------ 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 total_time: 300.776 parsing_time: 0.022 num_of_symbols: 31 num_of_terms: 3021190 ------ Propositional Solver prop_solver_calls: 643 prop_fast_solver_calls: 1319258 prop_num_of_clauses: 823421 prop_preprocess_simplified: 785097 prop_fo_subsumed: 231509 prop_solver_time: 14.835 prop_fast_solver_time: 37.488 ------ Instantiation inst_num_of_clauses: 212672 inst_num_in_passive: 132099 inst_num_in_active: 20679 inst_num_in_unprocessed: 1528 inst_num_in_simple_passive: 0 inst_num_of_loops: 22795 inst_num_of_learning_restarts: 10 inst_num_moves_active_passive: 2024 inst_lit_activity: 8061 inst_lit_activity_moves: 17 inst_num_tautologies: 85 inst_num_prop_implied: 0 inst_num_existing_simplified: 9137 inst_num_child_elim: 0 inst_num_of_dismatching_blockings: 737587 inst_num_of_non_proper_insts: 214429 inst_num_of_duplicates: 178949 inst_inst_num_from_inst_to_res: 0 inst_dismatching_checking_time: 17.297 ------ Resolution res_num_of_clauses: 376726 res_num_in_passive: 373565 res_num_in_passive_sim: 0 res_num_in_active: 3154 res_num_of_loops: 6519 res_forward_subset_subsumed: 61052 res_backward_subset_subsumed: 0 res_forward_subsumed: 3142 res_backward_subsumed: 153 res_forward_subsumption_resolution: 6 res_backward_subsumption_resolution: 0 res_clause_to_clause_subsumption: 106496 res_orphan_elimination: 57 res_tautology_del: 200 res_num_sel_changes: 1674 res_moves_from_active_to_pass: 4 WATCH: 300.29 CPU 300.86 WC FINAL WATCH: 300.29 CPU 300.86 WC