============================== Prover9 ===============================
Prover9 (32) version June-2006B, June 2006.
Process 30418 was started by zalta on mally,
Fri Sep 11 17:19:22 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(sos).  % not echoed (8 formulas)

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

============================== PROCESS INITIAL CLAUSES ===============
% Assigned IDs to 22 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 28.
% Level of proof is 6.
% Maximum clause weight is 8.
% Given clauses 7.

2 Proposition(c1).  [clausify].
3 World(c2).  [clausify].
4 TrueIn(c1,c2).  [clausify].
5 - PossiblyTrue(c1).  [clausify].
6 - WorldAt(x,y) | Object(x).  [clausify].
9 - World(x) | WorldAt(x,W).  [clausify].
12 PossiblyTrue(x) | - Point(y) | - True(x,y).  [clausify].
13 - TrueIn(x,y) | TrueInAt(x,y,W).  [clausify].
16 - Object(x) | - Point(y) | - WorldAt(x,y) | Point(f1(x,y)).  [clausify].
17 - Object(x) | - Proposition(y) | - Point(z) | - TrueInAt(y,x,z) | - Point(u) | TrueInAt(y,x,u).  [clausify].
19 - Object(x) | - Point(y) | - WorldAt(x,y) | - Proposition(z) | - TrueInAt(z,x,f1(x,y)) | True(z,f1(x,y)).  [clausify].
23 - Object(x) | - Point(y) | - TrueInAt(c1,x,y) | - Point(z) | TrueInAt(c1,x,z).  [resolve(17,b,2,a)].
25 - Object(x) | - Point(y) | - WorldAt(x,y) | - TrueInAt(c1,x,f1(x,y)) | True(c1,f1(x,y)).  [resolve(19,d,2,a)].
29 WorldAt(c2,W).  [resolve(9,a,3,a)].
34 Object(c2).  [resolve(29,a,6,a)].
36 - Object(c2) | - Point(W) | Point(f1(c2,W)).  [resolve(29,a,16,c)].
37 - Object(c2) | - Point(W) | - TrueInAt(c1,c2,f1(c2,W)) | True(c1,f1(c2,W)).  [resolve(29,a,25,c)].
40 - Point(W) | Point(f1(c2,W)).  [resolve(36,a,34,a)].
41 - Point(W) | - TrueInAt(c1,c2,f1(c2,W)) | True(c1,f1(c2,W)).  [resolve(37,a,34,a)].
43 Point(W).  [clausify].
44 TrueInAt(c1,c2,W).  [resolve(13,a,4,a)].
45 - Point(x) | - True(c1,x).  [resolve(12,a,5,a)].
48 - Point(x) | - TrueInAt(c1,c2,x) | - Point(y) | TrueInAt(c1,c2,y).  [resolve(34,a,23,a)].
49 Point(f1(c2,W)).  [copy(40),unit_del(a,43)].
50 - TrueInAt(c1,c2,f1(c2,W)) | True(c1,f1(c2,W)).  [copy(41),unit_del(a,43)].
54 - True(c1,f1(c2,W)).  [resolve(49,a,45,a)].
55 TrueInAt(c1,c2,f1(c2,W)).  [ur(48,a,43,a,b,44,a,c,49,a)].
56 $F.  [back_unit_del(50),unit_del(a,55),unit_del(b,54)].

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

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

Given=7. Generated=19. Kept=13. proofs=1.
Usable=7. Sos=2. Demods=0. Denials=0. Limbo=2, Disabled=44. 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 30418 exit (max_proofs) Fri Sep 11 17:19:22 2009