============================== FOF-Prover9 =========================== FOF-Prover9 (32) version 2009-02A, February 2009. Process 11559 was started by mccune on cleo, Wed Feb 25 09:32:32 2009 The command was "/home/mccune/bin/fof-prover9 -f SET598+3.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file SET598+3.in assign(max_seconds,30). set(prolog_style_variables). formulas(assumptions). (all B all C subset(intersection(B,C),B)). (all B all C all D (subset(B,C) & subset(B,D) -> subset(B,intersection(C,D)))). (all B all C all D (member(D,intersection(B,C)) <-> member(D,B) & member(D,C))). (all B all C (subset(B,C) <-> (all D (member(D,B) -> member(D,C))))). (all B all C (B = C <-> subset(B,C) & subset(C,B))). (all B all C intersection(B,C) = intersection(C,B)). (all B subset(B,B)). (all B all C (B = C <-> (all D (member(D,B) <-> member(D,C))))). -(all B all C all D (B = intersection(C,D) <-> subset(B,C) & subset(B,D) & (all E (subset(E,C) & subset(E,D) -> subset(E,B))))). end_of_list. ============================== end of input ========================== % clear(auto_denials), because it is incompatiable with FOF reduction. Attempting problem reduction; original problem has = <132,63>. Problem reduction (0.01 sec) gives 4 independent subproblems: ( <172,31> <171,31> <175,33> <180,33> ). Max nnf_size of subproblems is 180; max cnf_max is 33. ============================== FOF REDUCTION MULTISEARCH ============= Subproblem 1 of 4 (negated): ((all B (all C subset(intersection(B,C),B))) & (all B (all C (- subset(B,C) | (all D (- subset(B,D) | subset(B,intersection(C,D))))))) & (all B (all C (all D (member(D,intersection(B,C)) | - member(D,B) | - member(D,C))))) & (all B (all C (all D (member(D,B) | - member(D,intersection(B,C)))))) & (all B (all C (all D (member(D,C) | - member(D,intersection(B,C)))))) & (all B (all C (subset(B,C) | (exists D (member(D,B) & - member(D,C)))))) & (all B (all C ((all D (- member(D,B) | member(D,C))) | - subset(B,C)))) & (all B (all C ((all D (- member(D,B) | member(D,C))) | (exists D (member(D,B) & - member(D,C)))))) & (all B (all C (=(C,B) | - subset(B,C) | - subset(C,B)))) & (all B (all C (subset(B,C) | - =(C,B)))) & (all B (all C (subset(C,B) | - =(C,B)))) & (all B (all C =(intersection(C,B),intersection(B,C)))) & (all B subset(B,B)) & (all B (all C (=(C,B) | (exists D (member(D,B) & - member(D,C))) | (exists D (- member(D,B) & member(D,C)))))) & (all B (all C ((all D (member(D,B) | - member(D,C))) | - =(C,B)))) & (all B (all C ((all D (member(D,B) | - member(D,C))) | (exists D (member(D,B) & - member(D,C))) | (exists D (- member(D,B) & member(D,C)))))) & (all B (all C ((all D (member(D,C) | - member(D,B))) | - =(C,B)))) & (all B (all C ((all D (member(D,C) | - member(D,B))) | (exists D (member(D,B) & - member(D,C))) | (exists D (- member(D,B) & member(D,C)))))) & (exists B (exists C (- subset(B,C) & (exists D (=(intersection(C,D),B))))))). Max_seconds is 30 for this subproblem. Child search process 11560 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). subset(intersection(A,B),A). [assumption]. -subset(A,B) | -subset(A,C) | subset(A,intersection(B,C)). [assumption]. member(A,intersection(B,C)) | -member(A,B) | -member(A,C). [assumption]. member(A,B) | -member(A,intersection(B,C)). [assumption]. member(A,B) | -member(A,intersection(C,B)). [assumption]. subset(A,B) | member(f1(A,B),A). [assumption]. subset(A,B) | -member(f1(A,B),B). [assumption]. -member(A,B) | member(A,C) | -subset(B,C). [assumption]. -member(A,B) | member(A,C) | member(f2(B,C),B). [assumption]. -member(A,B) | member(A,C) | -member(f2(B,C),C). [assumption]. A = B | -subset(B,A) | -subset(A,B). [assumption]. subset(A,B) | B != A. [assumption]. subset(A,B) | A != B. [assumption]. intersection(A,B) = intersection(B,A). [assumption]. subset(A,A). [assumption]. A = B | member(f3(B,A),B) | -member(f4(B,A),B). [assumption]. A = B | member(f3(B,A),B) | member(f4(B,A),A). [assumption]. A = B | -member(f3(B,A),A) | -member(f4(B,A),B). [assumption]. A = B | -member(f3(B,A),A) | member(f4(B,A),A). [assumption]. member(A,B) | -member(A,C) | C != B. [assumption]. member(A,B) | -member(A,C) | member(f5(B,C),B) | -member(f6(B,C),B). [assumption]. member(A,B) | -member(A,C) | member(f5(B,C),B) | member(f6(B,C),C). [assumption]. member(A,B) | -member(A,C) | -member(f5(B,C),C) | -member(f6(B,C),B). [assumption]. member(A,B) | -member(A,C) | -member(f5(B,C),C) | member(f6(B,C),C). [assumption]. member(A,B) | -member(A,C) | B != C. [assumption]. member(A,B) | -member(A,C) | member(f7(C,B),C) | -member(f8(C,B),C). [assumption]. member(A,B) | -member(A,C) | member(f7(C,B),C) | member(f8(C,B),B). [assumption]. member(A,B) | -member(A,C) | -member(f7(C,B),B) | -member(f8(C,B),C). [assumption]. member(A,B) | -member(A,C) | -member(f7(C,B),B) | member(f8(C,B),B). [assumption]. -subset(c1,c2). [assumption]. intersection(c2,c3) = c1. [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ =, member, subset ]). Function symbol precedence: function_order([ c1, c2, c3, intersection, f1, f2, f3, f4, f5, f6, f7, f8 ]). After inverse_order: (no changes). Unfolding symbols: c1/0. Auto_inference settings: % set(paramodulation). % (positive equality literals) % 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: 1 subset(intersection(A,B),A). [assumption]. kept: 2 -subset(A,B) | -subset(A,C) | subset(A,intersection(B,C)). [assumption]. kept: 3 member(A,intersection(B,C)) | -member(A,B) | -member(A,C). [assumption]. kept: 4 member(A,B) | -member(A,intersection(B,C)). [assumption]. kept: 5 member(A,B) | -member(A,intersection(C,B)). [assumption]. kept: 6 subset(A,B) | member(f1(A,B),A). [assumption]. kept: 7 subset(A,B) | -member(f1(A,B),B). [assumption]. kept: 8 -member(A,B) | member(A,C) | -subset(B,C). [assumption]. kept: 9 -member(A,B) | member(A,C) | member(f2(B,C),B). [assumption]. kept: 10 -member(A,B) | member(A,C) | -member(f2(B,C),C). [assumption]. kept: 11 A = B | -subset(B,A) | -subset(A,B). [assumption]. kept: 12 subset(A,B) | B != A. [assumption]. kept: 13 subset(A,B) | A != B. [assumption]. % Operation intersection is commutative; C redundancy checks enabled. kept: 14 intersection(A,B) = intersection(B,A). [assumption]. kept: 15 subset(A,A). [assumption]. kept: 16 A = B | member(f3(B,A),B) | -member(f4(B,A),B). [assumption]. kept: 17 A = B | member(f3(B,A),B) | member(f4(B,A),A). [assumption]. kept: 18 A = B | -member(f3(B,A),A) | -member(f4(B,A),B). [assumption]. kept: 19 A = B | -member(f3(B,A),A) | member(f4(B,A),A). [assumption]. kept: 20 member(A,B) | -member(A,C) | C != B. [assumption]. kept: 21 member(A,B) | -member(A,C) | member(f5(B,C),B) | -member(f6(B,C),B). [assumption]. kept: 22 member(A,B) | -member(A,C) | member(f5(B,C),B) | member(f6(B,C),C). [assumption]. kept: 23 member(A,B) | -member(A,C) | -member(f5(B,C),C) | -member(f6(B,C),B). [assumption]. kept: 24 member(A,B) | -member(A,C) | -member(f5(B,C),C) | member(f6(B,C),C). [assumption]. kept: 25 member(A,B) | -member(A,C) | B != C. [assumption]. kept: 26 member(A,B) | -member(A,C) | member(f7(C,B),C) | -member(f8(C,B),C). [assumption]. kept: 27 member(A,B) | -member(A,C) | member(f7(C,B),C) | member(f8(C,B),B). [assumption]. kept: 28 member(A,B) | -member(A,C) | -member(f7(C,B),B) | -member(f8(C,B),C). [assumption]. kept: 29 member(A,B) | -member(A,C) | -member(f7(C,B),B) | member(f8(C,B),B). [assumption]. kept: 30 -subset(c1,c2). [assumption]. 31 intersection(c2,c3) = c1. [assumption]. kept: 32 c1 = intersection(c2,c3). [copy(31),flip(a)]. kept: 33 -subset(A,B) | subset(A,intersection(B,B)). [factor(2,a,b)]. kept: 34 member(A,intersection(B,B)) | -member(A,B). [factor(3,b,c)]. kept: 35 member(f5(A,B),A) | -member(f5(A,B),B) | -member(f6(A,B),A). [factor(21,a,c)]. kept: 36 member(f5(A,B),A) | -member(f5(A,B),B) | member(f6(A,B),B). [factor(22,a,c)]. kept: 37 member(f8(A,B),B) | -member(f8(A,B),A) | member(f7(A,B),A). [factor(26,b,d)]. kept: 38 member(f8(A,B),B) | -member(f8(A,B),A) | -member(f7(A,B),B). [factor(28,b,d)]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 5. % Level of proof is 2. % Maximum clause weight is 5. % Given clauses 0. 1 subset(intersection(A,B),A). [assumption]. 30 -subset(c1,c2). [assumption]. 31 intersection(c2,c3) = c1. [assumption]. 32 c1 = intersection(c2,c3). [copy(31),flip(a)]. 39 $F. [back_rewrite(30),rewrite([32(1)]),unit_del(a,1)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=0. Generated=53. Kept=37. proofs=1. Usable=0. Sos=29. Demods=2. Limbo=7, Disabled=32. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=15. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=2 (1 lex), Back_demodulated=1. Back_unit_deleted=0. Demod_attempts=284. Demod_rewrites=1. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=7. Nonunit_bsub_feature_tests=39. Megabytes=0.11. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 11560 exit (max_proofs) Wed Feb 25 09:32:32 2009 ============================== continuing FOF reduction multisearch == Subproblem 2 of 4 (negated): ((all B (all C subset(intersection(B,C),B))) & (all B (all C (- subset(B,C) | (all D (- subset(B,D) | subset(B,intersection(C,D))))))) & (all B (all C (all D (member(D,intersection(B,C)) | - member(D,B) | - member(D,C))))) & (all B (all C (all D (member(D,B) | - member(D,intersection(B,C)))))) & (all B (all C (all D (member(D,C) | - member(D,intersection(B,C)))))) & (all B (all C (subset(B,C) | (exists D (member(D,B) & - member(D,C)))))) & (all B (all C ((all D (- member(D,B) | member(D,C))) | - subset(B,C)))) & (all B (all C ((all D (- member(D,B) | member(D,C))) | (exists D (member(D,B) & - member(D,C)))))) & (all B (all C (=(C,B) | - subset(B,C) | - subset(C,B)))) & (all B (all C (subset(B,C) | - =(C,B)))) & (all B (all C (subset(C,B) | - =(C,B)))) & (all B (all C =(intersection(C,B),intersection(B,C)))) & (all B subset(B,B)) & (all B (all C (=(C,B) | (exists D (member(D,B) & - member(D,C))) | (exists D (- member(D,B) & member(D,C)))))) & (all B (all C ((all D (member(D,B) | - member(D,C))) | - =(C,B)))) & (all B (all C ((all D (member(D,B) | - member(D,C))) | (exists D (member(D,B) & - member(D,C))) | (exists D (- member(D,B) & member(D,C)))))) & (all B (all C ((all D (member(D,C) | - member(D,B))) | - =(C,B)))) & (all B (all C ((all D (member(D,C) | - member(D,B))) | (exists D (member(D,B) & - member(D,C))) | (exists D (- member(D,B) & member(D,C)))))) & (exists B (exists C (exists D (=(intersection(C,D),B) & - subset(B,D)))))). Max_seconds is 30 for this subproblem. Child search process 11561 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). subset(intersection(A,B),A). [assumption]. -subset(A,B) | -subset(A,C) | subset(A,intersection(B,C)). [assumption]. member(A,intersection(B,C)) | -member(A,B) | -member(A,C). [assumption]. member(A,B) | -member(A,intersection(B,C)). [assumption]. member(A,B) | -member(A,intersection(C,B)). [assumption]. subset(A,B) | member(f1(A,B),A). [assumption]. subset(A,B) | -member(f1(A,B),B). [assumption]. -member(A,B) | member(A,C) | -subset(B,C). [assumption]. -member(A,B) | member(A,C) | member(f2(B,C),B). [assumption]. -member(A,B) | member(A,C) | -member(f2(B,C),C). [assumption]. A = B | -subset(B,A) | -subset(A,B). [assumption]. subset(A,B) | B != A. [assumption]. subset(A,B) | A != B. [assumption]. intersection(A,B) = intersection(B,A). [assumption]. subset(A,A). [assumption]. A = B | member(f3(B,A),B) | -member(f4(B,A),B). [assumption]. A = B | member(f3(B,A),B) | member(f4(B,A),A). [assumption]. A = B | -member(f3(B,A),A) | -member(f4(B,A),B). [assumption]. A = B | -member(f3(B,A),A) | member(f4(B,A),A). [assumption]. member(A,B) | -member(A,C) | C != B. [assumption]. member(A,B) | -member(A,C) | member(f5(B,C),B) | -member(f6(B,C),B). [assumption]. member(A,B) | -member(A,C) | member(f5(B,C),B) | member(f6(B,C),C). [assumption]. member(A,B) | -member(A,C) | -member(f5(B,C),C) | -member(f6(B,C),B). [assumption]. member(A,B) | -member(A,C) | -member(f5(B,C),C) | member(f6(B,C),C). [assumption]. member(A,B) | -member(A,C) | B != C. [assumption]. member(A,B) | -member(A,C) | member(f7(C,B),C) | -member(f8(C,B),C). [assumption]. member(A,B) | -member(A,C) | member(f7(C,B),C) | member(f8(C,B),B). [assumption]. member(A,B) | -member(A,C) | -member(f7(C,B),B) | -member(f8(C,B),C). [assumption]. member(A,B) | -member(A,C) | -member(f7(C,B),B) | member(f8(C,B),B). [assumption]. intersection(c2,c3) = c1. [assumption]. -subset(c1,c3). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ =, member, subset ]). Function symbol precedence: function_order([ c1, c2, c3, intersection, f1, f2, f3, f4, f5, f6, f7, f8 ]). After inverse_order: (no changes). Unfolding symbols: c1/0. Auto_inference settings: % set(paramodulation). % (positive equality literals) % 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: 1 subset(intersection(A,B),A). [assumption]. kept: 2 -subset(A,B) | -subset(A,C) | subset(A,intersection(B,C)). [assumption]. kept: 3 member(A,intersection(B,C)) | -member(A,B) | -member(A,C). [assumption]. kept: 4 member(A,B) | -member(A,intersection(B,C)). [assumption]. kept: 5 member(A,B) | -member(A,intersection(C,B)). [assumption]. kept: 6 subset(A,B) | member(f1(A,B),A). [assumption]. kept: 7 subset(A,B) | -member(f1(A,B),B). [assumption]. kept: 8 -member(A,B) | member(A,C) | -subset(B,C). [assumption]. kept: 9 -member(A,B) | member(A,C) | member(f2(B,C),B). [assumption]. kept: 10 -member(A,B) | member(A,C) | -member(f2(B,C),C). [assumption]. kept: 11 A = B | -subset(B,A) | -subset(A,B). [assumption]. kept: 12 subset(A,B) | B != A. [assumption]. kept: 13 subset(A,B) | A != B. [assumption]. % Operation intersection is commutative; C redundancy checks enabled. kept: 14 intersection(A,B) = intersection(B,A). [assumption]. kept: 15 subset(A,A). [assumption]. kept: 16 A = B | member(f3(B,A),B) | -member(f4(B,A),B). [assumption]. kept: 17 A = B | member(f3(B,A),B) | member(f4(B,A),A). [assumption]. kept: 18 A = B | -member(f3(B,A),A) | -member(f4(B,A),B). [assumption]. kept: 19 A = B | -member(f3(B,A),A) | member(f4(B,A),A). [assumption]. kept: 20 member(A,B) | -member(A,C) | C != B. [assumption]. kept: 21 member(A,B) | -member(A,C) | member(f5(B,C),B) | -member(f6(B,C),B). [assumption]. kept: 22 member(A,B) | -member(A,C) | member(f5(B,C),B) | member(f6(B,C),C). [assumption]. kept: 23 member(A,B) | -member(A,C) | -member(f5(B,C),C) | -member(f6(B,C),B). [assumption]. kept: 24 member(A,B) | -member(A,C) | -member(f5(B,C),C) | member(f6(B,C),C). [assumption]. kept: 25 member(A,B) | -member(A,C) | B != C. [assumption]. kept: 26 member(A,B) | -member(A,C) | member(f7(C,B),C) | -member(f8(C,B),C). [assumption]. kept: 27 member(A,B) | -member(A,C) | member(f7(C,B),C) | member(f8(C,B),B). [assumption]. kept: 28 member(A,B) | -member(A,C) | -member(f7(C,B),B) | -member(f8(C,B),C). [assumption]. kept: 29 member(A,B) | -member(A,C) | -member(f7(C,B),B) | member(f8(C,B),B). [assumption]. 30 intersection(c2,c3) = c1. [assumption]. kept: 31 c1 = intersection(c2,c3). [copy(30),flip(a)]. 32 -subset(c1,c3). [assumption]. kept: 33 -subset(intersection(c2,c3),c3). [copy(32),rewrite([31(1)])]. kept: 34 -subset(A,B) | subset(A,intersection(B,B)). [factor(2,a,b)]. kept: 35 member(A,intersection(B,B)) | -member(A,B). [factor(3,b,c)]. kept: 36 member(f5(A,B),A) | -member(f5(A,B),B) | -member(f6(A,B),A). [factor(21,a,c)]. kept: 37 member(f5(A,B),A) | -member(f5(A,B),B) | member(f6(A,B),B). [factor(22,a,c)]. kept: 38 member(f8(A,B),B) | -member(f8(A,B),A) | member(f7(A,B),A). [factor(26,b,d)]. kept: 39 member(f8(A,B),B) | -member(f8(A,B),A) | -member(f7(A,B),B). [factor(28,b,d)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 1 subset(intersection(A,B),A). [assumption]. 2 -subset(A,B) | -subset(A,C) | subset(A,intersection(B,C)). [assumption]. 3 member(A,intersection(B,C)) | -member(A,B) | -member(A,C). [assumption]. 4 member(A,B) | -member(A,intersection(B,C)). [assumption]. 5 member(A,B) | -member(A,intersection(C,B)). [assumption]. 6 subset(A,B) | member(f1(A,B),A). [assumption]. 7 subset(A,B) | -member(f1(A,B),B). [assumption]. 8 -member(A,B) | member(A,C) | -subset(B,C). [assumption]. 9 -member(A,B) | member(A,C) | member(f2(B,C),B). [assumption]. 10 -member(A,B) | member(A,C) | -member(f2(B,C),C). [assumption]. 11 A = B | -subset(B,A) | -subset(A,B). [assumption]. 12 subset(A,B) | B != A. [assumption]. 13 subset(A,B) | A != B. [assumption]. 14 intersection(A,B) = intersection(B,A). [assumption]. 15 subset(A,A). [assumption]. 16 A = B | member(f3(B,A),B) | -member(f4(B,A),B). [assumption]. 17 A = B | member(f3(B,A),B) | member(f4(B,A),A). [assumption]. 18 A = B | -member(f3(B,A),A) | -member(f4(B,A),B). [assumption]. 19 A = B | -member(f3(B,A),A) | member(f4(B,A),A). [assumption]. 20 member(A,B) | -member(A,C) | C != B. [assumption]. 21 member(A,B) | -member(A,C) | member(f5(B,C),B) | -member(f6(B,C),B). [assumption]. 22 member(A,B) | -member(A,C) | member(f5(B,C),B) | member(f6(B,C),C). [assumption]. 23 member(A,B) | -member(A,C) | -member(f5(B,C),C) | -member(f6(B,C),B). [assumption]. 24 member(A,B) | -member(A,C) | -member(f5(B,C),C) | member(f6(B,C),C). [assumption]. 25 member(A,B) | -member(A,C) | B != C. [assumption]. 26 member(A,B) | -member(A,C) | member(f7(C,B),C) | -member(f8(C,B),C). [assumption]. 27 member(A,B) | -member(A,C) | member(f7(C,B),C) | member(f8(C,B),B). [assumption]. 28 member(A,B) | -member(A,C) | -member(f7(C,B),B) | -member(f8(C,B),C). [assumption]. 29 member(A,B) | -member(A,C) | -member(f7(C,B),B) | member(f8(C,B),B). [assumption]. 31 c1 = intersection(c2,c3). [copy(30),flip(a)]. 33 -subset(intersection(c2,c3),c3). [copy(32),rewrite([31(1)])]. 34 -subset(A,B) | subset(A,intersection(B,B)). [factor(2,a,b)]. 35 member(A,intersection(B,B)) | -member(A,B). [factor(3,b,c)]. 36 member(f5(A,B),A) | -member(f5(A,B),B) | -member(f6(A,B),A). [factor(21,a,c)]. 37 member(f5(A,B),A) | -member(f5(A,B),B) | member(f6(A,B),B). [factor(22,a,c)]. 38 member(f8(A,B),B) | -member(f8(A,B),A) | member(f7(A,B),A). [factor(26,b,d)]. 39 member(f8(A,B),B) | -member(f8(A,B),A) | -member(f7(A,B),B). [factor(28,b,d)]. end_of_list. formulas(demodulators). 14 intersection(A,B) = intersection(B,A). [assumption]. % (lex-dep) 31 c1 = intersection(c2,c3). [copy(30),flip(a)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=5): 1 subset(intersection(A,B),A). [assumption]. given #2 (I,wt=11): 2 -subset(A,B) | -subset(A,C) | subset(A,intersection(B,C)). [assumption]. given #3 (I,wt=11): 3 member(A,intersection(B,C)) | -member(A,B) | -member(A,C). [assumption]. given #4 (I,wt=8): 4 member(A,B) | -member(A,intersection(B,C)). [assumption]. given #5 (I,wt=8): 5 member(A,B) | -member(A,intersection(C,B)). [assumption]. given #6 (I,wt=8): 6 subset(A,B) | member(f1(A,B),A). [assumption]. given #7 (I,wt=8): 7 subset(A,B) | -member(f1(A,B),B). [assumption]. given #8 (I,wt=9): 8 -member(A,B) | member(A,C) | -subset(B,C). [assumption]. given #9 (I,wt=11): 9 -member(A,B) | member(A,C) | member(f2(B,C),B). [assumption]. given #10 (I,wt=11): 10 -member(A,B) | member(A,C) | -member(f2(B,C),C). [assumption]. given #11 (I,wt=9): 11 A = B | -subset(B,A) | -subset(A,B). [assumption]. given #12 (I,wt=6): 12 subset(A,B) | B != A. [assumption]. given #13 (I,wt=6): 13 subset(A,B) | A != B. [assumption]. given #14 (I,wt=7): 14 intersection(A,B) = intersection(B,A). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.01) seconds. % Length of proof is 8. % Level of proof is 3. % Maximum clause weight is 7. % Given clauses 14. 1 subset(intersection(A,B),A). [assumption]. 14 intersection(A,B) = intersection(B,A). [assumption]. 30 intersection(c2,c3) = c1. [assumption]. 31 c1 = intersection(c2,c3). [copy(30),flip(a)]. 32 -subset(c1,c3). [assumption]. 33 -subset(intersection(c2,c3),c3). [copy(32),rewrite([31(1)])]. 49 subset(intersection(A,B),B). [para(14(a,1),1(a,1))]. 50 $F. [resolve(49,a,33,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=14. Generated=70. Kept=47. proofs=1. Usable=14. Sos=31. Demods=2. Limbo=1, Disabled=31. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=23. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=2 (1 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=346. Demod_rewrites=1. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=19. Nonunit_bsub_feature_tests=61. Megabytes=0.13. User_CPU=0.00, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 11561 exit (max_proofs) Wed Feb 25 09:32:32 2009 ============================== continuing FOF reduction multisearch == Subproblem 3 of 4 (negated): ((all B (all C subset(intersection(B,C),B))) & (all B (all C (- subset(B,C) | (all D (- subset(B,D) | subset(B,intersection(C,D))))))) & (all B (all C (all D (member(D,intersection(B,C)) | - member(D,B) | - member(D,C))))) & (all B (all C (all D (member(D,B) | - member(D,intersection(B,C)))))) & (all B (all C (all D (member(D,C) | - member(D,intersection(B,C)))))) & (all B (all C (subset(B,C) | (exists D (member(D,B) & - member(D,C)))))) & (all B (all C ((all D (- member(D,B) | member(D,C))) | - subset(B,C)))) & (all B (all C ((all D (- member(D,B) | member(D,C))) | (exists D (member(D,B) & - member(D,C)))))) & (all B (all C (=(C,B) | - subset(B,C) | - subset(C,B)))) & (all B (all C (subset(B,C) | - =(C,B)))) & (all B (all C (subset(C,B) | - =(C,B)))) & (all B (all C =(intersection(C,B),intersection(B,C)))) & (all B subset(B,B)) & (all B (all C (=(C,B) | (exists D (member(D,B) & - member(D,C))) | (exists D (- member(D,B) & member(D,C)))))) & (all B (all C ((all D (member(D,B) | - member(D,C))) | - =(C,B)))) & (all B (all C ((all D (member(D,B) | - member(D,C))) | (exists D (member(D,B) & - member(D,C))) | (exists D (- member(D,B) & member(D,C)))))) & (all B (all C ((all D (member(D,C) | - member(D,B))) | - =(C,B)))) & (all B (all C ((all D (member(D,C) | - member(D,B))) | (exists D (member(D,B) & - member(D,C))) | (exists D (- member(D,B) & member(D,C)))))) & (exists B (exists C (exists D (=(intersection(C,D),B) & (exists E (subset(E,C) & subset(E,D) & - subset(E,B)))))))). Max_seconds is 30 for this subproblem. Child search process 11562 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). subset(intersection(A,B),A). [assumption]. -subset(A,B) | -subset(A,C) | subset(A,intersection(B,C)). [assumption]. member(A,intersection(B,C)) | -member(A,B) | -member(A,C). [assumption]. member(A,B) | -member(A,intersection(B,C)). [assumption]. member(A,B) | -member(A,intersection(C,B)). [assumption]. subset(A,B) | member(f1(A,B),A). [assumption]. subset(A,B) | -member(f1(A,B),B). [assumption]. -member(A,B) | member(A,C) | -subset(B,C). [assumption]. -member(A,B) | member(A,C) | member(f2(B,C),B). [assumption]. -member(A,B) | member(A,C) | -member(f2(B,C),C). [assumption]. A = B | -subset(B,A) | -subset(A,B). [assumption]. subset(A,B) | B != A. [assumption]. subset(A,B) | A != B. [assumption]. intersection(A,B) = intersection(B,A). [assumption]. subset(A,A). [assumption]. A = B | member(f3(B,A),B) | -member(f4(B,A),B). [assumption]. A = B | member(f3(B,A),B) | member(f4(B,A),A). [assumption]. A = B | -member(f3(B,A),A) | -member(f4(B,A),B). [assumption]. A = B | -member(f3(B,A),A) | member(f4(B,A),A). [assumption]. member(A,B) | -member(A,C) | C != B. [assumption]. member(A,B) | -member(A,C) | member(f5(B,C),B) | -member(f6(B,C),B). [assumption]. member(A,B) | -member(A,C) | member(f5(B,C),B) | member(f6(B,C),C). [assumption]. member(A,B) | -member(A,C) | -member(f5(B,C),C) | -member(f6(B,C),B). [assumption]. member(A,B) | -member(A,C) | -member(f5(B,C),C) | member(f6(B,C),C). [assumption]. member(A,B) | -member(A,C) | B != C. [assumption]. member(A,B) | -member(A,C) | member(f7(C,B),C) | -member(f8(C,B),C). [assumption]. member(A,B) | -member(A,C) | member(f7(C,B),C) | member(f8(C,B),B). [assumption]. member(A,B) | -member(A,C) | -member(f7(C,B),B) | -member(f8(C,B),C). [assumption]. member(A,B) | -member(A,C) | -member(f7(C,B),B) | member(f8(C,B),B). [assumption]. intersection(c2,c3) = c1. [assumption]. subset(c4,c2). [assumption]. subset(c4,c3). [assumption]. -subset(c4,c1). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ =, member, subset ]). Function symbol precedence: function_order([ c1, c2, c3, c4, intersection, f1, f2, f3, f4, f5, f6, f7, f8 ]). After inverse_order: (no changes). Unfolding symbols: c1/0. Auto_inference settings: % set(paramodulation). % (positive equality literals) % 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: 1 subset(intersection(A,B),A). [assumption]. kept: 2 -subset(A,B) | -subset(A,C) | subset(A,intersection(B,C)). [assumption]. kept: 3 member(A,intersection(B,C)) | -member(A,B) | -member(A,C). [assumption]. kept: 4 member(A,B) | -member(A,intersection(B,C)). [assumption]. kept: 5 member(A,B) | -member(A,intersection(C,B)). [assumption]. kept: 6 subset(A,B) | member(f1(A,B),A). [assumption]. kept: 7 subset(A,B) | -member(f1(A,B),B). [assumption]. kept: 8 -member(A,B) | member(A,C) | -subset(B,C). [assumption]. kept: 9 -member(A,B) | member(A,C) | member(f2(B,C),B). [assumption]. kept: 10 -member(A,B) | member(A,C) | -member(f2(B,C),C). [assumption]. kept: 11 A = B | -subset(B,A) | -subset(A,B). [assumption]. kept: 12 subset(A,B) | B != A. [assumption]. kept: 13 subset(A,B) | A != B. [assumption]. % Operation intersection is commutative; C redundancy checks enabled. kept: 14 intersection(A,B) = intersection(B,A). [assumption]. kept: 15 subset(A,A). [assumption]. kept: 16 A = B | member(f3(B,A),B) | -member(f4(B,A),B). [assumption]. kept: 17 A = B | member(f3(B,A),B) | member(f4(B,A),A). [assumption]. kept: 18 A = B | -member(f3(B,A),A) | -member(f4(B,A),B). [assumption]. kept: 19 A = B | -member(f3(B,A),A) | member(f4(B,A),A). [assumption]. kept: 20 member(A,B) | -member(A,C) | C != B. [assumption]. kept: 21 member(A,B) | -member(A,C) | member(f5(B,C),B) | -member(f6(B,C),B). [assumption]. kept: 22 member(A,B) | -member(A,C) | member(f5(B,C),B) | member(f6(B,C),C). [assumption]. kept: 23 member(A,B) | -member(A,C) | -member(f5(B,C),C) | -member(f6(B,C),B). [assumption]. kept: 24 member(A,B) | -member(A,C) | -member(f5(B,C),C) | member(f6(B,C),C). [assumption]. kept: 25 member(A,B) | -member(A,C) | B != C. [assumption]. kept: 26 member(A,B) | -member(A,C) | member(f7(C,B),C) | -member(f8(C,B),C). [assumption]. kept: 27 member(A,B) | -member(A,C) | member(f7(C,B),C) | member(f8(C,B),B). [assumption]. kept: 28 member(A,B) | -member(A,C) | -member(f7(C,B),B) | -member(f8(C,B),C). [assumption]. kept: 29 member(A,B) | -member(A,C) | -member(f7(C,B),B) | member(f8(C,B),B). [assumption]. 30 intersection(c2,c3) = c1. [assumption]. kept: 31 c1 = intersection(c2,c3). [copy(30),flip(a)]. kept: 32 subset(c4,c2). [assumption]. kept: 33 subset(c4,c3). [assumption]. 34 -subset(c4,c1). [assumption]. kept: 35 -subset(c4,intersection(c2,c3)). [copy(34),rewrite([31(2)])]. kept: 36 -subset(A,B) | subset(A,intersection(B,B)). [factor(2,a,b)]. kept: 37 member(A,intersection(B,B)) | -member(A,B). [factor(3,b,c)]. kept: 38 member(f5(A,B),A) | -member(f5(A,B),B) | -member(f6(A,B),A). [factor(21,a,c)]. kept: 39 member(f5(A,B),A) | -member(f5(A,B),B) | member(f6(A,B),B). [factor(22,a,c)]. kept: 40 member(f8(A,B),B) | -member(f8(A,B),A) | member(f7(A,B),A). [factor(26,b,d)]. kept: 41 member(f8(A,B),B) | -member(f8(A,B),A) | -member(f7(A,B),B). [factor(28,b,d)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 1 subset(intersection(A,B),A). [assumption]. 2 -subset(A,B) | -subset(A,C) | subset(A,intersection(B,C)). [assumption]. 3 member(A,intersection(B,C)) | -member(A,B) | -member(A,C). [assumption]. 4 member(A,B) | -member(A,intersection(B,C)). [assumption]. 5 member(A,B) | -member(A,intersection(C,B)). [assumption]. 6 subset(A,B) | member(f1(A,B),A). [assumption]. 7 subset(A,B) | -member(f1(A,B),B). [assumption]. 8 -member(A,B) | member(A,C) | -subset(B,C). [assumption]. 9 -member(A,B) | member(A,C) | member(f2(B,C),B). [assumption]. 10 -member(A,B) | member(A,C) | -member(f2(B,C),C). [assumption]. 11 A = B | -subset(B,A) | -subset(A,B). [assumption]. 12 subset(A,B) | B != A. [assumption]. 13 subset(A,B) | A != B. [assumption]. 14 intersection(A,B) = intersection(B,A). [assumption]. 15 subset(A,A). [assumption]. 16 A = B | member(f3(B,A),B) | -member(f4(B,A),B). [assumption]. 17 A = B | member(f3(B,A),B) | member(f4(B,A),A). [assumption]. 18 A = B | -member(f3(B,A),A) | -member(f4(B,A),B). [assumption]. 19 A = B | -member(f3(B,A),A) | member(f4(B,A),A). [assumption]. 20 member(A,B) | -member(A,C) | C != B. [assumption]. 21 member(A,B) | -member(A,C) | member(f5(B,C),B) | -member(f6(B,C),B). [assumption]. 22 member(A,B) | -member(A,C) | member(f5(B,C),B) | member(f6(B,C),C). [assumption]. 23 member(A,B) | -member(A,C) | -member(f5(B,C),C) | -member(f6(B,C),B). [assumption]. 24 member(A,B) | -member(A,C) | -member(f5(B,C),C) | member(f6(B,C),C). [assumption]. 25 member(A,B) | -member(A,C) | B != C. [assumption]. 26 member(A,B) | -member(A,C) | member(f7(C,B),C) | -member(f8(C,B),C). [assumption]. 27 member(A,B) | -member(A,C) | member(f7(C,B),C) | member(f8(C,B),B). [assumption]. 28 member(A,B) | -member(A,C) | -member(f7(C,B),B) | -member(f8(C,B),C). [assumption]. 29 member(A,B) | -member(A,C) | -member(f7(C,B),B) | member(f8(C,B),B). [assumption]. 31 c1 = intersection(c2,c3). [copy(30),flip(a)]. 32 subset(c4,c2). [assumption]. 33 subset(c4,c3). [assumption]. 35 -subset(c4,intersection(c2,c3)). [copy(34),rewrite([31(2)])]. 36 -subset(A,B) | subset(A,intersection(B,B)). [factor(2,a,b)]. 37 member(A,intersection(B,B)) | -member(A,B). [factor(3,b,c)]. 38 member(f5(A,B),A) | -member(f5(A,B),B) | -member(f6(A,B),A). [factor(21,a,c)]. 39 member(f5(A,B),A) | -member(f5(A,B),B) | member(f6(A,B),B). [factor(22,a,c)]. 40 member(f8(A,B),B) | -member(f8(A,B),A) | member(f7(A,B),A). [factor(26,b,d)]. 41 member(f8(A,B),B) | -member(f8(A,B),A) | -member(f7(A,B),B). [factor(28,b,d)]. end_of_list. formulas(demodulators). 14 intersection(A,B) = intersection(B,A). [assumption]. % (lex-dep) 31 c1 = intersection(c2,c3). [copy(30),flip(a)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=5): 1 subset(intersection(A,B),A). [assumption]. given #2 (I,wt=11): 2 -subset(A,B) | -subset(A,C) | subset(A,intersection(B,C)). [assumption]. given #3 (I,wt=11): 3 member(A,intersection(B,C)) | -member(A,B) | -member(A,C). [assumption]. given #4 (I,wt=8): 4 member(A,B) | -member(A,intersection(B,C)). [assumption]. given #5 (I,wt=8): 5 member(A,B) | -member(A,intersection(C,B)). [assumption]. given #6 (I,wt=8): 6 subset(A,B) | member(f1(A,B),A). [assumption]. given #7 (I,wt=8): 7 subset(A,B) | -member(f1(A,B),B). [assumption]. given #8 (I,wt=9): 8 -member(A,B) | member(A,C) | -subset(B,C). [assumption]. given #9 (I,wt=11): 9 -member(A,B) | member(A,C) | member(f2(B,C),B). [assumption]. given #10 (I,wt=11): 10 -member(A,B) | member(A,C) | -member(f2(B,C),C). [assumption]. given #11 (I,wt=9): 11 A = B | -subset(B,A) | -subset(A,B). [assumption]. given #12 (I,wt=6): 12 subset(A,B) | B != A. [assumption]. given #13 (I,wt=6): 13 subset(A,B) | A != B. [assumption]. given #14 (I,wt=7): 14 intersection(A,B) = intersection(B,A). [assumption]. given #15 (I,wt=3): 15 subset(A,A). [assumption]. given #16 (I,wt=13): 16 A = B | member(f3(B,A),B) | -member(f4(B,A),B). [assumption]. given #17 (I,wt=13): 17 A = B | member(f3(B,A),B) | member(f4(B,A),A). [assumption]. given #18 (I,wt=13): 18 A = B | -member(f3(B,A),A) | -member(f4(B,A),B). [assumption]. given #19 (I,wt=13): 19 A = B | -member(f3(B,A),A) | member(f4(B,A),A). [assumption]. given #20 (I,wt=9): 20 member(A,B) | -member(A,C) | C != B. [assumption]. given #21 (I,wt=16): 21 member(A,B) | -member(A,C) | member(f5(B,C),B) | -member(f6(B,C),B). [assumption]. given #22 (I,wt=16): 22 member(A,B) | -member(A,C) | member(f5(B,C),B) | member(f6(B,C),C). [assumption]. given #23 (I,wt=16): 23 member(A,B) | -member(A,C) | -member(f5(B,C),C) | -member(f6(B,C),B). [assumption]. given #24 (I,wt=16): 24 member(A,B) | -member(A,C) | -member(f5(B,C),C) | member(f6(B,C),C). [assumption]. given #25 (I,wt=9): 25 member(A,B) | -member(A,C) | B != C. [assumption]. given #26 (I,wt=16): 26 member(A,B) | -member(A,C) | member(f7(C,B),C) | -member(f8(C,B),C). [assumption]. given #27 (I,wt=16): 27 member(A,B) | -member(A,C) | member(f7(C,B),C) | member(f8(C,B),B). [assumption]. given #28 (I,wt=16): 28 member(A,B) | -member(A,C) | -member(f7(C,B),B) | -member(f8(C,B),C). [assumption]. given #29 (I,wt=16): 29 member(A,B) | -member(A,C) | -member(f7(C,B),B) | member(f8(C,B),B). [assumption]. given #30 (I,wt=5): 31 c1 = intersection(c2,c3). [copy(30),flip(a)]. given #31 (I,wt=3): 32 subset(c4,c2). [assumption]. given #32 (I,wt=3): 33 subset(c4,c3). [assumption]. given #33 (I,wt=5): 35 -subset(c4,intersection(c2,c3)). [copy(34),rewrite([31(2)])]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 8. % Level of proof is 3. % Maximum clause weight is 11. % Given clauses 33. 2 -subset(A,B) | -subset(A,C) | subset(A,intersection(B,C)). [assumption]. 30 intersection(c2,c3) = c1. [assumption]. 31 c1 = intersection(c2,c3). [copy(30),flip(a)]. 32 subset(c4,c2). [assumption]. 33 subset(c4,c3). [assumption]. 34 -subset(c4,c1). [assumption]. 35 -subset(c4,intersection(c2,c3)). [copy(34),rewrite([31(2)])]. 81 $F. [ur(2,b,33,a,c,35,a),unit_del(a,32)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=33. Generated=121. Kept=78. proofs=1. Usable=33. Sos=42. Demods=2. Limbo=3, Disabled=33. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=42. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=2 (1 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=660. Demod_rewrites=7. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=64. Nonunit_bsub_feature_tests=118. Megabytes=0.16. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 11562 exit (max_proofs) Wed Feb 25 09:32:32 2009 ============================== continuing FOF reduction multisearch == Subproblem 4 of 4 (negated): ((all B (all C subset(intersection(B,C),B))) & (all B (all C (- subset(B,C) | (all D (- subset(B,D) | subset(B,intersection(C,D))))))) & (all B (all C (all D (member(D,intersection(B,C)) | - member(D,B) | - member(D,C))))) & (all B (all C (all D (member(D,B) | - member(D,intersection(B,C)))))) & (all B (all C (all D (member(D,C) | - member(D,intersection(B,C)))))) & (all B (all C (subset(B,C) | (exists D (member(D,B) & - member(D,C)))))) & (all B (all C ((all D (- member(D,B) | member(D,C))) | - subset(B,C)))) & (all B (all C ((all D (- member(D,B) | member(D,C))) | (exists D (member(D,B) & - member(D,C)))))) & (all B (all C (=(C,B) | - subset(B,C) | - subset(C,B)))) & (all B (all C (subset(B,C) | - =(C,B)))) & (all B (all C (subset(C,B) | - =(C,B)))) & (all B (all C =(intersection(C,B),intersection(B,C)))) & (all B subset(B,B)) & (all B (all C (=(C,B) | (exists D (member(D,B) & - member(D,C))) | (exists D (- member(D,B) & member(D,C)))))) & (all B (all C ((all D (member(D,B) | - member(D,C))) | - =(C,B)))) & (all B (all C ((all D (member(D,B) | - member(D,C))) | (exists D (member(D,B) & - member(D,C))) | (exists D (- member(D,B) & member(D,C)))))) & (all B (all C ((all D (member(D,C) | - member(D,B))) | - =(C,B)))) & (all B (all C ((all D (member(D,C) | - member(D,B))) | (exists D (member(D,B) & - member(D,C))) | (exists D (- member(D,B) & member(D,C)))))) & (exists B (exists C (subset(B,C) & (exists D (- =(intersection(C,D),B) & subset(B,D) & (all E (- subset(E,C) | - subset(E,D) | subset(E,B))))))))). Max_seconds is 30 for this subproblem. Child search process 11563 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). subset(intersection(A,B),A). [assumption]. -subset(A,B) | -subset(A,C) | subset(A,intersection(B,C)). [assumption]. member(A,intersection(B,C)) | -member(A,B) | -member(A,C). [assumption]. member(A,B) | -member(A,intersection(B,C)). [assumption]. member(A,B) | -member(A,intersection(C,B)). [assumption]. subset(A,B) | member(f1(A,B),A). [assumption]. subset(A,B) | -member(f1(A,B),B). [assumption]. -member(A,B) | member(A,C) | -subset(B,C). [assumption]. -member(A,B) | member(A,C) | member(f2(B,C),B). [assumption]. -member(A,B) | member(A,C) | -member(f2(B,C),C). [assumption]. A = B | -subset(B,A) | -subset(A,B). [assumption]. subset(A,B) | B != A. [assumption]. subset(A,B) | A != B. [assumption]. intersection(A,B) = intersection(B,A). [assumption]. subset(A,A). [assumption]. A = B | member(f3(B,A),B) | -member(f4(B,A),B). [assumption]. A = B | member(f3(B,A),B) | member(f4(B,A),A). [assumption]. A = B | -member(f3(B,A),A) | -member(f4(B,A),B). [assumption]. A = B | -member(f3(B,A),A) | member(f4(B,A),A). [assumption]. member(A,B) | -member(A,C) | C != B. [assumption]. member(A,B) | -member(A,C) | member(f5(B,C),B) | -member(f6(B,C),B). [assumption]. member(A,B) | -member(A,C) | member(f5(B,C),B) | member(f6(B,C),C). [assumption]. member(A,B) | -member(A,C) | -member(f5(B,C),C) | -member(f6(B,C),B). [assumption]. member(A,B) | -member(A,C) | -member(f5(B,C),C) | member(f6(B,C),C). [assumption]. member(A,B) | -member(A,C) | B != C. [assumption]. member(A,B) | -member(A,C) | member(f7(C,B),C) | -member(f8(C,B),C). [assumption]. member(A,B) | -member(A,C) | member(f7(C,B),C) | member(f8(C,B),B). [assumption]. member(A,B) | -member(A,C) | -member(f7(C,B),B) | -member(f8(C,B),C). [assumption]. member(A,B) | -member(A,C) | -member(f7(C,B),B) | member(f8(C,B),B). [assumption]. subset(c1,c2). [assumption]. intersection(c2,c3) != c1. [assumption]. subset(c1,c3). [assumption]. -subset(A,c2) | -subset(A,c3) | subset(A,c1). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ =, member, subset ]). Function symbol precedence: function_order([ c1, c2, c3, intersection, f1, f2, f3, f4, f5, f6, f7, f8 ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % 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: 1 subset(intersection(A,B),A). [assumption]. kept: 2 -subset(A,B) | -subset(A,C) | subset(A,intersection(B,C)). [assumption]. kept: 3 member(A,intersection(B,C)) | -member(A,B) | -member(A,C). [assumption]. kept: 4 member(A,B) | -member(A,intersection(B,C)). [assumption]. kept: 5 member(A,B) | -member(A,intersection(C,B)). [assumption]. kept: 6 subset(A,B) | member(f1(A,B),A). [assumption]. kept: 7 subset(A,B) | -member(f1(A,B),B). [assumption]. kept: 8 -member(A,B) | member(A,C) | -subset(B,C). [assumption]. kept: 9 -member(A,B) | member(A,C) | member(f2(B,C),B). [assumption]. kept: 10 -member(A,B) | member(A,C) | -member(f2(B,C),C). [assumption]. kept: 11 A = B | -subset(B,A) | -subset(A,B). [assumption]. kept: 12 subset(A,B) | B != A. [assumption]. kept: 13 subset(A,B) | A != B. [assumption]. % Operation intersection is commutative; C redundancy checks enabled. kept: 14 intersection(A,B) = intersection(B,A). [assumption]. kept: 15 subset(A,A). [assumption]. kept: 16 A = B | member(f3(B,A),B) | -member(f4(B,A),B). [assumption]. kept: 17 A = B | member(f3(B,A),B) | member(f4(B,A),A). [assumption]. kept: 18 A = B | -member(f3(B,A),A) | -member(f4(B,A),B). [assumption]. kept: 19 A = B | -member(f3(B,A),A) | member(f4(B,A),A). [assumption]. kept: 20 member(A,B) | -member(A,C) | C != B. [assumption]. kept: 21 member(A,B) | -member(A,C) | member(f5(B,C),B) | -member(f6(B,C),B). [assumption]. kept: 22 member(A,B) | -member(A,C) | member(f5(B,C),B) | member(f6(B,C),C). [assumption]. kept: 23 member(A,B) | -member(A,C) | -member(f5(B,C),C) | -member(f6(B,C),B). [assumption]. kept: 24 member(A,B) | -member(A,C) | -member(f5(B,C),C) | member(f6(B,C),C). [assumption]. kept: 25 member(A,B) | -member(A,C) | B != C. [assumption]. kept: 26 member(A,B) | -member(A,C) | member(f7(C,B),C) | -member(f8(C,B),C). [assumption]. kept: 27 member(A,B) | -member(A,C) | member(f7(C,B),C) | member(f8(C,B),B). [assumption]. kept: 28 member(A,B) | -member(A,C) | -member(f7(C,B),B) | -member(f8(C,B),C). [assumption]. kept: 29 member(A,B) | -member(A,C) | -member(f7(C,B),B) | member(f8(C,B),B). [assumption]. kept: 30 subset(c1,c2). [assumption]. kept: 31 intersection(c2,c3) != c1. [assumption]. kept: 32 subset(c1,c3). [assumption]. kept: 33 -subset(A,c2) | -subset(A,c3) | subset(A,c1). [assumption]. kept: 34 -subset(A,B) | subset(A,intersection(B,B)). [factor(2,a,b)]. kept: 35 member(A,intersection(B,B)) | -member(A,B). [factor(3,b,c)]. kept: 36 member(f5(A,B),A) | -member(f5(A,B),B) | -member(f6(A,B),A). [factor(21,a,c)]. kept: 37 member(f5(A,B),A) | -member(f5(A,B),B) | member(f6(A,B),B). [factor(22,a,c)]. kept: 38 member(f8(A,B),B) | -member(f8(A,B),A) | member(f7(A,B),A). [factor(26,b,d)]. kept: 39 member(f8(A,B),B) | -member(f8(A,B),A) | -member(f7(A,B),B). [factor(28,b,d)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 1 subset(intersection(A,B),A). [assumption]. 2 -subset(A,B) | -subset(A,C) | subset(A,intersection(B,C)). [assumption]. 3 member(A,intersection(B,C)) | -member(A,B) | -member(A,C). [assumption]. 4 member(A,B) | -member(A,intersection(B,C)). [assumption]. 5 member(A,B) | -member(A,intersection(C,B)). [assumption]. 6 subset(A,B) | member(f1(A,B),A). [assumption]. 7 subset(A,B) | -member(f1(A,B),B). [assumption]. 8 -member(A,B) | member(A,C) | -subset(B,C). [assumption]. 9 -member(A,B) | member(A,C) | member(f2(B,C),B). [assumption]. 10 -member(A,B) | member(A,C) | -member(f2(B,C),C). [assumption]. 11 A = B | -subset(B,A) | -subset(A,B). [assumption]. 12 subset(A,B) | B != A. [assumption]. 13 subset(A,B) | A != B. [assumption]. 14 intersection(A,B) = intersection(B,A). [assumption]. 15 subset(A,A). [assumption]. 16 A = B | member(f3(B,A),B) | -member(f4(B,A),B). [assumption]. 17 A = B | member(f3(B,A),B) | member(f4(B,A),A). [assumption]. 18 A = B | -member(f3(B,A),A) | -member(f4(B,A),B). [assumption]. 19 A = B | -member(f3(B,A),A) | member(f4(B,A),A). [assumption]. 20 member(A,B) | -member(A,C) | C != B. [assumption]. 21 member(A,B) | -member(A,C) | member(f5(B,C),B) | -member(f6(B,C),B). [assumption]. 22 member(A,B) | -member(A,C) | member(f5(B,C),B) | member(f6(B,C),C). [assumption]. 23 member(A,B) | -member(A,C) | -member(f5(B,C),C) | -member(f6(B,C),B). [assumption]. 24 member(A,B) | -member(A,C) | -member(f5(B,C),C) | member(f6(B,C),C). [assumption]. 25 member(A,B) | -member(A,C) | B != C. [assumption]. 26 member(A,B) | -member(A,C) | member(f7(C,B),C) | -member(f8(C,B),C). [assumption]. 27 member(A,B) | -member(A,C) | member(f7(C,B),C) | member(f8(C,B),B). [assumption]. 28 member(A,B) | -member(A,C) | -member(f7(C,B),B) | -member(f8(C,B),C). [assumption]. 29 member(A,B) | -member(A,C) | -member(f7(C,B),B) | member(f8(C,B),B). [assumption]. 30 subset(c1,c2). [assumption]. 31 intersection(c2,c3) != c1. [assumption]. 32 subset(c1,c3). [assumption]. 33 -subset(A,c2) | -subset(A,c3) | subset(A,c1). [assumption]. 34 -subset(A,B) | subset(A,intersection(B,B)). [factor(2,a,b)]. 35 member(A,intersection(B,B)) | -member(A,B). [factor(3,b,c)]. 36 member(f5(A,B),A) | -member(f5(A,B),B) | -member(f6(A,B),A). [factor(21,a,c)]. 37 member(f5(A,B),A) | -member(f5(A,B),B) | member(f6(A,B),B). [factor(22,a,c)]. 38 member(f8(A,B),B) | -member(f8(A,B),A) | member(f7(A,B),A). [factor(26,b,d)]. 39 member(f8(A,B),B) | -member(f8(A,B),A) | -member(f7(A,B),B). [factor(28,b,d)]. end_of_list. formulas(demodulators). 14 intersection(A,B) = intersection(B,A). [assumption]. % (lex-dep) end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=5): 1 subset(intersection(A,B),A). [assumption]. given #2 (I,wt=11): 2 -subset(A,B) | -subset(A,C) | subset(A,intersection(B,C)). [assumption]. given #3 (I,wt=11): 3 member(A,intersection(B,C)) | -member(A,B) | -member(A,C). [assumption]. given #4 (I,wt=8): 4 member(A,B) | -member(A,intersection(B,C)). [assumption]. given #5 (I,wt=8): 5 member(A,B) | -member(A,intersection(C,B)). [assumption]. given #6 (I,wt=8): 6 subset(A,B) | member(f1(A,B),A). [assumption]. given #7 (I,wt=8): 7 subset(A,B) | -member(f1(A,B),B). [assumption]. given #8 (I,wt=9): 8 -member(A,B) | member(A,C) | -subset(B,C). [assumption]. given #9 (I,wt=11): 9 -member(A,B) | member(A,C) | member(f2(B,C),B). [assumption]. given #10 (I,wt=11): 10 -member(A,B) | member(A,C) | -member(f2(B,C),C). [assumption]. given #11 (I,wt=9): 11 A = B | -subset(B,A) | -subset(A,B). [assumption]. given #12 (I,wt=6): 12 subset(A,B) | B != A. [assumption]. given #13 (I,wt=6): 13 subset(A,B) | A != B. [assumption]. given #14 (I,wt=7): 14 intersection(A,B) = intersection(B,A). [assumption]. given #15 (I,wt=3): 15 subset(A,A). [assumption]. given #16 (I,wt=13): 16 A = B | member(f3(B,A),B) | -member(f4(B,A),B). [assumption]. given #17 (I,wt=13): 17 A = B | member(f3(B,A),B) | member(f4(B,A),A). [assumption]. given #18 (I,wt=13): 18 A = B | -member(f3(B,A),A) | -member(f4(B,A),B). [assumption]. given #19 (I,wt=13): 19 A = B | -member(f3(B,A),A) | member(f4(B,A),A). [assumption]. given #20 (I,wt=9): 20 member(A,B) | -member(A,C) | C != B. [assumption]. given #21 (I,wt=16): 21 member(A,B) | -member(A,C) | member(f5(B,C),B) | -member(f6(B,C),B). [assumption]. given #22 (I,wt=16): 22 member(A,B) | -member(A,C) | member(f5(B,C),B) | member(f6(B,C),C). [assumption]. given #23 (I,wt=16): 23 member(A,B) | -member(A,C) | -member(f5(B,C),C) | -member(f6(B,C),B). [assumption]. given #24 (I,wt=16): 24 member(A,B) | -member(A,C) | -member(f5(B,C),C) | member(f6(B,C),C). [assumption]. given #25 (I,wt=9): 25 member(A,B) | -member(A,C) | B != C. [assumption]. given #26 (I,wt=16): 26 member(A,B) | -member(A,C) | member(f7(C,B),C) | -member(f8(C,B),C). [assumption]. given #27 (I,wt=16): 27 member(A,B) | -member(A,C) | member(f7(C,B),C) | member(f8(C,B),B). [assumption]. given #28 (I,wt=16): 28 member(A,B) | -member(A,C) | -member(f7(C,B),B) | -member(f8(C,B),C). [assumption]. given #29 (I,wt=16): 29 member(A,B) | -member(A,C) | -member(f7(C,B),B) | member(f8(C,B),B). [assumption]. given #30 (I,wt=3): 30 subset(c1,c2). [assumption]. given #31 (I,wt=5): 31 intersection(c2,c3) != c1. [assumption]. given #32 (I,wt=3): 32 subset(c1,c3). [assumption]. given #33 (I,wt=9): 33 -subset(A,c2) | -subset(A,c3) | subset(A,c1). [assumption]. given #34 (I,wt=8): 34 -subset(A,B) | subset(A,intersection(B,B)). [factor(2,a,b)]. given #35 (I,wt=8): 35 member(A,intersection(B,B)) | -member(A,B). [factor(3,b,c)]. given #36 (I,wt=15): 36 member(f5(A,B),A) | -member(f5(A,B),B) | -member(f6(A,B),A). [factor(21,a,c)]. given #37 (I,wt=15): 37 member(f5(A,B),A) | -member(f5(A,B),B) | member(f6(A,B),B). [factor(22,a,c)]. given #38 (I,wt=15): 38 member(f8(A,B),B) | -member(f8(A,B),A) | member(f7(A,B),A). [factor(26,b,d)]. given #39 (I,wt=15): 39 member(f8(A,B),B) | -member(f8(A,B),A) | -member(f7(A,B),B). [factor(28,b,d)]. given #40 (A,wt=12): 40 -subset(intersection(A,B),C) | subset(intersection(A,B),intersection(A,C)). [resolve(2,a,1,a)]. given #41 (T,wt=5): 49 subset(intersection(A,B),B). [para(14(a,1),1(a,1))]. given #42 (T,wt=5): 79 subset(c1,intersection(c3,c3)). [resolve(34,a,32,a)]. given #43 (T,wt=5): 80 subset(c1,intersection(c2,c2)). [resolve(34,a,30,a)]. given #44 (T,wt=5): 81 subset(A,intersection(A,A)). [resolve(34,a,15,a)]. given #45 (A,wt=12): 41 -subset(intersection(A,B),C) | subset(intersection(A,B),intersection(C,A)). [resolve(2,b,1,a)]. given #46 (T,wt=5): 105 intersection(A,A) = A. [resolve(81,a,11,c),flip(a),unit_del(b,1)]. given #47 (T,wt=6): 68 c2 = c1 | -subset(c2,c1). [resolve(30,a,11,c),flip(a)]. given #48 (T,wt=6): 69 -member(A,c1) | member(A,c2). [resolve(30,a,8,c)]. given #49 (T,wt=6): 72 c3 = c1 | -subset(c3,c1). [resolve(32,a,11,c),flip(a)]. given #50 (A,wt=13): 42 member(f1(A,B),A) | -subset(A,C) | subset(A,intersection(C,B)). [resolve(6,a,2,b)]. given #51 (T,wt=6): 73 -member(A,c1) | member(A,c3). [resolve(32,a,8,c)]. given #52 (T,wt=6): 76 -subset(c3,c2) | subset(c3,c1). [resolve(33,b,15,a)]. given #53 (T,wt=7): 48 subset(intersection(A,B),intersection(B,A)). [resolve(14,a,13,b)]. given #54 (T,wt=8): 50 -subset(A,B) | subset(A,intersection(B,A)). [resolve(15,a,2,b)]. given #55 (A,wt=13): 43 member(f1(A,B),A) | -subset(A,C) | subset(A,intersection(B,C)). [resolve(6,a,2,a)]. given #56 (T,wt=5): 125 subset(c1,intersection(c1,c3)). [resolve(50,a,32,a),rewrite([14(4)])]. given #57 (T,wt=5): 126 subset(c1,intersection(c1,c2)). [resolve(50,a,30,a),rewrite([14(4)])]. given #58 (T,wt=5): 135 intersection(c1,c3) = c1. [resolve(125,a,11,c),flip(a),unit_del(b,1)]. given #59 (T,wt=5): 139 intersection(c1,c2) = c1. [resolve(126,a,11,c),flip(a),unit_del(b,1)]. given #60 (A,wt=11): 44 -member(A,B) | member(A,C) | member(f1(B,C),B). [resolve(8,c,6,a)]. given #61 (T,wt=8): 51 -subset(A,B) | subset(A,intersection(A,B)). [resolve(15,a,2,a)]. given #62 (T,wt=8): 70 -subset(c1,A) | subset(c1,intersection(A,c2)). [resolve(30,a,2,b)]. given #63 (T,wt=5): 142 subset(c1,intersection(c2,c3)). [resolve(70,a,32,a),rewrite([14(4)])]. given #64 (T,wt=7): 143 subset(c1,intersection(c2,intersection(c2,c3))). [resolve(142,a,70,a),rewrite([14(6)])]. given #65 (A,wt=11): 45 A = B | -subset(A,B) | member(f1(B,A),B). [resolve(11,b,6,a)]. given #66 (F,wt=5): 147 -subset(intersection(c2,c3),c1). [resolve(142,a,11,c),flip(a),unit_del(a,31)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 13. % Level of proof is 4. % Maximum clause weight is 11. % Given clauses 66. 1 subset(intersection(A,B),A). [assumption]. 2 -subset(A,B) | -subset(A,C) | subset(A,intersection(B,C)). [assumption]. 11 A = B | -subset(B,A) | -subset(A,B). [assumption]. 14 intersection(A,B) = intersection(B,A). [assumption]. 30 subset(c1,c2). [assumption]. 31 intersection(c2,c3) != c1. [assumption]. 32 subset(c1,c3). [assumption]. 33 -subset(A,c2) | -subset(A,c3) | subset(A,c1). [assumption]. 49 subset(intersection(A,B),B). [para(14(a,1),1(a,1))]. 70 -subset(c1,A) | subset(c1,intersection(A,c2)). [resolve(30,a,2,b)]. 142 subset(c1,intersection(c2,c3)). [resolve(70,a,32,a),rewrite([14(4)])]. 147 -subset(intersection(c2,c3),c1). [resolve(142,a,11,c),flip(a),unit_del(a,31)]. 164 $F. [ur(33,b,49,a,c,147,a),unit_del(a,1)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=66. Generated=338. Kept=163. proofs=1. Usable=59. Sos=75. Demods=4. Limbo=0, Disabled=62. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=174. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=4 (1 lex), Back_demodulated=29. Back_unit_deleted=0. Demod_attempts=2031. Demod_rewrites=122. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=392. Nonunit_bsub_feature_tests=321. Megabytes=0.22. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 11563 exit (max_proofs) Wed Feb 25 09:32:32 2009 ============================== end of multisearch ==================== All 4 subproblems have been proved, so we are done. Total user_CPU=0.03, system_CPU=0.01, wall_clock=0. THEOREM PROVED Exiting. Process 11559 exit (max_proofs) Wed Feb 25 09:32:32 2009