============================== Prover9 ===============================
Prover9 (32) version June-2006B, June 2006.
Process 3625 was started by root on mally,
Wed Jun 14 16:54:32 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 (4 formulas)

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

Attempting problem reduction; original problem has <nnf_size,cnf_max> = <115,57>.

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

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

Term ordering decisions:

============================== end of process initial clauses ========

============================== CLAUSES FOR SEARCH ====================

============================== end of clauses for search =============

============================== SEARCH ================================

% Starting search at 0.01 seconds.

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

% Proof 1 at 0.01 (+ 0.02) seconds.
% Length of proof is 18.
% Level of proof is 5.
% Maximum clause weight is 15.
% Given clauses 32.

1 Object(c1).  [clausify].
5 - Object(x) | - Property(y) | - IsTheFormOf(x,y) | IsAFormOf(x,y).  [clausify].
12 - Object(x) | - Property(y) | - IsAFormOf(x,y) | - Property(z) | Enc(x,z) | - Implies(y,z).  [clausify].
30 Property(c2).  [clausify].
31 IsTheFormOf(c1,c2).  [clausify].
32 - Enc(c1,c2).  [clausify].
33 - Property(x) | - Property(y) | Implies(x,y) | Ex1(x,f1(x,y),f2(x,y)).  [clausify].
34 - Property(x) | - Property(y) | Implies(x,y) | - Ex1(y,f1(x,y),f2(x,y)).  [clausify].
35 - Property(x) | - IsTheFormOf(c1,x) | IsAFormOf(c1,x).  [resolve(5,a,1,a)].
39 - Property(x) | - IsAFormOf(c1,x) | - Property(y) | Enc(c1,y) | - Implies(x,y).  [resolve(12,a,1,a)].
46 - Property(x) | Implies(x,x) | Ex1(x,f1(x,x),f2(x,x)).  [factor(33,a,b)].
47 - Property(x) | Implies(x,x) | - Ex1(x,f1(x,x),f2(x,x)).  [factor(34,a,b)].
49 - Property(x) | - IsAFormOf(c1,x) | Enc(c1,x) | - Implies(x,x).  [factor(39,a,c)].
60 IsAFormOf(c1,c2).  [resolve(35,b,31,a),unit_del(a,30)].
62 Implies(c2,c2) | Ex1(c2,f1(c2,c2),f2(c2,c2)).  [resolve(46,a,30,a)].
64 - Implies(c2,c2).  [ur(49,a,30,a,b,60,a,c,32,a)].
68 Ex1(c2,f1(c2,c2),f2(c2,c2)).  [back_unit_del(62),unit_del(a,64)].
69 $F.  [ur(47,a,30,a,b,64,a),unit_del(a,68)].

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

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

Given=32. Generated=60. Kept=39. proofs=1.
Usable=28. Sos=6. Demods=0. Denials=0. Limbo=0, Disabled=34. Hints=0.
Megabytes=0.09.
User_CPU=0.01, System_CPU=0.02, Wall_clock=0.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 3625 exit (max_proofs) Wed Jun 14 16:54:32 2006