============================== Prover9 ===============================
Prover9 (32) version 2009-02A, February 2009.
Process 15828 was started by mccune on cleo,
Wed Feb 25 12:25:50 2009
The command was "/home/mccune/bin/prover9 -f subset.in trans.in".
============================== end of head ===========================

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

% Reading from file subset.in


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

% Reading from file trans.in


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

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

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

% Formulas that are not ordinary clauses:
1 (all x all y (subset(x,y) <-> (all z (member(z,x) -> member(z,y))))) # label(non_clause).  [assumption].
2 (all x all y all z (subset(x,y) & subset(y,z) -> subset(x,z))) # 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).
-subset(x,y) | -member(z,x) | member(z,y).  [clausify(1)].
subset(x,y) | member(f1(x,y),x).  [clausify(1)].
subset(x,y) | -member(f1(x,y),y).  [clausify(1)].
subset(c1,c2).  [deny(2)].
subset(c2,c3).  [deny(2)].
-subset(c1,c3).  [deny(2)].
end_of_list.

formulas(demodulators).
end_of_list.

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

Eliminating subset/2
3 subset(x,y) | member(f1(x,y),x).  [clausify(1)].
4 -subset(x,y) | -member(z,x) | member(z,y).  [clausify(1)].
Derived: member(f1(x,y),x) | -member(z,x) | member(z,y).  [resolve(3,a,4,a)].
5 subset(x,y) | -member(f1(x,y),y).  [clausify(1)].
Derived: -member(f1(x,y),y) | -member(z,x) | member(z,y).  [resolve(5,a,4,a)].
6 subset(c1,c2).  [deny(2)].
Derived: -member(x,c1) | member(x,c2).  [resolve(6,a,4,a)].
7 subset(c2,c3).  [deny(2)].
Derived: -member(x,c2) | member(x,c3).  [resolve(7,a,4,a)].
8 -subset(c1,c3).  [deny(2)].
Derived: member(f1(c1,c3),c1).  [resolve(8,a,3,a)].
Derived: -member(f1(c1,c3),c3).  [resolve(8,a,5,a)].

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

Auto_denials:  (non-Horn, no changes).

Term ordering decisions:
Predicate symbol precedence:  predicate_order([ member ]).
Function symbol precedence:  function_order([ c1, c2, c3, f1 ]).
After inverse_order:  (no changes).
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(unit_deletion).  % (non-Horn)

kept:      9 member(f1(x,y),x) | -member(z,x) | member(z,y).  [resolve(3,a,4,a)].
kept:      10 -member(f1(x,y),y) | -member(z,x) | member(z,y).  [resolve(5,a,4,a)].
kept:      11 -member(x,c1) | member(x,c2).  [resolve(6,a,4,a)].
kept:      12 -member(x,c2) | member(x,c3).  [resolve(7,a,4,a)].
kept:      13 member(f1(c1,c3),c1).  [resolve(8,a,3,a)].
kept:      14 -member(f1(c1,c3),c3).  [resolve(8,a,5,a)].

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

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

% Clauses after input processing:

formulas(usable).
end_of_list.

formulas(sos).
9 member(f1(x,y),x) | -member(z,x) | member(z,y).  [resolve(3,a,4,a)].
10 -member(f1(x,y),y) | -member(z,x) | member(z,y).  [resolve(5,a,4,a)].
11 -member(x,c1) | member(x,c2).  [resolve(6,a,4,a)].
12 -member(x,c2) | member(x,c3).  [resolve(7,a,4,a)].
13 member(f1(c1,c3),c1).  [resolve(8,a,3,a)].
14 -member(f1(c1,c3),c3).  [resolve(8,a,5,a)].
end_of_list.

formulas(demodulators).
end_of_list.

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

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

% Starting search at 0.01 seconds.

given #1 (I,wt=11): 9 member(f1(x,y),x) | -member(z,x) | member(z,y).  [resolve(3,a,4,a)].

given #2 (I,wt=11): 10 -member(f1(x,y),y) | -member(z,x) | member(z,y).  [resolve(5,a,4,a)].

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

given #4 (I,wt=6): 12 -member(x,c2) | member(x,c3).  [resolve(7,a,4,a)].

given #5 (I,wt=5): 13 member(f1(c1,c3),c1).  [resolve(8,a,3,a)].

given #6 (I,wt=5): 14 -member(f1(c1,c3),c3).  [resolve(8,a,5,a)].

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

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

1 (all x all y (subset(x,y) <-> (all z (member(z,x) -> member(z,y))))) # label(non_clause).  [assumption].
2 (all x all y all z (subset(x,y) & subset(y,z) -> subset(x,z))) # label(non_clause) # label(goal).  [goal].
3 subset(x,y) | member(f1(x,y),x).  [clausify(1)].
4 -subset(x,y) | -member(z,x) | member(z,y).  [clausify(1)].
5 subset(x,y) | -member(f1(x,y),y).  [clausify(1)].
6 subset(c1,c2).  [deny(2)].
7 subset(c2,c3).  [deny(2)].
8 -subset(c1,c3).  [deny(2)].
11 -member(x,c1) | member(x,c2).  [resolve(6,a,4,a)].
12 -member(x,c2) | member(x,c3).  [resolve(7,a,4,a)].
13 member(f1(c1,c3),c1).  [resolve(8,a,3,a)].
14 -member(f1(c1,c3),c3).  [resolve(8,a,5,a)].
15 member(f1(c1,c3),c2).  [resolve(13,a,11,a)].
18 $F.  [ur(12,b,14,a),unit_del(a,15)].

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

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

Given=6. Generated=12. Kept=9. proofs=1.
Usable=6. Sos=3. Demods=0. Limbo=0, Disabled=12. Hints=0.
Kept_by_rule=0, Deleted_by_rule=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.03.
User_CPU=0.01, System_CPU=0.00, Wall_clock=0.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 15828 exit (max_proofs) Wed Feb 25 12:25:50 2009
