============================== Prover9 ===============================
Prover9 (32) version June-2006B, June 2006.
Process 3634 was started by zalta on mally,
Wed Jun 14 16:56:08 2006
The command was "prove".
============================== end of head ===========================

============================== INPUT =================================
set(auto2).
    % set(auto2) -> set(auto).
    % set(auto) -> set(auto_inference).
    % set(auto_inference) -> set(predicate_elim).
    % set(auto_inference) -> assign(eq_defs, unfold).
    % set(auto) -> set(auto_limits).
    % set(auto_limits) -> assign(max_weight, 100).
    % set(auto_limits) -> assign(sos_limit, 10000).
    % set(auto2) -> set(fof_reduction).
    % set(auto2) -> assign(new_constants, 1).
    % set(auto2) -> assign(fold_denial_max, 3).
    % set(auto2) -> assign(max_weight, 200).
    % set(auto2) -> assign(nest_penalty, 1).
    % set(auto2) -> assign(skolem_penalty, 3).
    % set(auto2) -> assign(sk_constant_weight, 0).
    % set(auto2) -> assign(prop_atom_weight, 5).
    % set(auto2) -> set(sort_initial_sos).
    % set(auto2) -> assign(sos_limit, -1).
    % set(auto2) -> assign(lrs_ticks, 3000).
    % set(auto2) -> assign(max_megs, 400).
    % set(auto2) -> assign(stats, some).
    % set(auto2) -> clear(echo_input).
    % set(auto2) -> set(quiet).
    % set(auto2) -> clear(print_subproblems).
    % set(auto2) -> clear(print_initial_clauses).
    % set(auto2) -> clear(print_given).

% formulas(sos).  % not echoed (2 formulas)

============================== end of input ==========================

Attempting problem reduction; original problem has <nnf_size,cnf_max> = <42,14>.

Problem reduction (0.00 sec) gives one subproblem (<68,13>);
  reverting to ordinary search with original formulas.

============================== PROCESS INITIAL CLAUSES ===============
% Assigned IDs to 10 clauses.

Term ordering decisions:

============================== PROOF =================================

% Proof 1 at 0.00 (+ 0.00) seconds.
% Length of proof is 14.
% Level of proof is 5.
% Maximum clause weight is 1.
% Given clauses 0.

1 Object(c1).  [clausify].
2 Object(c2).  [clausify].
3 Property(c3).  [clausify].
4 IsTheFormOf(c1,c3).  [clausify].
5 Enc(c2,c3).  [clausify].
6 - PartPH(c2,c1).  [clausify].
10 - Object(x) | - Object(y) | PartPH(x,y) | - Property(z) | - IsTheFormOf(y,z) | - Enc(x,z).  [clausify].
11 - Object(x) | - Object(y) | PartPH(x,y) | - IsTheFormOf(y,c3) | - Enc(x,c3).  [resolve(10,d,3,a)].
13 - Object(x) | - Object(c1) | PartPH(x,c1) | - Enc(x,c3).  [resolve(11,d,4,a)].
15 - Object(c2) | - Object(c1) | PartPH(c2,c1).  [resolve(13,d,5,a)].
16 - Object(c2) | - Object(c1).  [resolve(15,c,6,a)].
17 Object(c1).  [copy(1)].
18 Object(c2).  [copy(2)].
19 $F.  [copy(16),unit_del(a,18),unit_del(b,17)].

============================== end of proof ==========================

============================== STATISTICS ============================

Given=0. Generated=3. Kept=2. proofs=1.
Usable=0. Sos=0. Demods=0. Denials=0. Limbo=2, Disabled=16. Hints=0.
Megabytes=0.02.
User_CPU=0.00, System_CPU=0.00, Wall_clock=0.

============================== end of statistics =====================

============================== end of search =========================

THEOREM PROVED

Exiting with 1 proof.

Process 3634 exit (max_proofs) Wed Jun 14 16:56:08 2006