============================== Prover9 =============================== Prover9 (32) version 2009-02A, February 2009. Process 15826 was started by mccune on cleo, Wed Feb 25 12:25:50 2009 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 (member(z,x) -> member(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 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 15826 exit (max_proofs) Wed Feb 25 12:25:50 2009