%---------------- 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 true Horn true Has equality false ------ Proving... ------ Option_epr_horn 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 -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;+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 5 --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 solver --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 [-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 subset_subsumption --res_backward_subs subset_subsumption --res_forward_subs_resolution false --res_backward_subs_resolution false --res_orphan_elimination false --res_time_limit 2. ------ Combination Options --comb_res_mult 1000 --comb_inst_mult 300 ------ ------ Proving... WATCH: 2.99 CPU 3.02 WC WATCH: 5.99 CPU 6.03 WC WATCH: 9.00 CPU 9.04 WC WATCH: 12.00 CPU 12.05 WC WATCH: 15.00 CPU 15.06 WC WATCH: 18.02 CPU 18.08 WC WATCH: 21.02 CPU 21.09 WC WATCH: 24.03 CPU 24.10 WC WATCH: 27.04 CPU 27.12 WC WATCH: 30.04 CPU 30.13 WC WATCH: 33.05 CPU 33.14 WC WATCH: 36.06 CPU 36.15 WC WATCH: 39.07 CPU 39.17 WC WATCH: 42.08 CPU 42.18 WC WATCH: 45.09 CPU 45.20 WC WATCH: 48.10 CPU 48.21 WC WATCH: 51.10 CPU 51.22 WC WATCH: 54.11 CPU 54.23 WC WATCH: 57.12 CPU 57.25 WC WATCH: 60.13 CPU 60.26 WC WATCH: 63.14 CPU 63.28 WC WATCH: 66.16 CPU 66.30 WC WATCH: 69.16 CPU 69.31 WC WATCH: 72.18 CPU 72.33 WC WATCH: 75.19 CPU 75.34 WC WATCH: 78.20 CPU 78.36 WC WATCH: 81.21 CPU 81.38 WC WATCH: 84.22 CPU 84.39 WC WATCH: 87.23 CPU 87.41 WC WATCH: 90.24 CPU 90.43 WC WATCH: 93.25 CPU 93.44 WC WATCH: 96.27 CPU 96.46 WC WATCH: 99.27 CPU 99.48 WC WATCH: 102.28 CPU 102.49 WC WATCH: 105.29 CPU 105.51 WC WATCH: 108.31 CPU 108.53 WC WATCH: 111.32 CPU 111.54 WC WATCH: 114.33 CPU 114.56 WC WATCH: 117.34 CPU 117.57 WC WATCH: 120.35 CPU 120.59 WC WATCH: 123.36 CPU 123.61 WC WATCH: 126.37 CPU 126.62 WC WATCH: 129.39 CPU 129.64 WC WATCH: 132.40 CPU 132.66 WC WATCH: 135.41 CPU 135.67 WC WATCH: 138.42 CPU 138.69 WC WATCH: 141.43 CPU 141.71 WC WATCH: 144.44 CPU 144.72 WC WATCH: 147.46 CPU 147.74 WC WATCH: 150.46 CPU 150.76 WC WATCH: 153.48 CPU 153.77 WC WATCH: 156.48 CPU 156.79 WC WATCH: 159.49 CPU 159.80 WC WATCH: 162.51 CPU 162.82 WC WATCH: 165.52 CPU 165.84 WC WATCH: 168.53 CPU 168.85 WC WATCH: 171.55 CPU 171.87 WC WATCH: 174.56 CPU 174.89 WC WATCH: 177.57 CPU 177.90 WC WATCH: 180.57 CPU 180.92 WC WATCH: 183.59 CPU 183.94 WC WATCH: 186.60 CPU 186.95 WC WATCH: 189.61 CPU 189.96 WC WATCH: 192.61 CPU 192.97 WC WATCH: 195.62 CPU 195.99 WC WATCH: 198.63 CPU 199.00 WC WATCH: 201.63 CPU 202.01 WC WATCH: 204.64 CPU 205.02 WC WATCH: 207.63 CPU 208.03 WC WATCH: 210.64 CPU 211.04 WC WATCH: 213.64 CPU 214.05 WC WATCH: 216.65 CPU 217.06 WC WATCH: 219.66 CPU 220.07 WC WATCH: 222.66 CPU 223.08 WC WATCH: 225.67 CPU 226.09 WC WATCH: 228.67 CPU 229.10 WC WATCH: 231.68 CPU 232.11 WC WATCH: 234.69 CPU 235.12 WC WATCH: 237.69 CPU 238.13 WC WATCH: 240.70 CPU 241.15 WC WATCH: 243.71 CPU 244.16 WC WATCH: 246.71 CPU 247.17 WC WATCH: 249.72 CPU 250.19 WC WATCH: 252.73 CPU 253.20 WC WATCH: 255.74 CPU 256.21 WC WATCH: 258.75 CPU 259.22 WC WATCH: 261.75 CPU 262.24 WC WATCH: 264.76 CPU 265.25 WC WATCH: 267.76 CPU 268.26 WC WATCH: 270.77 CPU 271.28 WC WATCH: 273.78 CPU 274.29 WC WATCH: 276.79 CPU 277.30 WC WATCH: 279.80 CPU 280.32 WC WATCH: 282.81 CPU 283.33 WC WATCH: 285.81 CPU 286.34 WC WATCH: 288.82 CPU 289.36 WC WATCH: 291.83 CPU 292.37 WC WATCH: 294.84 CPU 295.38 WC WATCH: 297.85 CPU 298.39 WC % SZS status Unknown Time Out Real ------ 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 total_time: 300.103 parsing_time: 0.02 num_of_symbols: 28 num_of_terms: 260508 ------ Propositional Solver prop_solver_calls: 97 prop_fast_solver_calls: 255162 prop_num_of_clauses: 279153 prop_preprocess_simplified: 247925 prop_fo_subsumed: 15600 prop_solver_time: 0.113 prop_fast_solver_time: 1.735 ------ Instantiation inst_num_of_clauses: 18596 inst_num_in_passive: 1 inst_num_in_active: 9312 inst_num_in_unprocessed: 0 inst_num_in_simple_passive: 0 inst_num_of_loops: 18596 inst_num_of_learning_restarts: 4 inst_num_moves_active_passive: 0 inst_lit_activity: 4642 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: 9 inst_num_of_non_proper_insts: 9283 inst_num_of_duplicates: 0 inst_inst_num_from_inst_to_res: 0 inst_dismatching_checking_time: 116.59 ------ Resolution res_num_of_clauses: 212514 res_num_in_passive: 1 res_num_in_passive_sim: 0 res_num_in_active: 212513 res_num_of_loops: 212513 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: 299.61 CPU 300.17 WC FINAL WATCH: 299.61 CPU 300.17 WC