============================== Prover9 ===============================
Prover9 (32) version June-2006C, June 2006.
Process 13071 was started by mccune on cleo.thornwood,
Mon Jun 19 16:41:08 2006
The command was "/home/mccune/bin/prover9 -f w_sk.in".
============================== end of head ===========================

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

% Reading from file w_sk.in


clauses(sos).
a(a(a(S,x),y),z) = a(a(x,z),a(y,z)) # label(S).
a(a(K,x),y) = x # label(K).
end_of_list.

formulas(goals).
(exists W all x all y (a(a(W,x),y) = a(a(x,y),y))).
end_of_list.

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

============================== PROCESS GOALS =========================

% Each goal formula was negated; the result (to be placed in sos):

clauses(negated_goals).
a(a(x,f1(x)),f2(x)) != a(a(f1(x),f2(x)),f2(x)).
end_of_list.

============================== end of process goals ==================

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

% Clauses before input processing:

clauses(usable).
end_of_list.

clauses(sos).
1 a(a(a(S,x),y),z) = a(a(x,z),a(y,z)) # label(S).  [input].
2 a(a(K,x),y) = x # label(K).  [input].
3 a(a(x,f1(x)),f2(x)) != a(a(f1(x),f2(x)),f2(x)).  [clausify].
end_of_list.

clauses(demodulators).
end_of_list.

Predicate elimination: (none).

Auto_denials:  no changes.

Term ordering decisions:
Relation symbol precedence:  lex([ = ]).
Function symbol precedence:  lex([ K, S, a, f1, f2 ]).
After inverse_order: Function symbol precedence:  lex([ K, S, a, f1, f2 ]).
Unfolding symbols: (none).

Auto_inference settings:
  % set(paramodulation).  % (positive equality literals)
    % set(paramodulation) -> set(back_demod).

Auto_process settings:  no changes.

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

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

% Clauses after input processing:

clauses(usable).
end_of_list.

clauses(sos).
4 a(a(a(S,x),y),z) = a(a(x,z),a(y,z)) # label(S).  [input].
5 a(a(K,x),y) = x # label(K).  [input].
6 a(a(f1(x),f2(x)),f2(x)) != a(a(x,f1(x)),f2(x)).  [copy(3),flip(a)].
end_of_list.

clauses(demodulators).
5 a(a(K,x),y) = x # label(K).  [input].
end_of_list.

clauses(denials).
end_of_list.

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

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

% Starting search at 0.00 seconds.

given #1 (I,wt=15): 4 a(a(a(S,x),y),z) = a(a(x,z),a(y,z)) # label(S).  [input].

given #2 (I,wt=7): 5 a(a(K,x),y) = x # label(K).  [input].

given #3 (I,wt=16): 6 a(a(f1(x),f2(x)),f2(x)) != a(a(x,f1(x)),f2(x)).  [copy(3),flip(a)].

given #4 (T,wt=9): 15 a(a(a(S,K),x),y) = y.  [para(5(a,1),4(a,2))].

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

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

3 a(a(x,f1(x)),f2(x)) != a(a(f1(x),f2(x)),f2(x)).  [clausify].
4 a(a(a(S,x),y),z) = a(a(x,z),a(y,z)) # label(S).  [input].
5 a(a(K,x),y) = x # label(K).  [input].
6 a(a(f1(x),f2(x)),f2(x)) != a(a(x,f1(x)),f2(x)).  [copy(3),flip(a)].
15 a(a(a(S,K),x),y) = y.  [para(5(a,1),4(a,2))].
16 a(a(f1(a(a(S,x),y)),f2(a(a(S,x),y))),f2(a(a(S,x),y))) != a(a(a(x,f1(a(a(S,x),y))),a(y,f1(a(a(S,x),y)))),f2(a(a(S,x),y))).  [para(4(a,1),6(a,2,1))].
21 a(a(a(S,x),a(a(S,K),y)),z) = a(a(x,z),z).  [para(15(a,1),4(a,2,2))].
22 $F.  [resolve(21,a,16,a(flip))].

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

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

Given=4. Generated=33. Kept=18. proofs=1.
Usable=4. Sos=12. Demods=3. Denials=0. Limbo=1, Disabled=3. Hints=0.
Weight_deleted=0. Literals_deleted=0.
Forward_subsumed=15. Back_subsumed=0.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=3 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
Demod_attempts=360. Demod_rewrites=2.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=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 13071 exit (max_proofs) Mon Jun 19 16:41:08 2006