iProver-Eq---0.85.UNK-Non.f

%------------------------------------------------------------------------------
% File     : iProver-Eq---0.85
% Problem  : TOP048+2 : TPTP v5.5.0. Released v3.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : iprover-cvc4-eq-nc --time_out_virtual %d %s

% Computer : art03.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 : Sun Jun  9 07:39:50 EDT 2013

% Result   : Unknown 1.95s
% Output   : None 
% 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
%