%---------------- 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 false ------ 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... % SZS status Theorem ------ Statistics ------ General num_of_input_clauses: 5 num_of_input_neg_conjectures: 5 num_of_splits: 0 num_of_split_atoms: 0 forced_gc_time: 0 total_time: 0.053 parsing_time: 0.006 num_of_symbols: 28 num_of_terms: 2102 ------ Propositional Solver prop_solver_calls: 5 prop_fast_solver_calls: 7 prop_num_of_clauses: 388 prop_preprocess_simplified: 62 prop_fo_subsumed: 0 prop_solver_time: 0. prop_fast_solver_time: 0. ------ Instantiation inst_num_of_clauses: 226 inst_num_in_passive: 154 inst_num_in_active: 50 inst_num_in_unprocessed: 20 inst_num_in_simple_passive: 0 inst_num_of_loops: 58 inst_num_of_learning_restarts: 0 inst_num_moves_active_passive: 2 inst_lit_activity: 51 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: 64 inst_num_of_non_proper_insts: 108 inst_num_of_duplicates: 54 inst_inst_num_from_inst_to_res: 0 inst_dismatching_checking_time: 0. ------ Resolution res_num_of_clauses: undef res_num_in_passive: undef res_num_in_passive_sim: 0 res_num_in_active: 0 res_num_of_loops: 0 res_forward_subset_subsumed: 0 res_backward_subset_subsumed: 0 res_forward_subsumed: 0 res_backward_subsumed: 0 res_forward_subsumption_resolution: 0 res_backward_subsumption_resolution: 0 res_clause_to_clause_subsumption: 0 res_orphan_elimination: 0 res_tautology_del: 0 res_num_sel_changes: 0 res_moves_from_active_to_pass: 0 WATCH: 0.03 CPU 0.07 WC FINAL WATCH: 0.03 CPU 0.07 WC