============================== Prover9 ===============================
Prover9 (32) version June-2007, June 2007.
Process 26909 was started by mccune on rhea,
Thu Jun 14 14:03:55 2007
The command was "prover9 -f example.in".
============================== end of head ===========================

============================== INPUT =================================

% Reading from file example.in


formulas(assumptions).
p(x) -> q(x).
p(a).
end_of_list.

formulas(goals).
q(a).
end_of_list.

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

============================== PROCESS NON-CLAUSAL FORMULAS ==========

% Formulas that are not ordinary clauses:
1 p(x) -> q(x) # label(non_clause).  [assumption].
2 q(a) # label(non_clause) # label(goal).  [goal].

============================== end of process non-clausal formulas ===

============================== PROCESS INITIAL CLAUSES ===============

% Clauses before input processing:

formulas(usable).
end_of_list.

formulas(sos).
-p(x) | q(x).  [clausify(1)].
p(a).  [assumption].
-q(a).  [deny(2)].
end_of_list.

formulas(demodulators).
end_of_list.

============================== PREDICATE ELIMINATION =================

Eliminating p/1
3 p(a).  [assumption].
4 -p(x) | q(x).  [clausify(1)].
Derived: q(a).  [resolve(3,a,4,a)].

Eliminating q/1
5 q(a).  [resolve(3,a,4,a)].
6 -q(a).  [deny(2)].
Derived: $F.  [resolve(5,a,6,a)].

============================== end predicate elimination =============

Auto_denials:  (no changes).

Term ordering decisions:
Predicate symbol precedence:  predicate_order([ ]).
Function symbol precedence:  function_order([ ]).
After inverse_order:  (no changes).
Unfolding symbols: (none).

Auto_inference settings:
  % set(neg_binary_resolution).  % (HNE depth_diff=0)
  % clear(ordered_res).  % (HNE depth_diff=0)
  % set(ur_resolution).  % (HNE depth_diff=0)
    % set(ur_resolution) -> set(pos_ur_resolution).
    % set(ur_resolution) -> set(neg_ur_resolution).

Auto_process settings:  (no changes).

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

% Proof 1 at 0.00 (+ 0.00) seconds.
% Length of proof is 7.
% Level of proof is 3.
% Maximum clause weight is 0.
% Given clauses 0.

1 p(x) -> q(x) # label(non_clause).  [assumption].
2 q(a) # label(non_clause) # label(goal).  [goal].
3 p(a).  [assumption].
4 -p(x) | q(x).  [clausify(1)].
5 q(a).  [resolve(3,a,4,a)].
6 -q(a).  [deny(2)].
7 $F.  [resolve(5,a,6,a)].

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

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

Given=0. Generated=1. Kept=0. proofs=1.
Usable=0. Sos=0. Demods=0. Limbo=0, Disabled=5. Hints=0.
Weight_deleted=0. Literals_deleted=0.
Forward_subsumed=0. Back_subsumed=0.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
Demod_attempts=0. Demod_rewrites=0.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.
Megabytes=0.01.
User_CPU=0.00, System_CPU=0.00, Wall_clock=0.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 26909 exit (max_proofs) Thu Jun 14 14:03:55 2007