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

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

% Reading from file subset_trans.in


formulas(sos).
(all x all y (subset(x,y) <-> (all z (mem(z,x) -> mem(z,y))))).
end_of_list.

formulas(goals).
(all x all y all z (subset(x,y) & subset(y,z) -> subset(x,z))).
end_of_list.

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

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

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

clauses(negated_goals).
subset(c1,c2).
subset(c2,c3).
- subset(c1,c3).
end_of_list.

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

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

% Clauses before input processing:

clauses(usable).
end_of_list.

clauses(sos).
1 - subset(x,y) | - mem(z,x) | mem(z,y).  [clausify].
2 subset(x,y) | mem(f1(x,y),x).  [clausify].
3 subset(x,y) | - mem(f1(x,y),y).  [clausify].
4 subset(c1,c2).  [clausify].
5 subset(c2,c3).  [clausify].
6 - subset(c1,c3).  [clausify].
end_of_list.

clauses(demodulators).
end_of_list.

Predicate elimination: subset/2.

Auto_denials:  no changes.

Term ordering decisions:
Relation symbol precedence:  lex([ mem, subset ]).
Function symbol precedence:  lex([ c1, c2, c3, f1 ]).
After inverse_order: Function symbol precedence:  lex([ c1, c2, c3, f1 ]).
Unfolding symbols: (none).

Auto_inference settings:
  % set(binary_resolution).  % (non-Horn)
  % set(neg_ur_resolution).  % (non-Horn, less than 100 clauses)

Auto_process settings:
  % set(factor).  % (non-Horn)
  % set(back_unit_deletion).  % (non-Horn)
    % set(back_unit_deletion) -> set(unit_deletion).

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

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

% Clauses after input processing:

clauses(usable).
end_of_list.

clauses(sos).
13 mem(f1(x,y),x) | - mem(z,x) | mem(z,y).  [resolve(2,a,1,a)].
14 - mem(f1(x,y),y) | - mem(z,x) | mem(z,y).  [resolve(3,a,1,a)].
15 - mem(x,c1) | mem(x,c2).  [resolve(4,a,1,a)].
16 - mem(x,c2) | mem(x,c3).  [resolve(5,a,1,a)].
17 mem(f1(c1,c3),c1).  [resolve(6,a,2,a)].
18 - mem(f1(c1,c3),c3).  [resolve(6,a,3,a)].
end_of_list.

clauses(demodulators).
end_of_list.

clauses(denials).
end_of_list.

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

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

% Starting search at 0.00 seconds.

given #1 (I,wt=11): 13 mem(f1(x,y),x) | - mem(z,x) | mem(z,y).  [resolve(2,a,1,a)].

given #2 (I,wt=11): 14 - mem(f1(x,y),y) | - mem(z,x) | mem(z,y).  [resolve(3,a,1,a)].

given #3 (I,wt=6): 15 - mem(x,c1) | mem(x,c2).  [resolve(4,a,1,a)].

given #4 (I,wt=6): 16 - mem(x,c2) | mem(x,c3).  [resolve(5,a,1,a)].

given #5 (I,wt=5): 17 mem(f1(c1,c3),c1).  [resolve(6,a,2,a)].

given #6 (I,wt=5): 18 - mem(f1(c1,c3),c3).  [resolve(6,a,3,a)].

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

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

1 - subset(x,y) | - mem(z,x) | mem(z,y).  [clausify].
2 subset(x,y) | mem(f1(x,y),x).  [clausify].
3 subset(x,y) | - mem(f1(x,y),y).  [clausify].
4 subset(c1,c2).  [clausify].
5 subset(c2,c3).  [clausify].
6 - subset(c1,c3).  [clausify].
15 - mem(x,c1) | mem(x,c2).  [resolve(4,a,1,a)].
16 - mem(x,c2) | mem(x,c3).  [resolve(5,a,1,a)].
17 mem(f1(c1,c3),c1).  [resolve(6,a,2,a)].
18 - mem(f1(c1,c3),c3).  [resolve(6,a,3,a)].
19 mem(f1(c1,c3),c2).  [resolve(17,a,15,a)].
22 $F.  [ur(16,b,18,a),unit_del(a,19)].

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

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

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

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 13074 exit (max_proofs) Mon Jun 19 16:41:11 2006