============================== Prover9 ===============================
Prover9 (32) version June-2007, June 2007.
Process 4902 was started by zalta on mally,
Sat Jul 14 17:18:38 2007
The command was "prove".
============================== end of head ===========================

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

formulas(sos).
(all x all y Sum(x,y) = Sum(y,x)).
(all x all y (IsIn(x,y) <-> (exists z Sum(x,z) = y))).
end_of_list.

formulas(goals).
(all x all y (Sum(x,y) = x -> IsIn(y,x))).
end_of_list.

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

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

% Formulas that are not ordinary clauses:
1 (all x all y Sum(x,y) = Sum(y,x)) # label(non_clause).  [assumption].
2 (all x all y (IsIn(x,y) <-> (exists z Sum(x,z) = y))) # label(non_clause).  [assumption].
3 (all x all y (Sum(x,y) = x -> IsIn(y,x))) # 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).
Sum(x,y) = Sum(y,x).  [clausify(1)].
-IsIn(x,y) | Sum(x,f1(x,y)) = y.  [clausify(2)].
IsIn(x,y) | Sum(x,z) != y.  [clausify(2)].
Sum(c1,c2) = c1.  [deny(3)].
-IsIn(c2,c1).  [deny(3)].
end_of_list.

formulas(demodulators).
end_of_list.

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

No predicates eliminated.

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

Auto_denials:  (no changes).

Term ordering decisions:
Predicate symbol precedence:  predicate_order([ =, IsIn ]).
Function symbol precedence:  function_order([ c1, c2, Sum, f1 ]).
After inverse_order:  (no changes).
Unfolding symbols: (none).

Auto_inference settings:
  % set(paramodulation).  % (positive equality literals)
    % set(paramodulation) -> set(back_demod).
  % set(hyper_resolution).  % (nonunit Horn with equality)
    % set(hyper_resolution) -> set(pos_hyper_resolution).
  % set(neg_ur_resolution).  % (nonunit Horn with equality)
  % assign(para_lit_limit, 2).  % (nonunit Horn with equality)

Auto_process settings:  (no changes).

% Operation Sum is commutative; C redundancy checks enabled.

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

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

% Clauses after input processing:

formulas(usable).
end_of_list.

formulas(sos).
4 Sum(x,y) = Sum(y,x).  [clausify(1)].
5 -IsIn(x,y) | Sum(x,f1(x,y)) = y.  [clausify(2)].
6 IsIn(x,y) | Sum(x,z) != y.  [clausify(2)].
7 Sum(c1,c2) = c1.  [deny(3)].
8 -IsIn(c2,c1).  [deny(3)].
end_of_list.

formulas(demodulators).
4 Sum(x,y) = Sum(y,x).  [clausify(1)].
        % (lex-dep)
7 Sum(c1,c2) = c1.  [deny(3)].
end_of_list.

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

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

% Starting search at 0.00 seconds.

given #1 (I,wt=7): 4 Sum(x,y) = Sum(y,x).  [clausify(1)].

given #2 (I,wt=10): 5 -IsIn(x,y) | Sum(x,f1(x,y)) = y.  [clausify(2)].

given #3 (I,wt=8): 6 IsIn(x,y) | Sum(x,z) != y.  [clausify(2)].

given #4 (I,wt=5): 7 Sum(c1,c2) = c1.  [deny(3)].

given #5 (I,wt=3): 8 -IsIn(c2,c1).  [deny(3)].

given #6 (A,wt=5): 9 IsIn(x,Sum(y,x)).  [hyper(6,b,4,a)].

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

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

1 (all x all y Sum(x,y) = Sum(y,x)) # label(non_clause).  [assumption].
2 (all x all y (IsIn(x,y) <-> (exists z Sum(x,z) = y))) # label(non_clause).  [assumption].
3 (all x all y (Sum(x,y) = x -> IsIn(y,x))) # label(non_clause) # label(goal).  [goal].
4 Sum(x,y) = Sum(y,x).  [clausify(1)].
6 IsIn(x,y) | Sum(x,z) != y.  [clausify(2)].
7 Sum(c1,c2) = c1.  [deny(3)].
8 -IsIn(c2,c1).  [deny(3)].
9 IsIn(x,Sum(y,x)).  [hyper(6,b,4,a)].
16 IsIn(c2,c1).  [para(7(a,1),9(a,2))].
17 $F.  [resolve(16,a,8,a)].

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

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

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

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 4902 exit (max_proofs) Sat Jul 14 17:18:38 2007