============================== FOF-Prover9 =========================== FOF-Prover9 (32) version 2008-05A, May 2008. Process 21821 was started by mccune on cleo, Wed May 7 22:14:46 2008 The command was "/home/mccune/LADR/bin/fof-prover9 -f SET587+3.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file SET587+3.in assign(max_seconds,30). 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))))). Max_seconds is 30 for this subproblem. Child search process 21822 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: Predicate symbol precedence: predicate_order([ =, member, subset ]). Function symbol precedence: function_order([ 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(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) ============================== 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 (A,wt=20): 44 member(f2(A,B),difference(B,C)) | member(f2(A,B),C) | member(f1(A,B),A) | B = A. [resolve(7,b,4,b)]. given #41 (F,wt=3): 80 c2 != c1. [ur(18,a,37,a),flip(a)]. given #42 (F,wt=5): 81 -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 42. 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)])]. 79 member(f3(c1,c2),c1). [resolve(37,a,11,a)]. 81 -member(f3(c1,c2),c2). [ur(12,a,37,a)]. 117 $F. [ur(7,a,43,a,c,81,a),unit_del(a,79)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=42. Generated=171. Kept=113. proofs=1. Usable=42. Sos=68. Demods=1. Limbo=1, Disabled=39. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=57. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=1 (0 lex), Back_demodulated=1. Back_unit_deleted=0. Demod_attempts=1013. Demod_rewrites=7. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=145. Nonunit_bsub_feature_tests=133. 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 21822 exit (max_proofs) Wed May 7 22:14:46 2008 ============================== 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))))). Max_seconds is 30 for this subproblem. Child search process 21823 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: Predicate symbol precedence: predicate_order([ =, member, subset ]). Function symbol precedence: function_order([ 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(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) ============================== 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 (A,wt=20): 42 member(f2(A,B),difference(B,C)) | member(f2(A,B),C) | member(f1(A,B),A) | B = A. [resolve(7,b,4,b)]. given #41 (F,wt=5): 46 -member(A,difference(empty_set,B)). [ur(8,a,10,a)]. given #42 (F,wt=7): 114 -member(A,difference(difference(empty_set,B),C)). [ur(8,a,46,a)]. given #43 (F,wt=9): 117 -member(A,difference(difference(difference(empty_set,B),C),D)). [ur(8,a,114,a)]. given #44 (F,wt=11): 120 -member(A,difference(difference(difference(difference(empty_set,B),C),D),E)). [ur(8,a,117,a)]. given #45 (T,wt=6): 80 c2 = c1 | -subset(c2,c1). [resolve(36,a,16,c),flip(a)]. given #46 (T,wt=6): 81 -member(A,c1) | member(A,c2). [resolve(36,a,13,c)]. given #47 (T,wt=8): 45 member(f1(A,empty_set),A) | empty_set = A. [resolve(10,a,4,b)]. given #48 (T,wt=5): 131 difference(empty_set,A) = empty_set. [resolve(45,a,46,a),flip(a)]. given #49 (A,wt=19): 43 member(f2(A,difference(B,C)),B) | member(f1(A,difference(B,C)),A) | difference(B,C) = A. [resolve(8,b,4,b)]. given #50 (T,wt=7): 132 empty_set = A | member(f11(A),A). [resolve(45,a,37,a)]. given #51 (T,wt=7): 133 empty_set = A | member(f12(A),A). [resolve(45,a,34,a)]. given #52 (T,wt=7): 168 c1 = empty_set | member(f11(c1),c2). [resolve(132,b,81,a),flip(a)]. given #53 (T,wt=7): 184 c1 = empty_set | member(f12(c1),c2). [resolve(133,b,81,a),flip(a)]. given #54 (A,wt=19): 44 -member(f2(A,difference(B,C)),C) | member(f1(A,difference(B,C)),A) | difference(B,C) = A. [resolve(9,b,4,b)]. given #55 (F,wt=7): 227 -member(f2(empty_set,difference(c1,c2)),c2). [ur(44,b,10,a,c,35,a)]. given #56 (F,wt=7): 228 -member(f2(empty_set,difference(c1,c2)),c1). [ur(81,b,227,a)]. ============================== PROOF ================================= % Proof 1 at 0.02 (+ 0.00) seconds. % Length of proof is 13. % Level of proof is 4. % Maximum clause weight is 19. % Given clauses 56. 4 member(f1(A,B),A) | member(f2(A,B),B) | B = A. [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]. 13 -member(A,B) | member(A,C) | -subset(B,C). [assumption]. 35 difference(c1,c2) != empty_set. [assumption]. 36 subset(c1,c2). [assumption]. 43 member(f2(A,difference(B,C)),B) | member(f1(A,difference(B,C)),A) | difference(B,C) = A. [resolve(8,b,4,b)]. 44 -member(f2(A,difference(B,C)),C) | member(f1(A,difference(B,C)),A) | difference(B,C) = A. [resolve(9,b,4,b)]. 81 -member(A,c1) | member(A,c2). [resolve(36,a,13,c)]. 227 -member(f2(empty_set,difference(c1,c2)),c2). [ur(44,b,10,a,c,35,a)]. 228 -member(f2(empty_set,difference(c1,c2)),c1). [ur(81,b,227,a)]. 230 $F. [resolve(228,a,43,a),unit_del(a,10),unit_del(b,35)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=56. Generated=534. Kept=227. proofs=1. Usable=52. Sos=158. Demods=1. Limbo=0, Disabled=54. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=306. Back_subsumed=1. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=4 (0 lex), Back_demodulated=16. Back_unit_deleted=0. Demod_attempts=1305. Demod_rewrites=76. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=426. Nonunit_bsub_feature_tests=349. Megabytes=0.30. User_CPU=0.02, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 21823 exit (max_proofs) Wed May 7 22:14:46 2008 ============================== 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 21821 exit (max_proofs) Wed May 7 22:14:46 2008