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

============================== INPUT =================================
op(300,prefix,~).
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 (6 formulas)

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

============================== 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.00 seconds.

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

% Proof 1 at 0.00 (+ 0.01) seconds.
% Length of proof is 31.
% Level of proof is 6.
% Maximum clause weight is 11.
% Given clauses 12.

1 Possible(c1).  [clausify].
2 Situation(c1).  [clausify].
3 - Consistent(c1).  [clausify].
6 - Situation(x) | Object(x).  [clausify].
10 - Object(x) | - Possible(x) | Point(f1(x)).  [clausify].
11 - Object(x) | Consistent(x) | - Situation(x) | Proposition(f3(x)).  [clausify].
12 - Object(x) | Consistent(x) | - Situation(x) | TrueIn(f3(x),x).  [clausify].
14 - Object(x) | Consistent(x) | - Situation(x) | TrueIn(~ f3(x),x).  [clausify].
16 - Object(x) | - Possible(x) | - Proposition(y) | - TrueIn(y,x) | True(y,f1(x)).  [clausify].
20 - Object(c1) | Point(f1(c1)).  [resolve(10,b,1,a)].
22 - Object(c1) | - Proposition(x) | - TrueIn(x,c1) | True(x,f1(c1)).  [resolve(16,b,1,a)].
29 - Object(c1) | Consistent(c1) | Proposition(f3(c1)).  [resolve(11,c,2,a)].
30 - Object(c1) | Consistent(c1) | TrueIn(f3(c1),c1).  [resolve(12,c,2,a)].
31 - Object(c1) | Consistent(c1) | TrueIn(~ f3(c1),c1).  [resolve(14,c,2,a)].
53 - Object(c1) | Proposition(f3(c1)).  [resolve(29,b,3,a)].
55 - Object(c1) | TrueIn(f3(c1),c1).  [resolve(30,b,3,a)].
57 - Object(c1) | TrueIn(~ f3(c1),c1).  [resolve(31,b,3,a)].
77 - Point(x) | - Proposition(y) | - True(~ y,x) | - True(y,x).  [clausify].
78 - Proposition(x) | Proposition(~ x).  [clausify].
80 - Object(c1) | Point(f1(c1)).  [copy(20)].
81 - Object(c1) | - Proposition(x) | - TrueIn(x,c1) | True(x,f1(c1)).  [copy(22)].
82 Object(c1).  [resolve(6,a,2,a)].
89 Proposition(f3(c1)).  [copy(53),unit_del(a,82)].
90 TrueIn(f3(c1),c1).  [copy(55),unit_del(a,82)].
91 TrueIn(~ f3(c1),c1).  [copy(57),unit_del(a,82)].
92 - Proposition(x) | - TrueIn(x,c1) | True(x,f1(c1)).  [back_unit_del(81),unit_del(a,82)].
93 Point(f1(c1)).  [back_unit_del(80),unit_del(a,82)].
95 Proposition(~ f3(c1)).  [resolve(89,a,78,a)].
96 True(~ f3(c1),f1(c1)).  [resolve(92,b,91,a),unit_del(a,95)].
97 True(f3(c1),f1(c1)).  [resolve(92,b,90,a),unit_del(a,89)].
100 $F.  [ur(77,a,93,a,b,89,a,d,97,a),unit_del(a,96)].

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

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

Given=12. Generated=25. Kept=23. proofs=1.
Usable=12. Sos=3. Demods=0. Denials=0. Limbo=0, Disabled=54. Hints=0.
Megabytes=0.07.
User_CPU=0.00, System_CPU=0.01, Wall_clock=0.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 3743 exit (max_proofs) Wed Jun 14 17:08:55 2006