============================== FOF-Prover9 =========================== FOF-Prover9 (32) version November-2006, November 2006. Process 3779 was started by mccune on cleo.thornwood, Wed Nov 22 11:23:39 2006 The command was "/home/mccune/bin/fof-prover9 -f SET598+3.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file SET598+3.in 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.00 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))))))). Child search process 3780 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: Relation symbol precedence: lex([ member, subset, = ]). Function symbol precedence: lex([ 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(paramodulation) -> set(back_demod). % 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). % Operation intersection is commutative; C redundancy checks enabled. ============================== 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. Weight_deleted=0. Literals_deleted=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 3780 exit (max_proofs) Wed Nov 22 11:23:39 2006 ============================== 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)))))). Child search process 3781 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: Relation symbol precedence: lex([ member, subset, = ]). Function symbol precedence: lex([ 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(paramodulation) -> set(back_demod). % 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). % Operation intersection 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). 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.00) 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. Weight_deleted=0. Literals_deleted=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.12. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 3781 exit (max_proofs) Wed Nov 22 11:23:39 2006 ============================== 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)))))))). Child search process 3782 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: Relation symbol precedence: lex([ member, subset, = ]). Function symbol precedence: lex([ 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(paramodulation) -> set(back_demod). % 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). % Operation intersection 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). 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.00 (+ 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))]. 72 $F. [ur(2,b,33,a,c,35,a),unit_del(a,32)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=33. Generated=126. Kept=69. proofs=1. Usable=33. Sos=33. Demods=2. Limbo=3, Disabled=33. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=56. 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=645. Demod_rewrites=11. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=64. Nonunit_bsub_feature_tests=108. Megabytes=0.14. User_CPU=0.00, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 3782 exit (max_proofs) Wed Nov 22 11:23:39 2006 ============================== 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))))))))). Child search process 3783 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: Relation symbol precedence: lex([ member, subset, = ]). Function symbol precedence: lex([ 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(paramodulation) -> set(back_demod). % 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). % Operation intersection 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). 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 (T,wt=5): 49 subset(intersection(A,B),B). [para(14(a,1),1(a,1))]. given #41 (A,wt=12): 40 -subset(intersection(A,B),C) | subset(intersection(A,B),intersection(A,C)). [resolve(2,a,1,a)]. given #42 (F,wt=5): 72 subset(c1,intersection(c3,c3)). [resolve(34,a,32,a)]. given #43 (F,wt=5): 73 subset(c1,intersection(c2,c2)). [resolve(34,a,30,a)]. given #44 (T,wt=5): 74 subset(A,intersection(A,A)). [resolve(34,a,15,a)]. given #45 (T,wt=5): 97 intersection(A,A) = A. [resolve(74,a,11,c),flip(a),unit_del(b,1)]. given #46 (A,wt=12): 41 -subset(intersection(A,B),C) | subset(intersection(A,B),intersection(C,A)). [resolve(2,b,1,a)]. given #47 (F,wt=6): 59 c2 = c1 | -subset(c2,c1). [resolve(30,a,11,c),flip(a)]. given #48 (F,wt=6): 60 -member(A,c1) | member(A,c2). [resolve(30,a,8,c)]. given #49 (T,wt=6): 65 c3 = c1 | -subset(c3,c1). [resolve(32,a,11,c),flip(a)]. given #50 (T,wt=6): 66 -member(A,c1) | member(A,c3). [resolve(32,a,8,c)]. given #51 (A,wt=13): 42 member(f1(A,B),A) | -subset(A,C) | subset(A,intersection(C,B)). [resolve(6,a,2,b)]. given #52 (F,wt=6): 69 -subset(c3,c2) | subset(c3,c1). [resolve(33,b,15,a)]. given #53 (F,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 (T,wt=5): 114 subset(c1,intersection(c1,c3)). [resolve(50,a,32,a),rewrite(14(4))]. given #56 (A,wt=13): 43 member(f1(A,B),A) | -subset(A,C) | subset(A,intersection(B,C)). [resolve(6,a,2,a)]. given #57 (F,wt=5): 115 subset(c1,intersection(c1,c2)). [resolve(50,a,30,a),rewrite(14(4))]. given #58 (F,wt=5): 119 intersection(c1,c3) = c1. [resolve(114,a,11,c),flip(a),unit_del(b,1)]. given #59 (T,wt=5): 127 intersection(c1,c2) = c1. [resolve(115,a,11,c),flip(a),unit_del(b,1)]. given #60 (T,wt=8): 51 -subset(A,B) | subset(A,intersection(A,B)). [resolve(15,a,2,a)]. given #61 (A,wt=11): 44 -member(A,B) | member(A,C) | member(f1(B,C),B). [resolve(8,c,6,a)]. given #62 (F,wt=8): 61 -subset(c1,A) | subset(c1,intersection(A,c2)). [resolve(30,a,2,b)]. given #63 (F,wt=5): 129 subset(c1,intersection(c2,c3)). [resolve(61,a,32,a),rewrite(14(4))]. given #64 (T,wt=7): 130 subset(c1,intersection(c2,intersection(c2,c3))). [resolve(129,a,61,a),rewrite(14(6))]. given #65 (T,wt=7): 131 subset(c1,intersection(c1,intersection(c2,c3))). [resolve(129,a,51,a)]. given #66 (A,wt=11): 45 A = B | -subset(A,B) | member(f1(B,A),B). [resolve(11,b,6,a)]. given #67 (F,wt=5): 134 -subset(intersection(c2,c3),c1). [resolve(129,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 67. 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))]. 61 -subset(c1,A) | subset(c1,intersection(A,c2)). [resolve(30,a,2,b)]. 129 subset(c1,intersection(c2,c3)). [resolve(61,a,32,a),rewrite(14(4))]. 134 -subset(intersection(c2,c3),c1). [resolve(129,a,11,c),flip(a),unit_del(a,31)]. 156 $F. [ur(33,b,49,a,c,134,a),unit_del(a,1)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=67. Generated=366. Kept=155. proofs=1. Usable=59. Sos=64. Demods=5. Limbo=0, Disabled=65. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=210. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=5 (1 lex), Back_demodulated=32. Back_unit_deleted=0. Demod_attempts=2226. Demod_rewrites=156. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=407. Nonunit_bsub_feature_tests=301. Megabytes=0.20. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 3783 exit (max_proofs) Wed Nov 22 11:23:39 2006 ============================== end of multisearch ==================== All 4 subproblems have been proved, so we are done. Total user_CPU=0.03, system_CPU=0.00, wall_clock=0. THEOREM PROVED Exiting. Process 3779 exit (max_proofs) Wed Nov 22 11:23:39 2006