============================== FOF-Prover9 =========================== FOF-Prover9 (32) version November-2006, November 2006. Process 3773 was started by mccune on cleo.thornwood, Wed Nov 22 11:23:39 2006 The command was "/home/mccune/bin/fof-prover9 -f SET587+3.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file SET587+3.in set(prolog_style_variables). formulas(assumptions). (all B all C ((all D (member(D,B) <-> member(D,C))) -> B = C)). (all B all C all D (member(D,difference(B,C)) <-> member(D,B) & -member(D,C))). (all B (-member(B,empty_set))). (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 (B = C <-> (all D (member(D,B) <-> member(D,C))))). (all B (subset(B,B))). (all B (empty(B) <-> (all C (-member(C,B))))). -(all B all C (difference(B,C) = empty_set <-> subset(B,C))). end_of_list. ============================== end of input ========================== % clear(auto_denials), because it is incompatiable with FOF reduction. Attempting problem reduction; original problem has = <124,57>. Problem reduction (0.00 sec) gives 2 independent subproblems: ( <190,36> <190,36> ). Max nnf_size of subproblems is 190; max cnf_max is 36. ============================== FOF REDUCTION MULTISEARCH ============= Subproblem 1 of 2 (negated): ((all B (all C ((exists D (member(D,B) & - member(D,C))) | (exists D (- member(D,B) & member(D,C))) | =(C,B)))) & (all B (all C (all D (member(D,difference(B,C)) | - member(D,B) | member(D,C))))) & (all B (all C (all D (member(D,B) | - member(D,difference(B,C)))))) & (all B (all C (all D (- member(D,C) | - member(D,difference(B,C)))))) & (all B - member(B,empty_set)) & (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 (=(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)))))) & (all B subset(B,B)) & (all B (empty(B) | (exists C member(C,B)))) & (all B ((all C - member(C,B)) | - empty(B))) & (all B ((all C - member(C,B)) | (exists C member(C,B)))) & (exists B (exists C (=(difference(B,C),empty_set) & - subset(B,C))))). Child search process 3774 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). member(f1(A,B),A) | -member(f2(A,B),A) | B = A. [assumption]. member(f1(A,B),A) | member(f2(A,B),B) | B = A. [assumption]. -member(f1(A,B),B) | -member(f2(A,B),A) | B = A. [assumption]. -member(f1(A,B),B) | member(f2(A,B),B) | B = A. [assumption]. member(A,difference(B,C)) | -member(A,B) | member(A,C). [assumption]. member(A,B) | -member(A,difference(B,C)). [assumption]. -member(A,B) | -member(A,difference(C,B)). [assumption]. -member(A,empty_set). [assumption]. subset(A,B) | member(f3(A,B),A). [assumption]. subset(A,B) | -member(f3(A,B),B). [assumption]. -member(A,B) | member(A,C) | -subset(B,C). [assumption]. -member(A,B) | member(A,C) | member(f4(B,C),B). [assumption]. -member(A,B) | member(A,C) | -member(f4(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]. A = B | member(f5(B,A),B) | -member(f6(B,A),B). [assumption]. A = B | member(f5(B,A),B) | member(f6(B,A),A). [assumption]. A = B | -member(f5(B,A),A) | -member(f6(B,A),B). [assumption]. A = B | -member(f5(B,A),A) | member(f6(B,A),A). [assumption]. member(A,B) | -member(A,C) | C != B. [assumption]. member(A,B) | -member(A,C) | member(f7(B,C),B) | -member(f8(B,C),B). [assumption]. member(A,B) | -member(A,C) | member(f7(B,C),B) | member(f8(B,C),C). [assumption]. member(A,B) | -member(A,C) | -member(f7(B,C),C) | -member(f8(B,C),B). [assumption]. member(A,B) | -member(A,C) | -member(f7(B,C),C) | member(f8(B,C),C). [assumption]. member(A,B) | -member(A,C) | B != C. [assumption]. member(A,B) | -member(A,C) | member(f9(C,B),C) | -member(f10(C,B),C). [assumption]. member(A,B) | -member(A,C) | member(f9(C,B),C) | member(f10(C,B),B). [assumption]. member(A,B) | -member(A,C) | -member(f9(C,B),B) | -member(f10(C,B),C). [assumption]. member(A,B) | -member(A,C) | -member(f9(C,B),B) | member(f10(C,B),B). [assumption]. subset(A,A). [assumption]. empty(A) | member(f11(A),A). [assumption]. -member(A,B) | -empty(B). [assumption]. -member(A,B) | member(f12(B),B). [assumption]. difference(c1,c2) = empty_set. [assumption]. -subset(c1,c2). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating empty/1 1 -member(A,B) | -empty(B). [assumption]. 2 empty(A) | member(f11(A),A). [assumption]. Derived: -member(A,B) | member(f11(B),B). [resolve(1,b,2,a)]. ============================== end predicate elimination ============= Term ordering decisions: Relation symbol precedence: lex([ member, subset, =, empty ]). Function symbol precedence: lex([ empty_set, c1, c2, difference, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12 ]). After inverse_order: (no changes). Unfolding symbols: empty_set/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). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 3 member(f1(A,B),A) | -member(f2(A,B),A) | B = A. [assumption]. 4 member(f1(A,B),A) | member(f2(A,B),B) | B = A. [assumption]. 5 -member(f1(A,B),B) | -member(f2(A,B),A) | B = A. [assumption]. 6 -member(f1(A,B),B) | member(f2(A,B),B) | B = A. [assumption]. 7 member(A,difference(B,C)) | -member(A,B) | member(A,C). [assumption]. 8 member(A,B) | -member(A,difference(B,C)). [assumption]. 9 -member(A,B) | -member(A,difference(C,B)). [assumption]. 11 subset(A,B) | member(f3(A,B),A). [assumption]. 12 subset(A,B) | -member(f3(A,B),B). [assumption]. 13 -member(A,B) | member(A,C) | -subset(B,C). [assumption]. 14 -member(A,B) | member(A,C) | member(f4(B,C),B). [assumption]. 15 -member(A,B) | member(A,C) | -member(f4(B,C),C). [assumption]. 16 A = B | -subset(B,A) | -subset(A,B). [assumption]. 17 subset(A,B) | B != A. [assumption]. 18 subset(A,B) | A != B. [assumption]. 19 A = B | member(f5(B,A),B) | -member(f6(B,A),B). [assumption]. 20 A = B | member(f5(B,A),B) | member(f6(B,A),A). [assumption]. 21 A = B | -member(f5(B,A),A) | -member(f6(B,A),B). [assumption]. 22 A = B | -member(f5(B,A),A) | member(f6(B,A),A). [assumption]. 23 member(A,B) | -member(A,C) | C != B. [assumption]. 24 member(A,B) | -member(A,C) | member(f7(B,C),B) | -member(f8(B,C),B). [assumption]. 25 member(A,B) | -member(A,C) | member(f7(B,C),B) | member(f8(B,C),C). [assumption]. 26 member(A,B) | -member(A,C) | -member(f7(B,C),C) | -member(f8(B,C),B). [assumption]. 27 member(A,B) | -member(A,C) | -member(f7(B,C),C) | member(f8(B,C),C). [assumption]. 28 member(A,B) | -member(A,C) | B != C. [assumption]. 29 member(A,B) | -member(A,C) | member(f9(C,B),C) | -member(f10(C,B),C). [assumption]. 30 member(A,B) | -member(A,C) | member(f9(C,B),C) | member(f10(C,B),B). [assumption]. 31 member(A,B) | -member(A,C) | -member(f9(C,B),B) | -member(f10(C,B),C). [assumption]. 32 member(A,B) | -member(A,C) | -member(f9(C,B),B) | member(f10(C,B),B). [assumption]. 33 subset(A,A). [assumption]. 34 -member(A,B) | member(f12(B),B). [assumption]. 36 empty_set = difference(c1,c2). [copy(35),flip(a)]. 37 -subset(c1,c2). [assumption]. 38 -member(A,B) | member(f11(B),B). [resolve(1,b,2,a)]. 39 member(f7(A,B),A) | -member(f7(A,B),B) | -member(f8(A,B),A). [factor(24,a,c)]. 40 member(f7(A,B),A) | -member(f7(A,B),B) | member(f8(A,B),B). [factor(25,a,c)]. 41 member(f10(A,B),B) | -member(f10(A,B),A) | member(f9(A,B),A). [factor(29,b,d)]. 42 member(f10(A,B),B) | -member(f10(A,B),A) | -member(f9(A,B),B). [factor(31,b,d)]. 43 -member(A,difference(c1,c2)). [back_rewrite(10),rewrite(36(1))]. end_of_list. formulas(demodulators). 36 empty_set = difference(c1,c2). [copy(35),flip(a)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=13): 3 member(f1(A,B),A) | -member(f2(A,B),A) | B = A. [assumption]. given #2 (I,wt=13): 4 member(f1(A,B),A) | member(f2(A,B),B) | B = A. [assumption]. given #3 (I,wt=13): 5 -member(f1(A,B),B) | -member(f2(A,B),A) | B = A. [assumption]. given #4 (I,wt=13): 6 -member(f1(A,B),B) | member(f2(A,B),B) | B = A. [assumption]. given #5 (I,wt=11): 7 member(A,difference(B,C)) | -member(A,B) | member(A,C). [assumption]. given #6 (I,wt=8): 8 member(A,B) | -member(A,difference(B,C)). [assumption]. given #7 (I,wt=8): 9 -member(A,B) | -member(A,difference(C,B)). [assumption]. given #8 (I,wt=8): 11 subset(A,B) | member(f3(A,B),A). [assumption]. given #9 (I,wt=8): 12 subset(A,B) | -member(f3(A,B),B). [assumption]. given #10 (I,wt=9): 13 -member(A,B) | member(A,C) | -subset(B,C). [assumption]. given #11 (I,wt=11): 14 -member(A,B) | member(A,C) | member(f4(B,C),B). [assumption]. given #12 (I,wt=11): 15 -member(A,B) | member(A,C) | -member(f4(B,C),C). [assumption]. given #13 (I,wt=9): 16 A = B | -subset(B,A) | -subset(A,B). [assumption]. given #14 (I,wt=6): 17 subset(A,B) | B != A. [assumption]. given #15 (I,wt=6): 18 subset(A,B) | A != B. [assumption]. given #16 (I,wt=13): 19 A = B | member(f5(B,A),B) | -member(f6(B,A),B). [assumption]. given #17 (I,wt=13): 20 A = B | member(f5(B,A),B) | member(f6(B,A),A). [assumption]. given #18 (I,wt=13): 21 A = B | -member(f5(B,A),A) | -member(f6(B,A),B). [assumption]. given #19 (I,wt=13): 22 A = B | -member(f5(B,A),A) | member(f6(B,A),A). [assumption]. given #20 (I,wt=9): 23 member(A,B) | -member(A,C) | C != B. [assumption]. given #21 (I,wt=16): 24 member(A,B) | -member(A,C) | member(f7(B,C),B) | -member(f8(B,C),B). [assumption]. given #22 (I,wt=16): 25 member(A,B) | -member(A,C) | member(f7(B,C),B) | member(f8(B,C),C). [assumption]. given #23 (I,wt=16): 26 member(A,B) | -member(A,C) | -member(f7(B,C),C) | -member(f8(B,C),B). [assumption]. given #24 (I,wt=16): 27 member(A,B) | -member(A,C) | -member(f7(B,C),C) | member(f8(B,C),C). [assumption]. given #25 (I,wt=9): 28 member(A,B) | -member(A,C) | B != C. [assumption]. given #26 (I,wt=16): 29 member(A,B) | -member(A,C) | member(f9(C,B),C) | -member(f10(C,B),C). [assumption]. given #27 (I,wt=16): 30 member(A,B) | -member(A,C) | member(f9(C,B),C) | member(f10(C,B),B). [assumption]. given #28 (I,wt=16): 31 member(A,B) | -member(A,C) | -member(f9(C,B),B) | -member(f10(C,B),C). [assumption]. given #29 (I,wt=16): 32 member(A,B) | -member(A,C) | -member(f9(C,B),B) | member(f10(C,B),B). [assumption]. given #30 (I,wt=3): 33 subset(A,A). [assumption]. given #31 (I,wt=7): 34 -member(A,B) | member(f12(B),B). [assumption]. given #32 (I,wt=5): 36 empty_set = difference(c1,c2). [copy(35),flip(a)]. given #33 (I,wt=3): 37 -subset(c1,c2). [assumption]. given #34 (I,wt=7): 38 -member(A,B) | member(f11(B),B). [resolve(1,b,2,a)]. given #35 (I,wt=15): 39 member(f7(A,B),A) | -member(f7(A,B),B) | -member(f8(A,B),A). [factor(24,a,c)]. given #36 (I,wt=15): 40 member(f7(A,B),A) | -member(f7(A,B),B) | member(f8(A,B),B). [factor(25,a,c)]. given #37 (I,wt=15): 41 member(f10(A,B),B) | -member(f10(A,B),A) | member(f9(A,B),A). [factor(29,b,d)]. given #38 (I,wt=15): 42 member(f10(A,B),B) | -member(f10(A,B),A) | -member(f9(A,B),B). [factor(31,b,d)]. given #39 (I,wt=5): 43 -member(A,difference(c1,c2)). [back_rewrite(10),rewrite(36(1))]. given #40 (T,wt=5): 59 member(f3(c1,c2),c1). [resolve(37,a,11,a)]. given #41 (A,wt=11): 44 -member(A,B) | member(A,C) | member(f3(B,C),B). [resolve(13,c,11,a)]. given #42 (F,wt=3): 60 c2 != c1. [ur(18,a,37,a),flip(a)]. given #43 (F,wt=5): 61 -member(f3(c1,c2),c2). [ur(12,a,37,a)]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 11. % Level of proof is 3. % Maximum clause weight is 11. % Given clauses 43. 7 member(A,difference(B,C)) | -member(A,B) | member(A,C). [assumption]. 10 -member(A,empty_set). [assumption]. 11 subset(A,B) | member(f3(A,B),A). [assumption]. 12 subset(A,B) | -member(f3(A,B),B). [assumption]. 35 difference(c1,c2) = empty_set. [assumption]. 36 empty_set = difference(c1,c2). [copy(35),flip(a)]. 37 -subset(c1,c2). [assumption]. 43 -member(A,difference(c1,c2)). [back_rewrite(10),rewrite(36(1))]. 59 member(f3(c1,c2),c1). [resolve(37,a,11,a)]. 61 -member(f3(c1,c2),c2). [ur(12,a,37,a)]. 86 $F. [ur(7,a,43,a,c,61,a),unit_del(a,59)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=43. Generated=160. Kept=82. proofs=1. Usable=43. Sos=36. Demods=1. Limbo=2, Disabled=38. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=77. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=1 (0 lex), Back_demodulated=1. Back_unit_deleted=0. Demod_attempts=764. Demod_rewrites=11. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=29. Nonunit_bsub_feature_tests=89. Megabytes=0.14. User_CPU=0.01, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 3774 exit (max_proofs) Wed Nov 22 11:23:39 2006 ============================== continuing FOF reduction multisearch == Subproblem 2 of 2 (negated): ((all B (all C ((exists D (member(D,B) & - member(D,C))) | (exists D (- member(D,B) & member(D,C))) | =(C,B)))) & (all B (all C (all D (member(D,difference(B,C)) | - member(D,B) | member(D,C))))) & (all B (all C (all D (member(D,B) | - member(D,difference(B,C)))))) & (all B (all C (all D (- member(D,C) | - member(D,difference(B,C)))))) & (all B - member(B,empty_set)) & (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 (=(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)))))) & (all B subset(B,B)) & (all B (empty(B) | (exists C member(C,B)))) & (all B ((all C - member(C,B)) | - empty(B))) & (all B ((all C - member(C,B)) | (exists C member(C,B)))) & (exists B (exists C (- =(difference(B,C),empty_set) & subset(B,C))))). Child search process 3775 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). member(f1(A,B),A) | -member(f2(A,B),A) | B = A. [assumption]. member(f1(A,B),A) | member(f2(A,B),B) | B = A. [assumption]. -member(f1(A,B),B) | -member(f2(A,B),A) | B = A. [assumption]. -member(f1(A,B),B) | member(f2(A,B),B) | B = A. [assumption]. member(A,difference(B,C)) | -member(A,B) | member(A,C). [assumption]. member(A,B) | -member(A,difference(B,C)). [assumption]. -member(A,B) | -member(A,difference(C,B)). [assumption]. -member(A,empty_set). [assumption]. subset(A,B) | member(f3(A,B),A). [assumption]. subset(A,B) | -member(f3(A,B),B). [assumption]. -member(A,B) | member(A,C) | -subset(B,C). [assumption]. -member(A,B) | member(A,C) | member(f4(B,C),B). [assumption]. -member(A,B) | member(A,C) | -member(f4(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]. A = B | member(f5(B,A),B) | -member(f6(B,A),B). [assumption]. A = B | member(f5(B,A),B) | member(f6(B,A),A). [assumption]. A = B | -member(f5(B,A),A) | -member(f6(B,A),B). [assumption]. A = B | -member(f5(B,A),A) | member(f6(B,A),A). [assumption]. member(A,B) | -member(A,C) | C != B. [assumption]. member(A,B) | -member(A,C) | member(f7(B,C),B) | -member(f8(B,C),B). [assumption]. member(A,B) | -member(A,C) | member(f7(B,C),B) | member(f8(B,C),C). [assumption]. member(A,B) | -member(A,C) | -member(f7(B,C),C) | -member(f8(B,C),B). [assumption]. member(A,B) | -member(A,C) | -member(f7(B,C),C) | member(f8(B,C),C). [assumption]. member(A,B) | -member(A,C) | B != C. [assumption]. member(A,B) | -member(A,C) | member(f9(C,B),C) | -member(f10(C,B),C). [assumption]. member(A,B) | -member(A,C) | member(f9(C,B),C) | member(f10(C,B),B). [assumption]. member(A,B) | -member(A,C) | -member(f9(C,B),B) | -member(f10(C,B),C). [assumption]. member(A,B) | -member(A,C) | -member(f9(C,B),B) | member(f10(C,B),B). [assumption]. subset(A,A). [assumption]. empty(A) | member(f11(A),A). [assumption]. -member(A,B) | -empty(B). [assumption]. -member(A,B) | member(f12(B),B). [assumption]. difference(c1,c2) != empty_set. [assumption]. subset(c1,c2). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating empty/1 1 -member(A,B) | -empty(B). [assumption]. 2 empty(A) | member(f11(A),A). [assumption]. Derived: -member(A,B) | member(f11(B),B). [resolve(1,b,2,a)]. ============================== end predicate elimination ============= Term ordering decisions: Relation symbol precedence: lex([ member, subset, =, empty ]). Function symbol precedence: lex([ empty_set, c1, c2, difference, f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11, f12 ]). 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). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 3 member(f1(A,B),A) | -member(f2(A,B),A) | B = A. [assumption]. 4 member(f1(A,B),A) | member(f2(A,B),B) | B = A. [assumption]. 5 -member(f1(A,B),B) | -member(f2(A,B),A) | B = A. [assumption]. 6 -member(f1(A,B),B) | member(f2(A,B),B) | B = A. [assumption]. 7 member(A,difference(B,C)) | -member(A,B) | member(A,C). [assumption]. 8 member(A,B) | -member(A,difference(B,C)). [assumption]. 9 -member(A,B) | -member(A,difference(C,B)). [assumption]. 10 -member(A,empty_set). [assumption]. 11 subset(A,B) | member(f3(A,B),A). [assumption]. 12 subset(A,B) | -member(f3(A,B),B). [assumption]. 13 -member(A,B) | member(A,C) | -subset(B,C). [assumption]. 14 -member(A,B) | member(A,C) | member(f4(B,C),B). [assumption]. 15 -member(A,B) | member(A,C) | -member(f4(B,C),C). [assumption]. 16 A = B | -subset(B,A) | -subset(A,B). [assumption]. 17 subset(A,B) | B != A. [assumption]. 18 subset(A,B) | A != B. [assumption]. 19 A = B | member(f5(B,A),B) | -member(f6(B,A),B). [assumption]. 20 A = B | member(f5(B,A),B) | member(f6(B,A),A). [assumption]. 21 A = B | -member(f5(B,A),A) | -member(f6(B,A),B). [assumption]. 22 A = B | -member(f5(B,A),A) | member(f6(B,A),A). [assumption]. 23 member(A,B) | -member(A,C) | C != B. [assumption]. 24 member(A,B) | -member(A,C) | member(f7(B,C),B) | -member(f8(B,C),B). [assumption]. 25 member(A,B) | -member(A,C) | member(f7(B,C),B) | member(f8(B,C),C). [assumption]. 26 member(A,B) | -member(A,C) | -member(f7(B,C),C) | -member(f8(B,C),B). [assumption]. 27 member(A,B) | -member(A,C) | -member(f7(B,C),C) | member(f8(B,C),C). [assumption]. 28 member(A,B) | -member(A,C) | B != C. [assumption]. 29 member(A,B) | -member(A,C) | member(f9(C,B),C) | -member(f10(C,B),C). [assumption]. 30 member(A,B) | -member(A,C) | member(f9(C,B),C) | member(f10(C,B),B). [assumption]. 31 member(A,B) | -member(A,C) | -member(f9(C,B),B) | -member(f10(C,B),C). [assumption]. 32 member(A,B) | -member(A,C) | -member(f9(C,B),B) | member(f10(C,B),B). [assumption]. 33 subset(A,A). [assumption]. 34 -member(A,B) | member(f12(B),B). [assumption]. 35 difference(c1,c2) != empty_set. [assumption]. 36 subset(c1,c2). [assumption]. 37 -member(A,B) | member(f11(B),B). [resolve(1,b,2,a)]. 38 member(f7(A,B),A) | -member(f7(A,B),B) | -member(f8(A,B),A). [factor(24,a,c)]. 39 member(f7(A,B),A) | -member(f7(A,B),B) | member(f8(A,B),B). [factor(25,a,c)]. 40 member(f10(A,B),B) | -member(f10(A,B),A) | member(f9(A,B),A). [factor(29,b,d)]. 41 member(f10(A,B),B) | -member(f10(A,B),A) | -member(f9(A,B),B). [factor(31,b,d)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=13): 3 member(f1(A,B),A) | -member(f2(A,B),A) | B = A. [assumption]. given #2 (I,wt=13): 4 member(f1(A,B),A) | member(f2(A,B),B) | B = A. [assumption]. given #3 (I,wt=13): 5 -member(f1(A,B),B) | -member(f2(A,B),A) | B = A. [assumption]. given #4 (I,wt=13): 6 -member(f1(A,B),B) | member(f2(A,B),B) | B = A. [assumption]. given #5 (I,wt=11): 7 member(A,difference(B,C)) | -member(A,B) | member(A,C). [assumption]. given #6 (I,wt=8): 8 member(A,B) | -member(A,difference(B,C)). [assumption]. given #7 (I,wt=8): 9 -member(A,B) | -member(A,difference(C,B)). [assumption]. given #8 (I,wt=3): 10 -member(A,empty_set). [assumption]. given #9 (I,wt=8): 11 subset(A,B) | member(f3(A,B),A). [assumption]. given #10 (I,wt=8): 12 subset(A,B) | -member(f3(A,B),B). [assumption]. given #11 (I,wt=9): 13 -member(A,B) | member(A,C) | -subset(B,C). [assumption]. given #12 (I,wt=11): 14 -member(A,B) | member(A,C) | member(f4(B,C),B). [assumption]. given #13 (I,wt=11): 15 -member(A,B) | member(A,C) | -member(f4(B,C),C). [assumption]. given #14 (I,wt=9): 16 A = B | -subset(B,A) | -subset(A,B). [assumption]. given #15 (I,wt=6): 17 subset(A,B) | B != A. [assumption]. given #16 (I,wt=6): 18 subset(A,B) | A != B. [assumption]. given #17 (I,wt=13): 19 A = B | member(f5(B,A),B) | -member(f6(B,A),B). [assumption]. given #18 (I,wt=13): 20 A = B | member(f5(B,A),B) | member(f6(B,A),A). [assumption]. given #19 (I,wt=13): 21 A = B | -member(f5(B,A),A) | -member(f6(B,A),B). [assumption]. given #20 (I,wt=13): 22 A = B | -member(f5(B,A),A) | member(f6(B,A),A). [assumption]. given #21 (I,wt=9): 23 member(A,B) | -member(A,C) | C != B. [assumption]. given #22 (I,wt=16): 24 member(A,B) | -member(A,C) | member(f7(B,C),B) | -member(f8(B,C),B). [assumption]. given #23 (I,wt=16): 25 member(A,B) | -member(A,C) | member(f7(B,C),B) | member(f8(B,C),C). [assumption]. given #24 (I,wt=16): 26 member(A,B) | -member(A,C) | -member(f7(B,C),C) | -member(f8(B,C),B). [assumption]. given #25 (I,wt=16): 27 member(A,B) | -member(A,C) | -member(f7(B,C),C) | member(f8(B,C),C). [assumption]. given #26 (I,wt=9): 28 member(A,B) | -member(A,C) | B != C. [assumption]. given #27 (I,wt=16): 29 member(A,B) | -member(A,C) | member(f9(C,B),C) | -member(f10(C,B),C). [assumption]. given #28 (I,wt=16): 30 member(A,B) | -member(A,C) | member(f9(C,B),C) | member(f10(C,B),B). [assumption]. given #29 (I,wt=16): 31 member(A,B) | -member(A,C) | -member(f9(C,B),B) | -member(f10(C,B),C). [assumption]. given #30 (I,wt=16): 32 member(A,B) | -member(A,C) | -member(f9(C,B),B) | member(f10(C,B),B). [assumption]. given #31 (I,wt=3): 33 subset(A,A). [assumption]. given #32 (I,wt=7): 34 -member(A,B) | member(f12(B),B). [assumption]. given #33 (I,wt=5): 35 difference(c1,c2) != empty_set. [assumption]. given #34 (I,wt=3): 36 subset(c1,c2). [assumption]. given #35 (I,wt=7): 37 -member(A,B) | member(f11(B),B). [resolve(1,b,2,a)]. given #36 (I,wt=15): 38 member(f7(A,B),A) | -member(f7(A,B),B) | -member(f8(A,B),A). [factor(24,a,c)]. given #37 (I,wt=15): 39 member(f7(A,B),A) | -member(f7(A,B),B) | member(f8(A,B),B). [factor(25,a,c)]. given #38 (I,wt=15): 40 member(f10(A,B),B) | -member(f10(A,B),A) | member(f9(A,B),A). [factor(29,b,d)]. given #39 (I,wt=15): 41 member(f10(A,B),B) | -member(f10(A,B),A) | -member(f9(A,B),B). [factor(31,b,d)]. given #40 (T,wt=6): 62 c2 = c1 | -subset(c2,c1). [resolve(36,a,16,c),flip(a)]. given #41 (A,wt=5): 42 -member(A,difference(empty_set,B)). [ur(8,a,10,a)]. given #42 (F,wt=7): 65 -member(A,difference(difference(empty_set,B),C)). [ur(8,a,42,a)]. given #43 (F,wt=9): 66 -member(A,difference(difference(difference(empty_set,B),C),D)). [ur(8,a,65,a)]. given #44 (T,wt=6): 63 -member(A,c1) | member(A,c2). [resolve(36,a,13,c)]. given #45 (T,wt=8): 64 c2 = c1 | member(f3(c2,c1),c2). [resolve(62,b,11,a)]. given #46 (A,wt=11): 43 -member(A,B) | member(A,C) | member(f3(B,C),B). [resolve(13,c,11,a)]. given #47 (F,wt=11): 67 -member(A,difference(difference(difference(difference(empty_set,B),C),D),E)). [ur(8,a,66,a)]. given #48 (F,wt=13): 69 -member(A,difference(difference(difference(difference(difference(empty_set,B),C),D),E),F)). [ur(8,a,67,a)]. given #49 (T,wt=9): 58 member(f6(empty_set,difference(c1,c2)),difference(c1,c2)). [resolve(35,a,20,a),unit_del(a,10)]. given #50 (T,wt=7): 85 member(f6(empty_set,difference(c1,c2)),c1). [resolve(58,a,8,b)]. ============================== PROOF ================================= % Proof 1 at 0.02 (+ 0.00) seconds. % Length of proof is 12. % Level of proof is 3. % Maximum clause weight is 13. % Given clauses 50. 8 member(A,B) | -member(A,difference(B,C)). [assumption]. 9 -member(A,B) | -member(A,difference(C,B)). [assumption]. 10 -member(A,empty_set). [assumption]. 13 -member(A,B) | member(A,C) | -subset(B,C). [assumption]. 20 A = B | member(f5(B,A),B) | member(f6(B,A),A). [assumption]. 35 difference(c1,c2) != empty_set. [assumption]. 36 subset(c1,c2). [assumption]. 58 member(f6(empty_set,difference(c1,c2)),difference(c1,c2)). [resolve(35,a,20,a),unit_del(a,10)]. 63 -member(A,c1) | member(A,c2). [resolve(36,a,13,c)]. 84 -member(f6(empty_set,difference(c1,c2)),c2). [resolve(58,a,9,b)]. 85 member(f6(empty_set,difference(c1,c2)),c1). [resolve(58,a,8,b)]. 101 $F. [resolve(85,a,63,a),unit_del(a,84)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=50. Generated=524. Kept=98. proofs=1. Usable=50. Sos=48. Demods=0. Limbo=0, Disabled=37. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=425. Back_subsumed=0. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=0. Demod_rewrites=0. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=52. Nonunit_bsub_feature_tests=97. Megabytes=0.17. User_CPU=0.02, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 3775 exit (max_proofs) Wed Nov 22 11:23:39 2006 ============================== end of multisearch ==================== All 2 subproblems have been proved, so we are done. Total user_CPU=0.03, system_CPU=0.00, wall_clock=0. THEOREM PROVED Exiting. Process 3773 exit (max_proofs) Wed Nov 22 11:23:39 2006