============================== Prover9 ===============================
Prover9 (32) version Dec-2007, Dec 2007.
Process 10686 was started by mccune on cleo,
Wed Dec 12 20:34:11 2007
The command was "./prover9 -f temp1".
============================== end of head ===========================

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

% Reading from file temp1

op(400,infix,["=>"]).
set(raw).
    % set(raw) -> clear(auto).
    % clear(auto) -> clear(auto_inference).
    % clear(auto) -> clear(auto_setup).
    % clear(auto_setup) -> clear(predicate_elim).
    % clear(auto_setup) -> assign(eq_defs, pass).
    % clear(auto) -> clear(auto_limits).
    % clear(auto_limits) -> assign(max_weight, 2147483647).
    % clear(auto_limits) -> assign(sos_limit, -1).
    % clear(auto) -> clear(auto_denials).
    % clear(auto) -> clear(auto_process).
    % set(raw) -> clear(ordered_res).
    % set(raw) -> clear(ordered_para).
    % set(raw) -> assign(literal_selection, none).
    % set(raw) -> clear(back_demod).
    % set(raw) -> clear(cac_redundancy).
    % set(raw) -> assign(backsub_check, 2147483647).
    % set(raw) -> set(lightest_first).
    % set(lightest_first) -> assign(weight_part, 1).
    % set(lightest_first) -> assign(age_part, 0).
    % set(lightest_first) -> assign(false_part, 0).
    % set(lightest_first) -> assign(true_part, 0).
    % set(lightest_first) -> assign(random_part, 0).
set(paramodulation).
set(print_gen).

formulas(usable).
-DumLit | P(A => (1 => y)).
end_of_list.

formulas(sos).
1 => x = x.
end_of_list.

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

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

% Formulas that are not ordinary clauses:

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

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

% Clauses before input processing:

formulas(usable).
-DumLit | P(A => (1 => x)).  [assumption].
end_of_list.

formulas(sos).
1 => x = x.  [assumption].
end_of_list.

formulas(demodulators).
end_of_list.

Term ordering decisions:
Predicate symbol precedence:  predicate_order([ =, DumLit, P ]).
Function symbol precedence:  function_order([ 1, A, => ]).
After inverse_order:  (no changes).

generated: 1 => x = x.  [assumption].
kept:      2 1 => x = x.  [assumption].

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

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

% Clauses after input processing:

formulas(usable).
1 -DumLit | P(A => (1 => x)).  [assumption].
end_of_list.

formulas(sos).
2 1 => x = x.  [assumption].
end_of_list.

formulas(demodulators).
end_of_list.

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

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

% Starting search at 0.00 seconds.

given #1 (I,wt=5): 2 1 => x = x.  [assumption].

generated: -DumLit | P(A => v100).  [para(2(a,1),1(b,1,2))].
kept:      3 -DumLit | P(A => x).  [para(2(a,1),1(b,1,2))].

generated: v100 = v100.  [para(2(a,1),2(a,1))].
tautology

given #2 (W,wt=5): 3 -DumLit | P(A => x).  [para(2(a,1),1(b,1,2))].

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

Given=2. Generated=3. Kept=2. proofs=0.
Usable=2. Sos=0. Demods=0. Limbo=0, Disabled=2. Hints=0.
Weight_deleted=0. Literals_deleted=0.
Forward_subsumed=1. Back_subsumed=1.
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=2.
Megabytes=0.01.
User_CPU=0.00, System_CPU=0.00, Wall_clock=0.

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

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

SEARCH FAILED

Exiting with failure.

Process 10686 exit (sos_empty) Wed Dec 12 20:34:11 2007
