============================== FOF-Prover9 =========================== FOF-Prover9 (32) version August-2006A, August 2006. Process 11271 was started by mccune on cleo.thornwood, Sat Aug 12 20:59:24 2006 The command was "/home/mccune/bin/fof-prover9 -f SET593+3.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file SET593+3.in set(prolog_style_variables). formulas(assumptions). (all B all C all D (member(D,union(B,C)) <-> member(D,B) | member(D,C))). (all B all C all D (member(D,difference(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 (union(B,C) = union(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 (subset(B,union(C,D)) -> subset(difference(B,C),D) & subset(difference(B,D),C))). end_of_list. ============================== end of input ========================== % clear(auto_denials), because it is incompatiable with FOF reduction. Attempting problem reduction; original problem has = <98,47>. Problem reduction (0.00 sec) gives 2 independent subproblems: ( <160,29> <160,29> ). Max nnf_size of subproblems is 160; max cnf_max is 29. ============================== FOF REDUCTION MULTISEARCH ============= Subproblem 1 of 2 (negated): ((all B (all C (all D (member(D,union(B,C)) | - member(D,B))))) & (all B (all C (all D (member(D,union(B,C)) | - member(D,C))))) & (all B (all C (all D (member(D,B) | member(D,C) | - member(D,union(B,C)))))) & (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 (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 =(union(C,B),union(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 (subset(B,union(C,D)) & - subset(difference(B,C),D)))))). Child search process 11272 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). member(A,union(B,C)) | -member(A,B). [assumption]. member(A,union(B,C)) | -member(A,C). [assumption]. member(A,B) | member(A,C) | -member(A,union(B,C)). [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]. 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]. union(A,B) = union(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,union(c2,c3)). [assumption]. -subset(difference(c1,c2),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, union, difference, 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 union 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 member(A,union(B,C)) | -member(A,B). [assumption]. 2 member(A,union(B,C)) | -member(A,C). [assumption]. 3 member(A,B) | member(A,C) | -member(A,union(B,C)). [assumption]. 4 member(A,difference(B,C)) | -member(A,B) | member(A,C). [assumption]. 5 member(A,B) | -member(A,difference(B,C)). [assumption]. 6 -member(A,B) | -member(A,difference(C,B)). [assumption]. 7 subset(A,B) | member(f1(A,B),A). [assumption]. 8 subset(A,B) | -member(f1(A,B),B). [assumption]. 9 -member(A,B) | member(A,C) | -subset(B,C). [assumption]. 10 -member(A,B) | member(A,C) | member(f2(B,C),B). [assumption]. 11 -member(A,B) | member(A,C) | -member(f2(B,C),C). [assumption]. 12 union(A,B) = union(B,A). [assumption]. 13 subset(A,A). [assumption]. 14 A = B | member(f3(B,A),B) | -member(f4(B,A),B). [assumption]. 15 A = B | member(f3(B,A),B) | member(f4(B,A),A). [assumption]. 16 A = B | -member(f3(B,A),A) | -member(f4(B,A),B). [assumption]. 17 A = B | -member(f3(B,A),A) | member(f4(B,A),A). [assumption]. 18 member(A,B) | -member(A,C) | C != B. [assumption]. 19 member(A,B) | -member(A,C) | member(f5(B,C),B) | -member(f6(B,C),B). [assumption]. 20 member(A,B) | -member(A,C) | member(f5(B,C),B) | member(f6(B,C),C). [assumption]. 21 member(A,B) | -member(A,C) | -member(f5(B,C),C) | -member(f6(B,C),B). [assumption]. 22 member(A,B) | -member(A,C) | -member(f5(B,C),C) | member(f6(B,C),C). [assumption]. 23 member(A,B) | -member(A,C) | B != C. [assumption]. 24 member(A,B) | -member(A,C) | member(f7(C,B),C) | -member(f8(C,B),C). [assumption]. 25 member(A,B) | -member(A,C) | member(f7(C,B),C) | member(f8(C,B),B). [assumption]. 26 member(A,B) | -member(A,C) | -member(f7(C,B),B) | -member(f8(C,B),C). [assumption]. 27 member(A,B) | -member(A,C) | -member(f7(C,B),B) | member(f8(C,B),B). [assumption]. 28 subset(c1,union(c2,c3)). [assumption]. 29 -subset(difference(c1,c2),c3). [assumption]. 30 member(A,B) | -member(A,union(B,B)). [factor(3,a,b)]. 31 member(f5(A,B),A) | -member(f5(A,B),B) | -member(f6(A,B),A). [factor(19,a,c)]. 32 member(f5(A,B),A) | -member(f5(A,B),B) | member(f6(A,B),B). [factor(20,a,c)]. 33 member(f8(A,B),B) | -member(f8(A,B),A) | member(f7(A,B),A). [factor(24,b,d)]. 34 member(f8(A,B),B) | -member(f8(A,B),A) | -member(f7(A,B),B). [factor(26,b,d)]. end_of_list. formulas(demodulators). 12 union(A,B) = union(B,A). [assumption]. % (lex-dep) end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=8): 1 member(A,union(B,C)) | -member(A,B). [assumption]. given #2 (I,wt=8): 2 member(A,union(B,C)) | -member(A,C). [assumption]. given #3 (I,wt=11): 3 member(A,B) | member(A,C) | -member(A,union(B,C)). [assumption]. given #4 (I,wt=11): 4 member(A,difference(B,C)) | -member(A,B) | member(A,C). [assumption]. given #5 (I,wt=8): 5 member(A,B) | -member(A,difference(B,C)). [assumption]. given #6 (I,wt=8): 6 -member(A,B) | -member(A,difference(C,B)). [assumption]. given #7 (I,wt=8): 7 subset(A,B) | member(f1(A,B),A). [assumption]. given #8 (I,wt=8): 8 subset(A,B) | -member(f1(A,B),B). [assumption]. given #9 (I,wt=9): 9 -member(A,B) | member(A,C) | -subset(B,C). [assumption]. given #10 (I,wt=11): 10 -member(A,B) | member(A,C) | member(f2(B,C),B). [assumption]. given #11 (I,wt=11): 11 -member(A,B) | member(A,C) | -member(f2(B,C),C). [assumption]. given #12 (I,wt=7): 12 union(A,B) = union(B,A). [assumption]. given #13 (I,wt=3): 13 subset(A,A). [assumption]. given #14 (I,wt=13): 14 A = B | member(f3(B,A),B) | -member(f4(B,A),B). [assumption]. given #15 (I,wt=13): 15 A = B | member(f3(B,A),B) | member(f4(B,A),A). [assumption]. given #16 (I,wt=13): 16 A = B | -member(f3(B,A),A) | -member(f4(B,A),B). [assumption]. given #17 (I,wt=13): 17 A = B | -member(f3(B,A),A) | member(f4(B,A),A). [assumption]. given #18 (I,wt=9): 18 member(A,B) | -member(A,C) | C != B. [assumption]. given #19 (I,wt=16): 19 member(A,B) | -member(A,C) | member(f5(B,C),B) | -member(f6(B,C),B). [assumption]. given #20 (I,wt=16): 20 member(A,B) | -member(A,C) | member(f5(B,C),B) | member(f6(B,C),C). [assumption]. given #21 (I,wt=16): 21 member(A,B) | -member(A,C) | -member(f5(B,C),C) | -member(f6(B,C),B). [assumption]. given #22 (I,wt=16): 22 member(A,B) | -member(A,C) | -member(f5(B,C),C) | member(f6(B,C),C). [assumption]. given #23 (I,wt=9): 23 member(A,B) | -member(A,C) | B != C. [assumption]. given #24 (I,wt=16): 24 member(A,B) | -member(A,C) | member(f7(C,B),C) | -member(f8(C,B),C). [assumption]. given #25 (I,wt=16): 25 member(A,B) | -member(A,C) | member(f7(C,B),C) | member(f8(C,B),B). [assumption]. given #26 (I,wt=16): 26 member(A,B) | -member(A,C) | -member(f7(C,B),B) | -member(f8(C,B),C). [assumption]. given #27 (I,wt=16): 27 member(A,B) | -member(A,C) | -member(f7(C,B),B) | member(f8(C,B),B). [assumption]. given #28 (I,wt=5): 28 subset(c1,union(c2,c3)). [assumption]. given #29 (I,wt=5): 29 -subset(difference(c1,c2),c3). [assumption]. given #30 (I,wt=8): 30 member(A,B) | -member(A,union(B,B)). [factor(3,a,b)]. given #31 (I,wt=15): 31 member(f5(A,B),A) | -member(f5(A,B),B) | -member(f6(A,B),A). [factor(19,a,c)]. given #32 (I,wt=15): 32 member(f5(A,B),A) | -member(f5(A,B),B) | member(f6(A,B),B). [factor(20,a,c)]. given #33 (I,wt=15): 33 member(f8(A,B),B) | -member(f8(A,B),A) | member(f7(A,B),A). [factor(24,b,d)]. given #34 (I,wt=15): 34 member(f8(A,B),B) | -member(f8(A,B),A) | -member(f7(A,B),B). [factor(26,b,d)]. given #35 (T,wt=8): 41 -member(A,c1) | member(A,union(c2,c3)). [resolve(28,a,9,c)]. given #36 (A,wt=11): 35 -member(A,B) | member(A,C) | member(f1(B,C),B). [resolve(9,c,7,a)]. given #37 (F,wt=7): 43 -member(f1(difference(c1,c2),c3),c3). [ur(8,a,29,a)]. given #38 (F,wt=9): 44 -member(f1(difference(c1,c2),c3),union(c3,c3)). [ur(30,a,43,a)]. given #39 (T,wt=9): 42 member(f1(difference(c1,c2),c3),difference(c1,c2)). [resolve(29,a,7,a)]. given #40 (T,wt=7): 61 member(f1(difference(c1,c2),c3),c1). [resolve(42,a,5,b)]. given #41 (A,wt=16): 36 member(A,B) | -member(A,C) | member(f3(B,C),B) | member(f4(B,C),C). [resolve(18,c,15,a)]. given #42 (F,wt=3): 87 c3 != c1. [ur(23,a,43,a,b,61,a)]. given #43 (F,wt=3): 91 -subset(c1,c3). [ur(9,a,61,a,b,43,a)]. given #44 (T,wt=5): 97 member(f1(c1,c3),c1). [resolve(91,a,7,a)]. given #45 (T,wt=7): 99 member(f1(c1,c3),union(c2,c3)). [resolve(97,a,41,a)]. given #46 (A,wt=10): 37 member(A,union(B,C)) | -member(A,union(C,B)). [resolve(18,c,12,a)]. given #47 (F,wt=5): 66 difference(c1,c2) != c3. [ur(23,a,43,a,b,42,a),flip(a)]. given #48 (F,wt=5): 86 union(c3,c3) != c1. [ur(23,a,44,a,b,61,a)]. given #49 (T,wt=5): 129 member(f1(c1,c3),c2). [resolve(99,a,3,c),unit_del(b,98)]. given #50 (T,wt=7): 113 member(f1(c1,c3),union(A,c1)). [resolve(97,a,2,b)]. given #51 (A,wt=16): 38 member(A,B) | -member(A,C) | member(f3(C,B),C) | member(f4(C,B),B). [resolve(18,c,15,a(flip))]. given #52 (F,wt=5): 89 -member(f2(c1,c3),c3). [ur(11,a,61,a,b,43,a)]. given #53 (F,wt=5): 90 -subset(c1,union(c3,c3)). [ur(9,a,61,a,b,44,a)]. given #54 (T,wt=7): 114 member(f1(c1,c3),union(c1,A)). [resolve(97,a,1,b)]. given #55 (T,wt=7): 150 member(f1(c1,c3),union(A,c2)). [resolve(129,a,2,b)]. given #56 (A,wt=15): 39 member(f3(A,B),A) | -member(f3(A,B),B) | member(f4(A,B),B). [factor(36,a,c)]. given #57 (F,wt=5): 98 -member(f1(c1,c3),c3). [ur(8,a,91,a)]. given #58 (F,wt=3): 214 c3 != c2. [ur(23,a,98,a,b,129,a)]. given #59 (T,wt=7): 151 member(f1(c1,c3),union(c2,A)). [resolve(129,a,1,b)]. given #60 (T,wt=7): 176 member(f1(c1,union(c3,c3)),c1). [resolve(90,a,7,a)]. given #61 (A,wt=15): 40 member(f4(A,B),B) | -member(f4(A,B),A) | member(f3(A,B),A). [factor(38,a,d)]. given #62 (F,wt=3): 222 -subset(c2,c3). [ur(9,a,129,a,b,98,a)]. given #63 (F,wt=5): 213 union(A,c2) != c3. [ur(23,a,98,a,b,150,a),flip(a)]. given #64 (T,wt=5): 266 member(f1(c2,c3),c2). [resolve(222,a,7,a)]. given #65 (T,wt=7): 284 member(f1(c2,c3),union(A,c2)). [resolve(266,a,2,b)]. given #66 (A,wt=9): 45 -member(f1(difference(c1,c2),c3),difference(c3,A)). [ur(5,a,43,a)]. given #67 (F,wt=5): 215 union(c1,A) != c3. [ur(23,a,98,a,b,114,a),flip(a)]. given #68 (F,wt=5): 216 union(A,c1) != c3. [ur(23,a,98,a,b,113,a),flip(a)]. given #69 (T,wt=7): 285 member(f1(c2,c3),union(c2,A)). [resolve(266,a,1,b)]. given #70 (T,wt=9): 71 member(f1(difference(c1,c2),c3),union(c2,c3)). [resolve(61,a,41,a)]. ============================== PROOF ================================= % Proof 1 at 0.02 (+ 0.00) seconds. % Length of proof is 15. % Level of proof is 4. % Maximum clause weight is 11. % Given clauses 70. 3 member(A,B) | member(A,C) | -member(A,union(B,C)). [assumption]. 5 member(A,B) | -member(A,difference(B,C)). [assumption]. 6 -member(A,B) | -member(A,difference(C,B)). [assumption]. 7 subset(A,B) | member(f1(A,B),A). [assumption]. 8 subset(A,B) | -member(f1(A,B),B). [assumption]. 9 -member(A,B) | member(A,C) | -subset(B,C). [assumption]. 28 subset(c1,union(c2,c3)). [assumption]. 29 -subset(difference(c1,c2),c3). [assumption]. 41 -member(A,c1) | member(A,union(c2,c3)). [resolve(28,a,9,c)]. 42 member(f1(difference(c1,c2),c3),difference(c1,c2)). [resolve(29,a,7,a)]. 43 -member(f1(difference(c1,c2),c3),c3). [ur(8,a,29,a)]. 60 -member(f1(difference(c1,c2),c3),c2). [resolve(42,a,6,b)]. 61 member(f1(difference(c1,c2),c3),c1). [resolve(42,a,5,b)]. 71 member(f1(difference(c1,c2),c3),union(c2,c3)). [resolve(61,a,41,a)]. 350 $F. [resolve(71,a,3,c),unit_del(a,60),unit_del(b,43)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=70. Generated=472. Kept=349. proofs=1. Usable=69. Sos=248. Demods=1. Limbo=14, Disabled=47. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=122. Back_subsumed=18. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=1 (1 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=4409. Demod_rewrites=7. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=635. Nonunit_bsub_feature_tests=854. Megabytes=0.35. User_CPU=0.02, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 11272 exit (max_proofs) Sat Aug 12 20:59:24 2006 ============================== continuing FOF reduction multisearch == Subproblem 2 of 2 (negated): ((all B (all C (all D (member(D,union(B,C)) | - member(D,B))))) & (all B (all C (all D (member(D,union(B,C)) | - member(D,C))))) & (all B (all C (all D (member(D,B) | member(D,C) | - member(D,union(B,C)))))) & (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 (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 =(union(C,B),union(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 (subset(B,union(C,D)) & - subset(difference(B,D),C)))))). Child search process 11273 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). member(A,union(B,C)) | -member(A,B). [assumption]. member(A,union(B,C)) | -member(A,C). [assumption]. member(A,B) | member(A,C) | -member(A,union(B,C)). [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]. 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]. union(A,B) = union(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,union(c2,c3)). [assumption]. -subset(difference(c1,c3),c2). [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, union, difference, 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 union 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 member(A,union(B,C)) | -member(A,B). [assumption]. 2 member(A,union(B,C)) | -member(A,C). [assumption]. 3 member(A,B) | member(A,C) | -member(A,union(B,C)). [assumption]. 4 member(A,difference(B,C)) | -member(A,B) | member(A,C). [assumption]. 5 member(A,B) | -member(A,difference(B,C)). [assumption]. 6 -member(A,B) | -member(A,difference(C,B)). [assumption]. 7 subset(A,B) | member(f1(A,B),A). [assumption]. 8 subset(A,B) | -member(f1(A,B),B). [assumption]. 9 -member(A,B) | member(A,C) | -subset(B,C). [assumption]. 10 -member(A,B) | member(A,C) | member(f2(B,C),B). [assumption]. 11 -member(A,B) | member(A,C) | -member(f2(B,C),C). [assumption]. 12 union(A,B) = union(B,A). [assumption]. 13 subset(A,A). [assumption]. 14 A = B | member(f3(B,A),B) | -member(f4(B,A),B). [assumption]. 15 A = B | member(f3(B,A),B) | member(f4(B,A),A). [assumption]. 16 A = B | -member(f3(B,A),A) | -member(f4(B,A),B). [assumption]. 17 A = B | -member(f3(B,A),A) | member(f4(B,A),A). [assumption]. 18 member(A,B) | -member(A,C) | C != B. [assumption]. 19 member(A,B) | -member(A,C) | member(f5(B,C),B) | -member(f6(B,C),B). [assumption]. 20 member(A,B) | -member(A,C) | member(f5(B,C),B) | member(f6(B,C),C). [assumption]. 21 member(A,B) | -member(A,C) | -member(f5(B,C),C) | -member(f6(B,C),B). [assumption]. 22 member(A,B) | -member(A,C) | -member(f5(B,C),C) | member(f6(B,C),C). [assumption]. 23 member(A,B) | -member(A,C) | B != C. [assumption]. 24 member(A,B) | -member(A,C) | member(f7(C,B),C) | -member(f8(C,B),C). [assumption]. 25 member(A,B) | -member(A,C) | member(f7(C,B),C) | member(f8(C,B),B). [assumption]. 26 member(A,B) | -member(A,C) | -member(f7(C,B),B) | -member(f8(C,B),C). [assumption]. 27 member(A,B) | -member(A,C) | -member(f7(C,B),B) | member(f8(C,B),B). [assumption]. 28 subset(c1,union(c2,c3)). [assumption]. 29 -subset(difference(c1,c3),c2). [assumption]. 30 member(A,B) | -member(A,union(B,B)). [factor(3,a,b)]. 31 member(f5(A,B),A) | -member(f5(A,B),B) | -member(f6(A,B),A). [factor(19,a,c)]. 32 member(f5(A,B),A) | -member(f5(A,B),B) | member(f6(A,B),B). [factor(20,a,c)]. 33 member(f8(A,B),B) | -member(f8(A,B),A) | member(f7(A,B),A). [factor(24,b,d)]. 34 member(f8(A,B),B) | -member(f8(A,B),A) | -member(f7(A,B),B). [factor(26,b,d)]. end_of_list. formulas(demodulators). 12 union(A,B) = union(B,A). [assumption]. % (lex-dep) end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=8): 1 member(A,union(B,C)) | -member(A,B). [assumption]. given #2 (I,wt=8): 2 member(A,union(B,C)) | -member(A,C). [assumption]. given #3 (I,wt=11): 3 member(A,B) | member(A,C) | -member(A,union(B,C)). [assumption]. given #4 (I,wt=11): 4 member(A,difference(B,C)) | -member(A,B) | member(A,C). [assumption]. given #5 (I,wt=8): 5 member(A,B) | -member(A,difference(B,C)). [assumption]. given #6 (I,wt=8): 6 -member(A,B) | -member(A,difference(C,B)). [assumption]. given #7 (I,wt=8): 7 subset(A,B) | member(f1(A,B),A). [assumption]. given #8 (I,wt=8): 8 subset(A,B) | -member(f1(A,B),B). [assumption]. given #9 (I,wt=9): 9 -member(A,B) | member(A,C) | -subset(B,C). [assumption]. given #10 (I,wt=11): 10 -member(A,B) | member(A,C) | member(f2(B,C),B). [assumption]. given #11 (I,wt=11): 11 -member(A,B) | member(A,C) | -member(f2(B,C),C). [assumption]. given #12 (I,wt=7): 12 union(A,B) = union(B,A). [assumption]. given #13 (I,wt=3): 13 subset(A,A). [assumption]. given #14 (I,wt=13): 14 A = B | member(f3(B,A),B) | -member(f4(B,A),B). [assumption]. given #15 (I,wt=13): 15 A = B | member(f3(B,A),B) | member(f4(B,A),A). [assumption]. given #16 (I,wt=13): 16 A = B | -member(f3(B,A),A) | -member(f4(B,A),B). [assumption]. given #17 (I,wt=13): 17 A = B | -member(f3(B,A),A) | member(f4(B,A),A). [assumption]. given #18 (I,wt=9): 18 member(A,B) | -member(A,C) | C != B. [assumption]. given #19 (I,wt=16): 19 member(A,B) | -member(A,C) | member(f5(B,C),B) | -member(f6(B,C),B). [assumption]. given #20 (I,wt=16): 20 member(A,B) | -member(A,C) | member(f5(B,C),B) | member(f6(B,C),C). [assumption]. given #21 (I,wt=16): 21 member(A,B) | -member(A,C) | -member(f5(B,C),C) | -member(f6(B,C),B). [assumption]. given #22 (I,wt=16): 22 member(A,B) | -member(A,C) | -member(f5(B,C),C) | member(f6(B,C),C). [assumption]. given #23 (I,wt=9): 23 member(A,B) | -member(A,C) | B != C. [assumption]. given #24 (I,wt=16): 24 member(A,B) | -member(A,C) | member(f7(C,B),C) | -member(f8(C,B),C). [assumption]. given #25 (I,wt=16): 25 member(A,B) | -member(A,C) | member(f7(C,B),C) | member(f8(C,B),B). [assumption]. given #26 (I,wt=16): 26 member(A,B) | -member(A,C) | -member(f7(C,B),B) | -member(f8(C,B),C). [assumption]. given #27 (I,wt=16): 27 member(A,B) | -member(A,C) | -member(f7(C,B),B) | member(f8(C,B),B). [assumption]. given #28 (I,wt=5): 28 subset(c1,union(c2,c3)). [assumption]. given #29 (I,wt=5): 29 -subset(difference(c1,c3),c2). [assumption]. given #30 (I,wt=8): 30 member(A,B) | -member(A,union(B,B)). [factor(3,a,b)]. given #31 (I,wt=15): 31 member(f5(A,B),A) | -member(f5(A,B),B) | -member(f6(A,B),A). [factor(19,a,c)]. given #32 (I,wt=15): 32 member(f5(A,B),A) | -member(f5(A,B),B) | member(f6(A,B),B). [factor(20,a,c)]. given #33 (I,wt=15): 33 member(f8(A,B),B) | -member(f8(A,B),A) | member(f7(A,B),A). [factor(24,b,d)]. given #34 (I,wt=15): 34 member(f8(A,B),B) | -member(f8(A,B),A) | -member(f7(A,B),B). [factor(26,b,d)]. given #35 (T,wt=8): 41 -member(A,c1) | member(A,union(c2,c3)). [resolve(28,a,9,c)]. given #36 (A,wt=11): 35 -member(A,B) | member(A,C) | member(f1(B,C),B). [resolve(9,c,7,a)]. given #37 (F,wt=7): 43 -member(f1(difference(c1,c3),c2),c2). [ur(8,a,29,a)]. given #38 (F,wt=9): 44 -member(f1(difference(c1,c3),c2),union(c2,c2)). [ur(30,a,43,a)]. given #39 (T,wt=9): 42 member(f1(difference(c1,c3),c2),difference(c1,c3)). [resolve(29,a,7,a)]. given #40 (T,wt=7): 61 member(f1(difference(c1,c3),c2),c1). [resolve(42,a,5,b)]. given #41 (A,wt=16): 36 member(A,B) | -member(A,C) | member(f3(B,C),B) | member(f4(B,C),C). [resolve(18,c,15,a)]. given #42 (F,wt=3): 87 c2 != c1. [ur(23,a,43,a,b,61,a)]. given #43 (F,wt=3): 91 -subset(c1,c2). [ur(9,a,61,a,b,43,a)]. given #44 (T,wt=5): 97 member(f1(c1,c2),c1). [resolve(91,a,7,a)]. given #45 (T,wt=7): 99 member(f1(c1,c2),union(c2,c3)). [resolve(97,a,41,a)]. given #46 (A,wt=10): 37 member(A,union(B,C)) | -member(A,union(C,B)). [resolve(18,c,12,a)]. given #47 (F,wt=5): 66 difference(c1,c3) != c2. [ur(23,a,43,a,b,42,a),flip(a)]. given #48 (F,wt=5): 86 union(c2,c2) != c1. [ur(23,a,44,a,b,61,a)]. given #49 (T,wt=5): 129 member(f1(c1,c2),c3). [resolve(99,a,3,c),unit_del(a,98)]. given #50 (T,wt=7): 113 member(f1(c1,c2),union(A,c1)). [resolve(97,a,2,b)]. given #51 (A,wt=16): 38 member(A,B) | -member(A,C) | member(f3(C,B),C) | member(f4(C,B),B). [resolve(18,c,15,a(flip))]. given #52 (F,wt=5): 89 -member(f2(c1,c2),c2). [ur(11,a,61,a,b,43,a)]. given #53 (F,wt=5): 90 -subset(c1,union(c2,c2)). [ur(9,a,61,a,b,44,a)]. given #54 (T,wt=7): 114 member(f1(c1,c2),union(c1,A)). [resolve(97,a,1,b)]. given #55 (T,wt=7): 150 member(f1(c1,c2),union(A,c3)). [resolve(129,a,2,b)]. given #56 (A,wt=15): 39 member(f3(A,B),A) | -member(f3(A,B),B) | member(f4(A,B),B). [factor(36,a,c)]. given #57 (F,wt=5): 98 -member(f1(c1,c2),c2). [ur(8,a,91,a)]. given #58 (F,wt=3): 214 c3 != c2. [ur(23,a,98,a,b,129,a),flip(a)]. given #59 (T,wt=7): 151 member(f1(c1,c2),union(c3,A)). [resolve(129,a,1,b)]. given #60 (T,wt=7): 176 member(f1(c1,union(c2,c2)),c1). [resolve(90,a,7,a)]. given #61 (A,wt=15): 40 member(f4(A,B),B) | -member(f4(A,B),A) | member(f3(A,B),A). [factor(38,a,d)]. given #62 (F,wt=3): 222 -subset(c3,c2). [ur(9,a,129,a,b,98,a)]. given #63 (F,wt=5): 213 union(A,c3) != c2. [ur(23,a,98,a,b,150,a),flip(a)]. given #64 (T,wt=5): 266 member(f1(c3,c2),c3). [resolve(222,a,7,a)]. given #65 (T,wt=7): 284 member(f1(c3,c2),union(A,c3)). [resolve(266,a,2,b)]. given #66 (A,wt=9): 45 -member(f1(difference(c1,c3),c2),difference(c2,A)). [ur(5,a,43,a)]. given #67 (F,wt=5): 215 union(c1,A) != c2. [ur(23,a,98,a,b,114,a),flip(a)]. given #68 (F,wt=5): 216 union(A,c1) != c2. [ur(23,a,98,a,b,113,a),flip(a)]. given #69 (T,wt=7): 285 member(f1(c3,c2),union(c3,A)). [resolve(266,a,1,b)]. given #70 (T,wt=9): 71 member(f1(difference(c1,c3),c2),union(c2,c3)). [resolve(61,a,41,a)]. ============================== PROOF ================================= % Proof 1 at 0.02 (+ 0.00) seconds. % Length of proof is 15. % Level of proof is 4. % Maximum clause weight is 11. % Given clauses 70. 3 member(A,B) | member(A,C) | -member(A,union(B,C)). [assumption]. 5 member(A,B) | -member(A,difference(B,C)). [assumption]. 6 -member(A,B) | -member(A,difference(C,B)). [assumption]. 7 subset(A,B) | member(f1(A,B),A). [assumption]. 8 subset(A,B) | -member(f1(A,B),B). [assumption]. 9 -member(A,B) | member(A,C) | -subset(B,C). [assumption]. 28 subset(c1,union(c2,c3)). [assumption]. 29 -subset(difference(c1,c3),c2). [assumption]. 41 -member(A,c1) | member(A,union(c2,c3)). [resolve(28,a,9,c)]. 42 member(f1(difference(c1,c3),c2),difference(c1,c3)). [resolve(29,a,7,a)]. 43 -member(f1(difference(c1,c3),c2),c2). [ur(8,a,29,a)]. 60 -member(f1(difference(c1,c3),c2),c3). [resolve(42,a,6,b)]. 61 member(f1(difference(c1,c3),c2),c1). [resolve(42,a,5,b)]. 71 member(f1(difference(c1,c3),c2),union(c2,c3)). [resolve(61,a,41,a)]. 350 $F. [resolve(71,a,3,c),unit_del(a,43),unit_del(b,60)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=70. Generated=472. Kept=349. proofs=1. Usable=69. Sos=248. Demods=1. Limbo=14, Disabled=47. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=122. Back_subsumed=18. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=1 (1 lex), Back_demodulated=0. Back_unit_deleted=0. Demod_attempts=4409. Demod_rewrites=7. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=635. Nonunit_bsub_feature_tests=824. Megabytes=0.35. User_CPU=0.02, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 11273 exit (max_proofs) Sat Aug 12 20:59:24 2006 ============================== end of multisearch ==================== All 2 subproblems have been proved, so we are done. Total user_CPU=0.05, system_CPU=0.00, wall_clock=0. THEOREM PROVED Exiting. Process 11271 exit (max_proofs) Sat Aug 12 20:59:24 2006