%------------------------------------------------------------------------------ % File : iProver-Eq---0.85 % Problem : CSR044+3 : TPTP v5.5.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : iprover-cvc4-eq-nc --time_out_virtual %d %s % Computer : art05.cs.miami.edu % Model : i686 i686 % CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz % Memory : 2005MB % OS : Linux 2.6.32.26-175.fc12.i686.PAE % CPULimit : 300s % DateTime : Tue Jun 4 10:53:08 EDT 2013 % Result : Theorem 12.14s % Output : Assurance 12.14s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----NO SOLUTION OUTPUT BY SYSTEM %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % ---------------- iProver-Eq CASC-J6 --------------- % % % ------ 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_z3_max_conflicts 0 % --prop_find_incons_bsearch true % --prop_gnd_by_bot false % --prop_undo_non_eq_to_eq true % --time_out_real 0. % --time_out_virtual 300. % --schedule eq_labels % --non_eq_to_eq true % --symbol_type_check false % --sub_typing true % --gnd_solver auto % --sim_gnd_solver_rlimit 1 % --sim_gnd_solver SMT % --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 none % % ------ 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 true % --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;+ground;-num_var;-num_symb] % --up_pass_queue2 [+age;-num_symb] % --up_pass_queue1_mult 20 % --up_pass_queue2_mult 10 % --up_pass_demod_queue1 [+ground;+orient;-num_var;-num_symb] % --up_pass_demod_queue2 [+age;-num_symb] % --up_pass_demod_queue1_mult 20 % --up_pass_demod_queue2_mult 10 % --up_orient_after_subst true % --up_superposition true % --up_inference_type_check true % --up_use_demod true % --up_demod_inst_eager false % --up_demod_inst_to_solver_only false % --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_from_inst true % --up_demod_inst_clauses false % --up_unit_not_neg false % --up_pure_lit_proof true % --up_dism_for_unit_literals true % --up_dism_inherit true % --up_dism_check_equation true % --up_dism_check_demod 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 0 % --up_unselect_var_eq false % --up_instantiate_var_eq false % % ------ Combination Options % % --comb_res_mult 100 % --comb_inst_mult 100 % --comb_up_mult 100 % --comb_demod_mult 100 % --comb_superpos_mult 10 % ------ % % ------ Parsing... % ------ Clausification by vclausify_rel & Parsing by iProver... % % ------ Non-equational problem: switching off unit paramodulation, using only instantiation. % % ------ Non-equational problem: not translating non-equational predicates. % % ------ Omitting equality axioms % % ------ Problem Properties % % % EPR false % Horn true % Has equality false % Unit equational false % % ------ Proving... % % ------ Tree labels with BDD subsumption check Input Options Time limit: 20.00 % ------ Proving ... % % % % SZS status Theorem % % SatSolverExchange.add_clause: SAT solver returned unsatisfiable. % % % ------ Statistics % % ------ General % % num_of_input_clauses: 7288 % num_of_input_neg_conjectures: 2 % num_of_splits: 0 % num_of_split_atoms: 0 % num_of_subtypes: 131 % forced_gc_time: 0 % num_of_symbols: 4599 % num_of_terms: 80019 % debug_timer: 0. % % ------ Propositional Solver % % prop_solver_calls: 28 % prop_fast_solver_calls: 21130 % prop_aborted_fast_solver_calls: undef % % prop_num_of_clauses: 19650 % prop_preprocess_simplified: 17106 % prop_fo_subsumed: 88 % prop_solver_time_sum: 0. % prop_solver_time_add_clause: 0. % prop_solver_time_lit_val: 0. % prop_solver_time_solve: 0.021 % prop_solver_time_solve_sat: 0. % prop_solver_time_solve_assumptions: 0.002 % prop_solver_time_fast_solve: 0.07 % prop_solver_time_find_consistent_assumptions: 0. % check_constr_norm_list_time: 0. % % ------ Instantiation % % inst_num_of_clauses: 8243 % inst_num_in_passive: 2164 % inst_num_in_active: 14839 % inst_num_in_unprocessed: 190 % inst_num_in_simple_passive: 0 % inst_num_of_loops: 14898 % inst_num_passive_empty: 3 % inst_num_of_selection_renewals: 0 % inst_num_of_learning_restarts: 2 % inst_num_of_forced_restarts: 0 % inst_num_moves_active_passive: 56 % inst_lit_activity: 202 % inst_lit_activity_moves: 1 % inst_num_tautologies: 0 % inst_num_prop_implied: 0 % inst_num_existing_simplified: 0 % inst_num_child_elim: 0 % inst_num_of_dismatching_blockings: 380 % inst_num_of_non_proper_insts: 4900 % inst_num_of_duplicates: 0 % inst_inst_num_from_inst_to_res: 0 % % ------ Resolution % % res_num_of_clauses: 16725 % res_num_in_passive: 3788 % res_num_in_passive_sim: 0 % res_num_in_active: 12936 % res_num_of_loops: 14964 % res_forward_subset_subsumed: 6199 % res_backward_subset_subsumed: 0 % res_forward_subsumed: 400 % res_backward_subsumed: 219 % res_forward_subsumption_resolution: 67 % res_backward_subsumption_resolution: 221 % res_clause_to_clause_subsumption: 89193 % res_orphan_elimination: 0 % res_tautology_del: 214 % res_num_sel_changes: 1908 % res_moves_from_active_to_pass: 1179 % inst_dismatching_checking_time: 0.012802362442 % % ------ Unit Paramodulation % % up_num_in_passive: 0 % up_num_in_passive_demodulators: 0 % up_num_of_literals: 0 % up_closures_in_bdd_labels: 0 % up_nodes_in_bdd_labels: 2 % up_labels_htree_table_len: undef % up_labels_htree_num_entries: undef % up_num_of_loops: 0 % up_num_passive_empty: 0 % up_num_in_active: 0 % up_num_in_active_demodulators: 0 % up_num_in_unprocessed: 14895 % up_num_in_omitted_clauses: 0 % up_sel_not_oriented: 0 % up_eliminated_active_passive_inter: 0 % up_eliminated_closures_in_label: 0 % up_dismatched_literals: 0 % up_clauses_demodulated: 0 % up_given_demodulated: 0 % up_active_demodulated: 0 % up_conclusions_demodulated: 0 % up_demodulators_demodulated: 0 % up_input_demodulated: 0 % up_demod_orient_after_subst: 0 % up_demod_inst_eager: 0 % up_unit_inst_eager: 0 % up_given_simpl_after_demod_clauses: 0 % up_active_simpl_after_demod_clauses: 0 % up_inferences: 0 % up_inference_types_blocked: 0 % up_inferences_unit_lit: 0 % up_dismatched_inferences: 0 % up_dismatched_unit_premises: 0 % up_eq_orient_after_subst: 0 % up_lit_orient_after_subst: 0 % up_tautologies: 0 % up_inference_label_subsumed: 0 % up_cycles: 0 % up_contradictions: 0 % up_gnd_lemmas: 0 % up_proof_size_0: 0 % up_proof_size_1: 0 % up_proof_size_2: 0 % up_proof_size_3: 0 % up_proof_size_4: 0 % up_proof_size_5: 0 % up_proof_size_greater: 0 % up_dismatched_contradictions: 0 % up_duplicate_conclusions: 0 % up_duplicate_unit_conclusions: 0 % up_duplicate_insts: 0 % up_non_proper_insts: 0 % up_dismatched_proofs: 0 % up_active_literals: 0 % up_active_clauses: 0 % up_unselected_var_eqs: 0 % up_var_eq_lemmas: 0 % up_clause_inst_var_eq: 0 % % %------------------------------------------------------------------------------