============================== Prover9 ===============================
Prover9 (32) version June-2006B, June 2006.
Process 3766 was started by zalta on mally,
Wed Jun 14 17:11:39 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> = <91,37>.

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

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

Term ordering decisions:

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

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

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

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

% Starting search at 0.00 seconds.

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

% Proof 1 at 0.01 (+ 0.01) seconds.
% Length of proof is 25.
% Level of proof is 6.
% Maximum clause weight is 24.
% Given clauses 18.

2 PartOf(c1,c2).  [clausify].
4 - PartOf(x,y) | Object(x).  [clausify].
5 - PartOf(x,y) | Object(y).  [clausify].
8 - Object(x) | - Object(y) | - PartOf(x,y) | Ex1(A,x,W).  [clausify].
11 - Object(x) | - Situation(x) | - Property(y) | - Enc(x,y) | Proposition(f1(x,y)).  [clausify].
13 - Object(x) | Situation(x) | - Ex1(A,x,W) | - Proposition(y) | VAC(y) != f2(x).  [clausify].
14 - Object(x) | - Object(y) | - PartOf(x,y) | - Property(z) | - Enc(x,z) | Enc(y,z).  [clausify].
20 - Object(c1) | - Object(c2) | Ex1(A,c1,W).  [resolve(8,c,2,a)].
22 - Object(c1) | - Object(c2) | - Property(x) | - Enc(c1,x) | Enc(c2,x).  [resolve(14,c,2,a)].
26 - Object(x) | Situation(x) | - Ex1(A,x,W) | VAC(f1(y,z)) != f2(x) | - Object(y) | - Situation(y) | - Property(z) | - Enc(y,z).  [resolve(13,d,11,e)].
27 Situation(c2).  [clausify].
28 - Situation(c1).  [clausify].
30 - Object(x) | Situation(x) | - Ex1(A,x,W) | Property(f2(x)).  [clausify].
31 - Object(x) | Situation(x) | - Ex1(A,x,W) | Enc(x,f2(x)).  [clausify].
32 - Object(x) | - Situation(x) | - Property(y) | - Enc(x,y) | VAC(f1(x,y)) = y.  [clausify].
33 Object(c1).  [resolve(4,a,2,a)].
34 Object(c2).  [resolve(5,a,2,a)].
35 Ex1(A,c1,W).  [copy(20),unit_del(a,33),unit_del(b,34)].
37 - Property(x) | - Enc(c1,x) | Enc(c2,x).  [copy(22),unit_del(a,33),unit_del(b,34)].
41 - Object(x) | Situation(x) | - Ex1(A,x,W) | f2(x) != VAC(f1(y,z)) | - Object(y) | - Situation(y) | - Property(z) | - Enc(y,z).  [copy(26),flip(d)].
42 Enc(c1,f2(c1)).  [resolve(35,a,31,c),unit_del(a,33),unit_del(b,28)].
43 Property(f2(c1)).  [resolve(35,a,30,c),unit_del(a,33),unit_del(b,28)].
56 Enc(c2,f2(c1)).  [resolve(42,a,37,b),unit_del(a,43)].
57 VAC(f1(c2,f2(c1))) = f2(c1).  [resolve(56,a,32,d),unit_del(a,34),unit_del(b,27),unit_del(c,43)].
58 $F.  [ur(41,a,33,a,b,28,a,c,35,a,e,34,a,f,27,a,g,43,a,h,56,a),demod(57(7)),xx(a)].

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

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

Given=18. Generated=53. Kept=31. proofs=1.
Usable=18. Sos=12. Demods=1. Denials=0. Limbo=1, Disabled=26. Hints=0.
Megabytes=0.08.
User_CPU=0.01, System_CPU=0.01, Wall_clock=0.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 3766 exit (max_proofs) Wed Jun 14 17:11:39 2006