============================== Prover9 ===============================
Prover9 (32) version June-2006B, June 2006.
Process 30336 was started by zalta on mally,
Fri Sep 11 16:58:45 2009
The command was "prover9.orig".
============================== 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).
clear(fof_reduction).

% formulas(usable).  % not echoed (3 formulas)

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

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

============================== PROCESS INITIAL CLAUSES ===============
% Assigned IDs to 13 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.00 (+ 0.00) seconds.
% Length of proof is 23.
% Level of proof is 5.
% Maximum clause weight is 3.
% Given clauses 10.

1 - Object(x) | - Property(y) | - Point(z) | - EncAt(x,y,z) | - Point(u) | EncAt(x,y,u).  [clausify].
2 - Object(x) | - Proposition(y) | - Point(z) | - EncpAt(x,y,z) | Property(f1(x,y,z)).  [clausify].
3 - Object(x) | - Proposition(y) | - Point(z) | - EncpAt(x,y,z) | VAC(y) = f1(x,y,z).  [clausify].
4 - Object(x) | - Proposition(y) | - Point(z) | - EncpAt(x,y,z) | EncAt(x,f1(x,y,z),z).  [clausify].
5 - Object(x) | - Proposition(y) | - Point(z) | EncpAt(x,y,z) | - Property(u) | VAC(y) != u | - EncAt(x,u,z).  [clausify].
6 - Object(x) | - Proposition(y) | - Point(z) | - TrueInAt(y,x,z) | EncpAt(x,y,z).  [clausify].
7 - Object(x) | - Proposition(y) | - Point(z) | TrueInAt(y,x,z) | - EncpAt(x,y,z).  [clausify].
14 - Object(x) | - Proposition(y) | - Point(z) | - EncpAt(x,y,z) | f1(x,y,z) = VAC(y).  [copy(3),flip(e)].
15 Object(c1).  [clausify].
16 Proposition(c2).  [clausify].
17 Point(c3).  [clausify].
18 Point(c4).  [clausify].
19 TrueInAt(c2,c1,c3).  [clausify].
20 - TrueInAt(c2,c1,c4).  [clausify].
21 EncpAt(c1,c2,c3).  [hyper(6,a,15,a,b,16,a,c,17,a,d,19,a)].
22 - EncpAt(c1,c2,c4).  [ur(7,a,15,a,b,16,a,c,18,a,d,20,a)].
23 EncAt(c1,f1(c1,c2,c3),c3).  [hyper(4,a,15,a,b,16,a,c,17,a,d,21,a)].
24 f1(c1,c2,c3) = VAC(c2).  [hyper(14,a,15,a,b,16,a,c,17,a,d,21,a)].
25 Property(VAC(c2)).  [hyper(2,a,15,a,b,16,a,c,17,a,d,21,a),demod(24(4))].
26 EncAt(c1,VAC(c2),c3).  [back_demod(23),demod(24(5))].
27 - EncAt(c1,VAC(c2),c4).  [ur(5,a,15,a,b,16,a,c,18,a,d,22,a,e,25,a,f,xx)].
28 EncAt(c1,VAC(c2),c4).  [hyper(1,a,15,a,b,25,a,c,17,a,d,26,a,e,18,a)].
29 $F.  [resolve(28,a,27,a)].

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

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

Given=10. Generated=17. Kept=14. proofs=1.
Usable=17. Sos=2. Demods=1. Denials=0. Limbo=0, Disabled=8. Hints=0.
Megabytes=0.05.
User_CPU=0.00, System_CPU=0.00, Wall_clock=0.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 30336 exit (max_proofs) Fri Sep 11 16:58:45 2009