============================== FOF-Prover9 =========================== FOF-Prover9 (32) version 22-May-2007, May 2007. Process 27387 was started by mccune on cleo, Tue May 22 14:45:14 2007 The command was "/home/mccune/bin/fof-prover9 -f SET660+3.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file SET660+3.in assign(max_seconds,120). set(prolog_style_variables). formulas(assumptions). (all B (ilf_type(B,binary_relation_type) -> (all C (ilf_type(C,set_type) -> (member(C,range_of(B)) <-> (exists D (ilf_type(D,set_type) & member(ordered_pair(D,C),B)))))))). (all B (ilf_type(B,binary_relation_type) -> ilf_type(range_of(B),set_type))). (all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> (all D (ilf_type(D,binary_relation_type) -> (member(ordered_pair(B,C),D) -> member(B,domain_of(D)) & member(C,range_of(D))))))))). (all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> ((all D (ilf_type(D,set_type) -> (member(D,B) <-> member(D,C)))) -> B = C))))). (all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> (all D (ilf_type(D,set_type) -> (all E (ilf_type(E,set_type) -> (all F (ilf_type(F,set_type) -> (F = ordered_pair(D,E) <-> F = unordered_pair(unordered_pair(D,E),singleton(D))))))))))))). (all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> ilf_type(ordered_pair(B,C),set_type))))). (all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> (all D (ilf_type(D,subset_type(cross_product(B,C))) -> ilf_type(D,relation_type(B,C)))) & (all E (ilf_type(E,relation_type(B,C)) -> ilf_type(E,subset_type(cross_product(B,C))))))))). (all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> (exists D ilf_type(D,relation_type(C,B))))))). (all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> (B = C <-> subset(B,C) & subset(C,B)))))). (all B (ilf_type(B,binary_relation_type) -> ilf_type(domain_of(B),set_type))). (all B (ilf_type(B,set_type) -> ilf_type(singleton(B),set_type))). (all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> ilf_type(cross_product(B,C),set_type))))). (all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> ilf_type(unordered_pair(B,C),set_type))))). (all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> unordered_pair(B,C) = unordered_pair(C,B))))). (all B (ilf_type(B,set_type) -> (ilf_type(B,binary_relation_type) <-> relation_like(B) & ilf_type(B,set_type)))). (exists B ilf_type(B,binary_relation_type)). (all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> (ilf_type(C,subset_type(B)) <-> ilf_type(C,member_type(power_set(B)))))))). (all B (ilf_type(B,set_type) -> (exists C ilf_type(C,subset_type(B))))). (all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> (B = C <-> (all D (ilf_type(D,set_type) -> (member(D,B) <-> member(D,C))))))))). (all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> (subset(B,C) <-> (all D (ilf_type(D,set_type) -> (member(D,B) -> member(D,C))))))))). (all B (ilf_type(B,set_type) -> subset(B,B))). (all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> (member(B,power_set(C)) <-> (all D (ilf_type(D,set_type) -> (member(D,B) -> member(D,C))))))))). (all B (ilf_type(B,set_type) -> -empty(power_set(B)) & ilf_type(power_set(B),set_type))). (all B (ilf_type(B,set_type) -> (all C (-empty(C) & ilf_type(C,set_type) -> (ilf_type(B,member_type(C)) <-> member(B,C)))))). (all B (-empty(B) & ilf_type(B,set_type) -> (exists C ilf_type(C,member_type(B))))). (all B (ilf_type(B,set_type) -> (relation_like(B) <-> (all C (ilf_type(C,set_type) -> (member(C,B) -> (exists D (ilf_type(D,set_type) & (exists E (ilf_type(E,set_type) & C = ordered_pair(D,E))))))))))). (all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> (all D (ilf_type(D,subset_type(cross_product(B,C))) -> relation_like(D))))))). (all B (ilf_type(B,set_type) -> (empty(B) <-> (all C (ilf_type(C,set_type) -> -member(C,B)))))). (all B (empty(B) & ilf_type(B,set_type) -> relation_like(B))). (all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> (all D (ilf_type(D,relation_type(B,C)) -> domain(B,C,D) = domain_of(D))))))). (all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> (all D (ilf_type(D,relation_type(B,C)) -> ilf_type(domain(B,C,D),subset_type(B)))))))). (all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> (all D (ilf_type(D,relation_type(B,C)) -> range(B,C,D) = range_of(D))))))). (all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> (all D (ilf_type(D,relation_type(B,C)) -> ilf_type(range(B,C,D),subset_type(C)))))))). (all B ilf_type(B,set_type)). -(all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> (all D (ilf_type(D,relation_type(B,C)) -> ((all E (ilf_type(E,set_type) -> (member(E,C) -> (exists F (ilf_type(F,set_type) & member(ordered_pair(F,E),D)))))) <-> range(B,C,D) = C))))))). end_of_list. ============================== end of input ========================== % clear(auto_denials), because it is incompatiable with FOF reduction. Attempting problem reduction; original problem has = <549,143>. Problem reduction (0.01 sec) gives 6 independent subproblems: ( <735,116> <734,117> <709,115> <708,116> <709,115> <708,116> ). Max nnf_size of subproblems is 735; max cnf_max is 117. ============================== FOF REDUCTION MULTISEARCH ============= Subproblem 1 of 6 (negated): ((all B (- ilf_type(B,binary_relation_type) | (all C (- ilf_type(C,set_type) | member(C,range_of(B)) | (all D (- ilf_type(D,set_type) | - member(ordered_pair(D,C),B))))))) & (all B (- ilf_type(B,binary_relation_type) | (all C (- ilf_type(C,set_type) | (exists D (ilf_type(D,set_type) & member(ordered_pair(D,C),B))) | - member(C,range_of(B)))))) & (all B (- ilf_type(B,binary_relation_type) | (all C (- ilf_type(C,set_type) | (exists D (ilf_type(D,set_type) & member(ordered_pair(D,C),B))) | (all D (- ilf_type(D,set_type) | - member(ordered_pair(D,C),B))))))) & (all B (- ilf_type(B,binary_relation_type) | ilf_type(range_of(B),set_type))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,binary_relation_type) | - member(ordered_pair(B,C),D) | member(B,domain_of(D)))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,binary_relation_type) | - member(ordered_pair(B,C),D) | member(C,range_of(D)))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (exists D (ilf_type(D,set_type) & member(D,B) & - member(D,C))) | (exists D (ilf_type(D,set_type) & - member(D,B) & member(D,C))) | =(C,B))))) & (all D (- ilf_type(D,set_type) | (all E (- ilf_type(E,set_type) | (all F (- ilf_type(F,set_type) | =(ordered_pair(D,E),F) | - =(unordered_pair(unordered_pair(D,E),singleton(D)),F))))))) & (all D (- ilf_type(D,set_type) | (all E (- ilf_type(E,set_type) | (all F (- ilf_type(F,set_type) | =(unordered_pair(unordered_pair(D,E),singleton(D)),F) | - =(ordered_pair(D,E),F))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | ilf_type(ordered_pair(B,C),set_type))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,subset_type(cross_product(B,C))) | ilf_type(D,relation_type(B,C)))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all E (- ilf_type(E,relation_type(B,C)) | ilf_type(E,subset_type(cross_product(B,C))))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (exists D ilf_type(D,relation_type(C,B))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | =(C,B) | - subset(B,C) | - subset(C,B))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | subset(B,C) | - =(C,B))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | subset(C,B) | - =(C,B))))) & (all B (- ilf_type(B,binary_relation_type) | ilf_type(domain_of(B),set_type))) & (all B (- ilf_type(B,set_type) | ilf_type(singleton(B),set_type))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | ilf_type(cross_product(B,C),set_type))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | ilf_type(unordered_pair(B,C),set_type))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | =(unordered_pair(C,B),unordered_pair(B,C)))))) & (all B (- ilf_type(B,set_type) | ilf_type(B,binary_relation_type) | - relation_like(B))) & (all B (- ilf_type(B,set_type) | relation_like(B) | - ilf_type(B,binary_relation_type))) & (exists B ilf_type(B,binary_relation_type)) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | ilf_type(C,subset_type(B)) | - ilf_type(C,member_type(power_set(B))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | ilf_type(C,member_type(power_set(B))) | - ilf_type(C,subset_type(B)))))) & (all B (- ilf_type(B,set_type) | (exists C ilf_type(C,subset_type(B))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | =(C,B) | (exists D (ilf_type(D,set_type) & member(D,B) & - member(D,C))) | (exists D (ilf_type(D,set_type) & - member(D,B) & member(D,C))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,set_type) | member(D,B) | - member(D,C))) | - =(C,B))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,set_type) | member(D,B) | - member(D,C))) | (exists D (ilf_type(D,set_type) & member(D,B) & - member(D,C))) | (exists D (ilf_type(D,set_type) & - member(D,B) & member(D,C))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,set_type) | member(D,C) | - member(D,B))) | - =(C,B))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,set_type) | member(D,C) | - member(D,B))) | (exists D (ilf_type(D,set_type) & member(D,B) & - member(D,C))) | (exists D (ilf_type(D,set_type) & - member(D,B) & member(D,C))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | subset(B,C) | (exists D (ilf_type(D,set_type) & member(D,B) & - member(D,C))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,set_type) | - member(D,B) | member(D,C))) | - subset(B,C))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,set_type) | - member(D,B) | member(D,C))) | (exists D (ilf_type(D,set_type) & member(D,B) & - member(D,C))))))) & (all B (- ilf_type(B,set_type) | subset(B,B))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | member(B,power_set(C)) | (exists D (ilf_type(D,set_type) & member(D,B) & - member(D,C))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,set_type) | - member(D,B) | member(D,C))) | - member(B,power_set(C)))))) & (all B (- ilf_type(B,set_type) | - empty(power_set(B)))) & (all B (- ilf_type(B,set_type) | ilf_type(power_set(B),set_type))) & (all B (- ilf_type(B,set_type) | (all C (empty(C) | - ilf_type(C,set_type) | ilf_type(B,member_type(C)) | - member(B,C))))) & (all B (- ilf_type(B,set_type) | (all C (empty(C) | - ilf_type(C,set_type) | member(B,C) | - ilf_type(B,member_type(C)))))) & (all B (empty(B) | - ilf_type(B,set_type) | (exists C ilf_type(C,member_type(B))))) & (all B (- ilf_type(B,set_type) | relation_like(B) | (exists C (ilf_type(C,set_type) & member(C,B) & (all D (- ilf_type(D,set_type) | (all E (- ilf_type(E,set_type) | - =(ordered_pair(D,E),C))))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | - member(C,B) | (exists D (ilf_type(D,set_type) & (exists E (ilf_type(E,set_type) & =(ordered_pair(D,E),C))))))) | - relation_like(B))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | - member(C,B) | (exists D (ilf_type(D,set_type) & (exists E (ilf_type(E,set_type) & =(ordered_pair(D,E),C))))))) | (exists C (ilf_type(C,set_type) & member(C,B) & (all D (- ilf_type(D,set_type) | (all E (- ilf_type(E,set_type) | - =(ordered_pair(D,E),C))))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,subset_type(cross_product(B,C))) | relation_like(D))))))) & (all B (- ilf_type(B,set_type) | empty(B) | (exists C (ilf_type(C,set_type) & member(C,B))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | - member(C,B))) | - empty(B))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | - member(C,B))) | (exists C (ilf_type(C,set_type) & member(C,B))))) & (all B (- empty(B) | - ilf_type(B,set_type) | relation_like(B))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,relation_type(B,C)) | =(domain(B,C,D),domain_of(D)))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,relation_type(B,C)) | ilf_type(domain(B,C,D),subset_type(B)))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,relation_type(B,C)) | =(range(B,C,D),range_of(D)))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,relation_type(B,C)) | ilf_type(range(B,C,D),subset_type(C)))))))) & (all B ilf_type(B,set_type)) & (exists B (ilf_type(B,set_type) & (exists C (ilf_type(C,set_type) & (exists D (ilf_type(D,relation_type(B,C)) & (all E (- ilf_type(E,set_type) | - member(E,C) | (exists F (ilf_type(F,set_type) & member(ordered_pair(F,E),D))))) & - =(range(B,C,D),C)))))))). Max_seconds is 120 for this subproblem. Child search process 27388 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). -ilf_type(A,binary_relation_type) | -ilf_type(B,set_type) | member(B,range_of(A)) | -ilf_type(C,set_type) | -member(ordered_pair(C,B),A). [assumption]. -ilf_type(A,binary_relation_type) | -ilf_type(B,set_type) | ilf_type(f1(A,B),set_type) | -member(B,range_of(A)). [assumption]. -ilf_type(A,binary_relation_type) | -ilf_type(B,set_type) | member(ordered_pair(f1(A,B),B),A) | -member(B,range_of(A)). [assumption]. -ilf_type(A,binary_relation_type) | -ilf_type(B,set_type) | ilf_type(f2(A,B),set_type) | -ilf_type(C,set_type) | -member(ordered_pair(C,B),A). [assumption]. -ilf_type(A,binary_relation_type) | -ilf_type(B,set_type) | member(ordered_pair(f2(A,B),B),A) | -ilf_type(C,set_type) | -member(ordered_pair(C,B),A). [assumption]. -ilf_type(A,binary_relation_type) | ilf_type(range_of(A),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,binary_relation_type) | -member(ordered_pair(A,B),C) | member(A,domain_of(C)). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,binary_relation_type) | -member(ordered_pair(A,B),C) | member(B,range_of(C)). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | ilf_type(f3(A,B),set_type) | ilf_type(f4(A,B),set_type) | B = A. [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | ilf_type(f3(A,B),set_type) | -member(f4(A,B),A) | B = A. [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | ilf_type(f3(A,B),set_type) | member(f4(A,B),B) | B = A. [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | member(f3(A,B),A) | ilf_type(f4(A,B),set_type) | B = A. [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | member(f3(A,B),A) | -member(f4(A,B),A) | B = A. [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | member(f3(A,B),A) | member(f4(A,B),B) | B = A. [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(f3(A,B),B) | ilf_type(f4(A,B),set_type) | B = A. [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(f3(A,B),B) | -member(f4(A,B),A) | B = A. [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(f3(A,B),B) | member(f4(A,B),B) | B = A. [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | ordered_pair(A,B) = C | unordered_pair(unordered_pair(A,B),singleton(A)) != C. [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | unordered_pair(unordered_pair(A,B),singleton(A)) = C | ordered_pair(A,B) != C. [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | ilf_type(ordered_pair(A,B),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,subset_type(cross_product(A,B))) | ilf_type(C,relation_type(A,B)). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,relation_type(A,B)) | ilf_type(C,subset_type(cross_product(A,B))). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | ilf_type(f5(A,B),relation_type(B,A)). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | B = A | -subset(A,B) | -subset(B,A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | subset(A,B) | B != A. [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | subset(B,A) | B != A. [assumption]. -ilf_type(A,binary_relation_type) | ilf_type(domain_of(A),set_type). [assumption]. -ilf_type(A,set_type) | ilf_type(singleton(A),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | ilf_type(cross_product(A,B),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | ilf_type(unordered_pair(A,B),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | unordered_pair(B,A) = unordered_pair(A,B). [assumption]. -ilf_type(A,set_type) | ilf_type(A,binary_relation_type) | -relation_like(A). [assumption]. -ilf_type(A,set_type) | relation_like(A) | -ilf_type(A,binary_relation_type). [assumption]. ilf_type(c1,binary_relation_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | ilf_type(B,subset_type(A)) | -ilf_type(B,member_type(power_set(A))). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | ilf_type(B,member_type(power_set(A))) | -ilf_type(B,subset_type(A)). [assumption]. -ilf_type(A,set_type) | ilf_type(f6(A),subset_type(A)). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | B = A | ilf_type(f7(A,B),set_type) | ilf_type(f8(A,B),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | B = A | ilf_type(f7(A,B),set_type) | -member(f8(A,B),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | B = A | ilf_type(f7(A,B),set_type) | member(f8(A,B),B). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | B = A | member(f7(A,B),A) | ilf_type(f8(A,B),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | B = A | member(f7(A,B),A) | -member(f8(A,B),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | B = A | member(f7(A,B),A) | member(f8(A,B),B). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | B = A | -member(f7(A,B),B) | ilf_type(f8(A,B),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | B = A | -member(f7(A,B),B) | -member(f8(A,B),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | B = A | -member(f7(A,B),B) | member(f8(A,B),B). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | member(C,A) | -member(C,B) | B != A. [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | member(C,A) | -member(C,B) | ilf_type(f9(A,B),set_type) | ilf_type(f10(A,B),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | member(C,A) | -member(C,B) | ilf_type(f9(A,B),set_type) | -member(f10(A,B),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | member(C,A) | -member(C,B) | ilf_type(f9(A,B),set_type) | member(f10(A,B),B). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | member(C,A) | -member(C,B) | member(f9(A,B),A) | ilf_type(f10(A,B),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | member(C,A) | -member(C,B) | member(f9(A,B),A) | -member(f10(A,B),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | member(C,A) | -member(C,B) | member(f9(A,B),A) | member(f10(A,B),B). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | member(C,A) | -member(C,B) | -member(f9(A,B),B) | ilf_type(f10(A,B),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | member(C,A) | -member(C,B) | -member(f9(A,B),B) | -member(f10(A,B),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | member(C,A) | -member(C,B) | -member(f9(A,B),B) | member(f10(A,B),B). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | member(C,B) | -member(C,A) | B != A. [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | member(C,B) | -member(C,A) | ilf_type(f11(A,B),set_type) | ilf_type(f12(A,B),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | member(C,B) | -member(C,A) | ilf_type(f11(A,B),set_type) | -member(f12(A,B),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | member(C,B) | -member(C,A) | ilf_type(f11(A,B),set_type) | member(f12(A,B),B). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | member(C,B) | -member(C,A) | member(f11(A,B),A) | ilf_type(f12(A,B),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | member(C,B) | -member(C,A) | member(f11(A,B),A) | -member(f12(A,B),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | member(C,B) | -member(C,A) | member(f11(A,B),A) | member(f12(A,B),B). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | member(C,B) | -member(C,A) | -member(f11(A,B),B) | ilf_type(f12(A,B),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | member(C,B) | -member(C,A) | -member(f11(A,B),B) | -member(f12(A,B),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | member(C,B) | -member(C,A) | -member(f11(A,B),B) | member(f12(A,B),B). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | subset(A,B) | ilf_type(f13(A,B),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | subset(A,B) | member(f13(A,B),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | subset(A,B) | -member(f13(A,B),B). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | -member(C,A) | member(C,B) | -subset(A,B). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | -member(C,A) | member(C,B) | ilf_type(f14(A,B),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | -member(C,A) | member(C,B) | member(f14(A,B),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | -member(C,A) | member(C,B) | -member(f14(A,B),B). [assumption]. -ilf_type(A,set_type) | subset(A,A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | member(A,power_set(B)) | ilf_type(f15(A,B),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | member(A,power_set(B)) | member(f15(A,B),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | member(A,power_set(B)) | -member(f15(A,B),B). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | -member(C,A) | member(C,B) | -member(A,power_set(B)). [assumption]. -ilf_type(A,set_type) | -empty(power_set(A)). [assumption]. -ilf_type(A,set_type) | ilf_type(power_set(A),set_type). [assumption]. -ilf_type(A,set_type) | empty(B) | -ilf_type(B,set_type) | ilf_type(A,member_type(B)) | -member(A,B). [assumption]. -ilf_type(A,set_type) | empty(B) | -ilf_type(B,set_type) | member(A,B) | -ilf_type(A,member_type(B)). [assumption]. empty(A) | -ilf_type(A,set_type) | ilf_type(f16(A),member_type(A)). [assumption]. -ilf_type(A,set_type) | relation_like(A) | ilf_type(f17(A),set_type). [assumption]. -ilf_type(A,set_type) | relation_like(A) | member(f17(A),A). [assumption]. -ilf_type(A,set_type) | relation_like(A) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | ordered_pair(B,C) != f17(A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f18(A,B),set_type) | -relation_like(A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f19(A,B),set_type) | -relation_like(A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ordered_pair(f18(A,B),f19(A,B)) = B | -relation_like(A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f20(A,B),set_type) | ilf_type(f22(A),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f20(A,B),set_type) | member(f22(A),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f20(A,B),set_type) | -ilf_type(C,set_type) | -ilf_type(D,set_type) | ordered_pair(C,D) != f22(A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f21(A,B),set_type) | ilf_type(f22(A),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f21(A,B),set_type) | member(f22(A),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f21(A,B),set_type) | -ilf_type(C,set_type) | -ilf_type(D,set_type) | ordered_pair(C,D) != f22(A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ordered_pair(f20(A,B),f21(A,B)) = B | ilf_type(f22(A),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ordered_pair(f20(A,B),f21(A,B)) = B | member(f22(A),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ordered_pair(f20(A,B),f21(A,B)) = B | -ilf_type(C,set_type) | -ilf_type(D,set_type) | ordered_pair(C,D) != f22(A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,subset_type(cross_product(A,B))) | relation_like(C). [assumption]. -ilf_type(A,set_type) | empty(A) | ilf_type(f23(A),set_type). [assumption]. -ilf_type(A,set_type) | empty(A) | member(f23(A),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | -empty(A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f24(A),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | member(f24(A),A). [assumption]. -empty(A) | -ilf_type(A,set_type) | relation_like(A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,relation_type(A,B)) | domain(A,B,C) = domain_of(C). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,relation_type(A,B)) | ilf_type(domain(A,B,C),subset_type(A)). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,relation_type(A,B)) | range(A,B,C) = range_of(C). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,relation_type(A,B)) | ilf_type(range(A,B,C),subset_type(B)). [assumption]. ilf_type(A,set_type). [assumption]. ilf_type(c2,set_type). [assumption]. ilf_type(c3,set_type). [assumption]. ilf_type(c4,relation_type(c2,c3)). [assumption]. -ilf_type(A,set_type) | -member(A,c3) | ilf_type(f25(A),set_type). [assumption]. -ilf_type(A,set_type) | -member(A,c3) | member(ordered_pair(f25(A),A),c4). [assumption]. range(c2,c3,c4) != c3. [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating relation_like/1 1 -ilf_type(A,set_type) | relation_like(A) | -ilf_type(A,binary_relation_type). [assumption]. 2 -ilf_type(A,set_type) | ilf_type(A,binary_relation_type) | -relation_like(A). [assumption]. 3 -ilf_type(A,set_type) | relation_like(A) | ilf_type(f17(A),set_type). [assumption]. 4 -ilf_type(A,set_type) | relation_like(A) | member(f17(A),A). [assumption]. Derived: -ilf_type(A,set_type) | member(f17(A),A) | -ilf_type(A,set_type) | ilf_type(A,binary_relation_type). [resolve(4,b,2,c)]. 5 -ilf_type(A,set_type) | relation_like(A) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | ordered_pair(B,C) != f17(A). [assumption]. Derived: -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | ordered_pair(B,C) != f17(A) | -ilf_type(A,set_type) | ilf_type(A,binary_relation_type). [resolve(5,b,2,c)]. 6 -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f18(A,B),set_type) | -relation_like(A). [assumption]. 7 -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f19(A,B),set_type) | -relation_like(A). [assumption]. 8 -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ordered_pair(f18(A,B),f19(A,B)) = B | -relation_like(A). [assumption]. Derived: -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ordered_pair(f18(A,B),f19(A,B)) = B | -ilf_type(A,set_type) | -ilf_type(A,binary_relation_type). [resolve(8,e,1,b)]. Derived: -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ordered_pair(f18(A,B),f19(A,B)) = B | -ilf_type(A,set_type) | member(f17(A),A). [resolve(8,e,4,b)]. Derived: -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ordered_pair(f18(A,B),f19(A,B)) = B | -ilf_type(A,set_type) | -ilf_type(C,set_type) | -ilf_type(D,set_type) | ordered_pair(C,D) != f17(A). [resolve(8,e,5,b)]. 9 -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,subset_type(cross_product(A,B))) | relation_like(C). [assumption]. Derived: -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,subset_type(cross_product(A,B))) | -ilf_type(C,set_type) | ilf_type(C,binary_relation_type). [resolve(9,d,2,c)]. Derived: -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,subset_type(cross_product(A,B))) | -ilf_type(C,set_type) | -ilf_type(D,set_type) | -member(D,C) | ordered_pair(f18(C,D),f19(C,D)) = D. [resolve(9,d,8,e)]. 10 -empty(A) | -ilf_type(A,set_type) | relation_like(A). [assumption]. Derived: -empty(A) | -ilf_type(A,set_type) | -ilf_type(A,set_type) | ilf_type(A,binary_relation_type). [resolve(10,c,2,c)]. Derived: -empty(A) | -ilf_type(A,set_type) | -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ordered_pair(f18(A,B),f19(A,B)) = B. [resolve(10,c,8,e)]. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ =, empty, ilf_type, member, subset ]). Function symbol precedence: function_order([ set_type, binary_relation_type, c1, c2, c3, c4, ordered_pair, relation_type, unordered_pair, cross_product, f1, f2, f3, f4, f5, f7, f8, f9, f10, f11, f12, f13, f14, f15, f18, f19, f20, f21, subset_type, power_set, range_of, member_type, domain_of, singleton, f6, f16, f17, f22, f23, f24, f25, domain, range ]). 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) Auto_process settings: % set(factor). % (non-Horn) % set(back_unit_deletion). % (non-Horn) % set(back_unit_deletion) -> set(unit_deletion). % Operation unordered_pair 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). 41 ilf_type(c1,binary_relation_type). [assumption]. 112 ilf_type(A,set_type). [assumption]. 113 ilf_type(c4,relation_type(c2,c3)). [assumption]. 116 -member(A,c3) | member(ordered_pair(f25(A),A),c4). [copy(115),unit_del(a,112)]. 117 range(c2,c3,c4) != c3. [assumption]. 119 member(f17(A),A) | ilf_type(A,binary_relation_type). [copy(118),merge(c),unit_del(a,112)]. 121 f17(A) != ordered_pair(B,C) | ilf_type(A,binary_relation_type). [copy(120),flip(d),merge(e),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. 123 -member(A,B) | ordered_pair(f18(B,A),f19(B,A)) = A | -ilf_type(B,binary_relation_type). [copy(122),merge(e),unit_del(a,112),unit_del(b,112)]. 125 -member(A,B) | ordered_pair(f18(B,A),f19(B,A)) = A | member(f17(B),B). [copy(124),merge(e),unit_del(a,112),unit_del(b,112)]. 127 -member(A,B) | ordered_pair(f18(B,A),f19(B,A)) = A | f17(B) != ordered_pair(C,D). [copy(126),flip(h),merge(e),unit_del(a,112),unit_del(b,112),unit_del(e,112),unit_del(f,112)]. 129 -ilf_type(A,subset_type(cross_product(B,C))) | ilf_type(A,binary_relation_type). [copy(128),unit_del(a,112),unit_del(b,112),unit_del(d,112)]. 131 -ilf_type(A,subset_type(cross_product(B,C))) | -member(D,A) | ordered_pair(f18(A,D),f19(A,D)) = D. [copy(130),unit_del(a,112),unit_del(b,112),unit_del(d,112),unit_del(e,112)]. 133 -empty(A) | ilf_type(A,binary_relation_type). [copy(132),merge(c),unit_del(b,112)]. 148 subset(A,A). [factor(34,a,b),xx(c),unit_del(a,112)]. 155 member(f9(A,B),A) | -member(f9(A,B),B) | -member(f10(A,B),A). [factor(59,d,f),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. 158 member(f9(A,B),A) | -member(f9(A,B),B) | member(f10(A,B),B). [factor(60,d,f),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. 167 member(f12(A,B),B) | -member(f12(A,B),A) | member(f11(A,B),A). [factor(69,e,g),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. 172 member(f12(A,B),B) | -member(f12(A,B),A) | -member(f11(A,B),B). [factor(72,e,g),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. 185 -member(power_set(A),power_set(A)) | member(power_set(A),A). [factor(85,d,f),merge(c),unit_del(a,112),unit_del(b,112)]. 201 -ilf_type(A,relation_type(B,C)) | ilf_type(range(B,C,A),subset_type(C)). [back_unit_del(111),unit_del(a,112),unit_del(b,112)]. 202 -ilf_type(A,relation_type(B,C)) | range(B,C,A) = range_of(A). [back_unit_del(110),unit_del(a,112),unit_del(b,112)]. 203 -ilf_type(A,relation_type(B,C)) | ilf_type(domain(B,C,A),subset_type(B)). [back_unit_del(109),unit_del(a,112),unit_del(b,112)]. 204 -ilf_type(A,relation_type(B,C)) | domain(B,C,A) = domain_of(A). [back_unit_del(108),unit_del(a,112),unit_del(b,112)]. 205 -member(A,B) | member(f24(B),B). [back_unit_del(107),unit_del(a,112),unit_del(b,112)]. 206 -member(A,B) | -empty(B). [back_unit_del(105),unit_del(a,112),unit_del(b,112)]. 207 empty(A) | member(f23(A),A). [back_unit_del(104),unit_del(a,112)]. 208 -member(A,B) | ordered_pair(f20(B,A),f21(B,A)) = A | f22(B) != ordered_pair(C,D). [back_unit_del(102),unit_del(a,112),unit_del(b,112),unit_del(e,112),unit_del(f,112)]. 209 -member(A,B) | ordered_pair(f20(B,A),f21(B,A)) = A | member(f22(B),B). [back_unit_del(100),unit_del(a,112),unit_del(b,112)]. 210 empty(A) | ilf_type(f16(A),member_type(A)). [back_unit_del(90),unit_del(b,112)]. 211 empty(A) | member(B,A) | -ilf_type(B,member_type(A)). [back_unit_del(89),unit_del(a,112),unit_del(c,112)]. 212 empty(A) | ilf_type(B,member_type(A)) | -member(B,A). [back_unit_del(88),unit_del(a,112),unit_del(c,112)]. 213 -empty(power_set(A)). [back_unit_del(86),unit_del(a,112)]. 214 -member(A,B) | member(A,C) | -member(B,power_set(C)). [back_unit_del(85),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. 215 member(A,power_set(B)) | -member(f15(A,B),B). [back_unit_del(84),unit_del(a,112),unit_del(b,112)]. 216 member(A,power_set(B)) | member(f15(A,B),A). [back_unit_del(83),unit_del(a,112),unit_del(b,112)]. 217 -member(A,B) | member(A,C) | -member(f14(B,C),C). [back_unit_del(80),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. 218 -member(A,B) | member(A,C) | member(f14(B,C),B). [back_unit_del(79),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. 219 -member(A,B) | member(A,C) | -subset(B,C). [back_unit_del(77),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. 220 subset(A,B) | -member(f13(A,B),B). [back_unit_del(76),unit_del(a,112),unit_del(b,112)]. 221 subset(A,B) | member(f13(A,B),A). [back_unit_del(75),unit_del(a,112),unit_del(b,112)]. 222 member(A,B) | -member(A,C) | -member(f11(C,B),B) | member(f12(C,B),B). [back_unit_del(73),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. 223 member(A,B) | -member(A,C) | -member(f11(C,B),B) | -member(f12(C,B),C). [back_unit_del(72),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. 224 member(A,B) | -member(A,C) | member(f11(C,B),C) | member(f12(C,B),B). [back_unit_del(70),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. 225 member(A,B) | -member(A,C) | member(f11(C,B),C) | -member(f12(C,B),C). [back_unit_del(69),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. 226 member(A,B) | -member(A,C) | B != C. [back_unit_del(64),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. 227 member(A,B) | -member(A,C) | -member(f9(B,C),C) | member(f10(B,C),C). [back_unit_del(63),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. 228 member(A,B) | -member(A,C) | -member(f9(B,C),C) | -member(f10(B,C),B). [back_unit_del(62),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. 229 member(A,B) | -member(A,C) | member(f9(B,C),B) | member(f10(B,C),C). [back_unit_del(60),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. 230 member(A,B) | -member(A,C) | member(f9(B,C),B) | -member(f10(B,C),B). [back_unit_del(59),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. 231 member(A,B) | -member(A,C) | C != B. [back_unit_del(54),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. 232 A = B | -member(f7(B,A),A) | member(f8(B,A),A). [back_unit_del(53),unit_del(a,112),unit_del(b,112)]. 233 A = B | -member(f7(B,A),A) | -member(f8(B,A),B). [back_unit_del(52),unit_del(a,112),unit_del(b,112)]. 234 A = B | member(f7(B,A),B) | member(f8(B,A),A). [back_unit_del(50),unit_del(a,112),unit_del(b,112)]. 235 A = B | member(f7(B,A),B) | -member(f8(B,A),B). [back_unit_del(49),unit_del(a,112),unit_del(b,112)]. 236 ilf_type(f6(A),subset_type(A)). [back_unit_del(44),unit_del(a,112)]. 237 ilf_type(A,member_type(power_set(B))) | -ilf_type(A,subset_type(B)). [back_unit_del(43),unit_del(a,112),unit_del(b,112)]. 238 ilf_type(A,subset_type(B)) | -ilf_type(A,member_type(power_set(B))). [back_unit_del(42),unit_del(a,112),unit_del(b,112)]. 239 unordered_pair(A,B) = unordered_pair(B,A). [back_unit_del(40),unit_del(a,112),unit_del(b,112)]. 240 subset(A,B) | A != B. [back_unit_del(35),unit_del(a,112),unit_del(b,112)]. 241 subset(A,B) | B != A. [back_unit_del(34),unit_del(a,112),unit_del(b,112)]. 242 A = B | -subset(B,A) | -subset(A,B). [back_unit_del(33),unit_del(a,112),unit_del(b,112)]. 243 ilf_type(f5(A,B),relation_type(B,A)). [back_unit_del(32),unit_del(a,112),unit_del(b,112)]. 244 -ilf_type(A,relation_type(B,C)) | ilf_type(A,subset_type(cross_product(B,C))). [back_unit_del(31),unit_del(a,112),unit_del(b,112)]. 245 -ilf_type(A,subset_type(cross_product(B,C))) | ilf_type(A,relation_type(B,C)). [back_unit_del(30),unit_del(a,112),unit_del(b,112)]. 246 unordered_pair(unordered_pair(A,B),singleton(A)) = C | ordered_pair(A,B) != C. [back_unit_del(28),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. 247 ordered_pair(A,B) = C | unordered_pair(unordered_pair(A,B),singleton(A)) != C. [back_unit_del(27),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. 248 -member(f3(A,B),B) | member(f4(A,B),B) | B = A. [back_unit_del(26),unit_del(a,112),unit_del(b,112)]. 249 -member(f3(A,B),B) | -member(f4(A,B),A) | B = A. [back_unit_del(25),unit_del(a,112),unit_del(b,112)]. 250 member(f3(A,B),A) | member(f4(A,B),B) | B = A. [back_unit_del(23),unit_del(a,112),unit_del(b,112)]. 251 member(f3(A,B),A) | -member(f4(A,B),A) | B = A. [back_unit_del(22),unit_del(a,112),unit_del(b,112)]. 252 -ilf_type(A,binary_relation_type) | -member(ordered_pair(B,C),A) | member(B,domain_of(A)). [back_unit_del(17),unit_del(a,112),unit_del(b,112)]. 253 -ilf_type(A,binary_relation_type) | member(ordered_pair(f2(A,B),B),A) | -member(ordered_pair(C,B),A). [back_unit_del(15),unit_del(b,112),unit_del(d,112)]. 254 -ilf_type(A,binary_relation_type) | member(ordered_pair(f1(A,B),B),A) | -member(B,range_of(A)). [back_unit_del(13),unit_del(b,112)]. 255 -ilf_type(A,binary_relation_type) | member(B,range_of(A)) | -member(ordered_pair(C,B),A). [back_unit_del(11),unit_del(b,112),unit_del(d,112)]. end_of_list. formulas(demodulators). 239 unordered_pair(A,B) = unordered_pair(B,A). [back_unit_del(40),unit_del(a,112),unit_del(b,112)]. % (lex-dep) end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.02 seconds. given #1 (I,wt=3): 41 ilf_type(c1,binary_relation_type). [assumption]. given #2 (I,wt=3): 112 ilf_type(A,set_type). [assumption]. given #3 (I,wt=5): 113 ilf_type(c4,relation_type(c2,c3)). [assumption]. given #4 (I,wt=9): 116 -member(A,c3) | member(ordered_pair(f25(A),A),c4). [copy(115),unit_del(a,112)]. given #5 (I,wt=6): 117 range(c2,c3,c4) != c3. [assumption]. given #6 (I,wt=7): 119 member(f17(A),A) | ilf_type(A,binary_relation_type). [copy(118),merge(c),unit_del(a,112)]. given #7 (I,wt=9): 121 f17(A) != ordered_pair(B,C) | ilf_type(A,binary_relation_type). [copy(120),flip(d),merge(e),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. given #8 (I,wt=15): 123 -member(A,B) | ordered_pair(f18(B,A),f19(B,A)) = A | -ilf_type(B,binary_relation_type). [copy(122),merge(e),unit_del(a,112),unit_del(b,112)]. given #9 (I,wt=16): 125 -member(A,B) | ordered_pair(f18(B,A),f19(B,A)) = A | member(f17(B),B). [copy(124),merge(e),unit_del(a,112),unit_del(b,112)]. given #10 (I,wt=18): 127 -member(A,B) | ordered_pair(f18(B,A),f19(B,A)) = A | f17(B) != ordered_pair(C,D). [copy(126),flip(h),merge(e),unit_del(a,112),unit_del(b,112),unit_del(e,112),unit_del(f,112)]. given #11 (I,wt=9): 129 -ilf_type(A,subset_type(cross_product(B,C))) | ilf_type(A,binary_relation_type). [copy(128),unit_del(a,112),unit_del(b,112),unit_del(d,112)]. given #12 (I,wt=18): 131 -ilf_type(A,subset_type(cross_product(B,C))) | -member(D,A) | ordered_pair(f18(A,D),f19(A,D)) = D. [copy(130),unit_del(a,112),unit_del(b,112),unit_del(d,112),unit_del(e,112)]. given #13 (I,wt=5): 133 -empty(A) | ilf_type(A,binary_relation_type). [copy(132),merge(c),unit_del(b,112)]. given #14 (I,wt=3): 148 subset(A,A). [factor(34,a,b),xx(c),unit_del(a,112)]. given #15 (I,wt=15): 155 member(f9(A,B),A) | -member(f9(A,B),B) | -member(f10(A,B),A). [factor(59,d,f),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. given #16 (I,wt=15): 158 member(f9(A,B),A) | -member(f9(A,B),B) | member(f10(A,B),B). [factor(60,d,f),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. given #17 (I,wt=15): 167 member(f12(A,B),B) | -member(f12(A,B),A) | member(f11(A,B),A). [factor(69,e,g),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. given #18 (I,wt=15): 172 member(f12(A,B),B) | -member(f12(A,B),A) | -member(f11(A,B),B). [factor(72,e,g),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. given #19 (I,wt=9): 185 -member(power_set(A),power_set(A)) | member(power_set(A),A). [factor(85,d,f),merge(c),unit_del(a,112),unit_del(b,112)]. given #20 (I,wt=12): 201 -ilf_type(A,relation_type(B,C)) | ilf_type(range(B,C,A),subset_type(C)). [back_unit_del(111),unit_del(a,112),unit_del(b,112)]. given #21 (I,wt=12): 202 -ilf_type(A,relation_type(B,C)) | range(B,C,A) = range_of(A). [back_unit_del(110),unit_del(a,112),unit_del(b,112)]. given #22 (I,wt=12): 203 -ilf_type(A,relation_type(B,C)) | ilf_type(domain(B,C,A),subset_type(B)). [back_unit_del(109),unit_del(a,112),unit_del(b,112)]. given #23 (I,wt=12): 204 -ilf_type(A,relation_type(B,C)) | domain(B,C,A) = domain_of(A). [back_unit_del(108),unit_del(a,112),unit_del(b,112)]. given #24 (I,wt=7): 205 -member(A,B) | member(f24(B),B). [back_unit_del(107),unit_del(a,112),unit_del(b,112)]. given #25 (I,wt=5): 206 -member(A,B) | -empty(B). [back_unit_del(105),unit_del(a,112),unit_del(b,112)]. given #26 (I,wt=6): 207 empty(A) | member(f23(A),A). [back_unit_del(104),unit_del(a,112)]. given #27 (I,wt=18): 208 -member(A,B) | ordered_pair(f20(B,A),f21(B,A)) = A | f22(B) != ordered_pair(C,D). [back_unit_del(102),unit_del(a,112),unit_del(b,112),unit_del(e,112),unit_del(f,112)]. given #28 (I,wt=16): 209 -member(A,B) | ordered_pair(f20(B,A),f21(B,A)) = A | member(f22(B),B). [back_unit_del(100),unit_del(a,112),unit_del(b,112)]. given #29 (I,wt=7): 210 empty(A) | ilf_type(f16(A),member_type(A)). [back_unit_del(90),unit_del(b,112)]. given #30 (I,wt=9): 211 empty(A) | member(B,A) | -ilf_type(B,member_type(A)). [back_unit_del(89),unit_del(a,112),unit_del(c,112)]. given #31 (I,wt=9): 212 empty(A) | ilf_type(B,member_type(A)) | -member(B,A). [back_unit_del(88),unit_del(a,112),unit_del(c,112)]. given #32 (I,wt=3): 213 -empty(power_set(A)). [back_unit_del(86),unit_del(a,112)]. given #33 (I,wt=10): 214 -member(A,B) | member(A,C) | -member(B,power_set(C)). [back_unit_del(85),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. given #34 (I,wt=9): 215 member(A,power_set(B)) | -member(f15(A,B),B). [back_unit_del(84),unit_del(a,112),unit_del(b,112)]. given #35 (I,wt=9): 216 member(A,power_set(B)) | member(f15(A,B),A). [back_unit_del(83),unit_del(a,112),unit_del(b,112)]. given #36 (I,wt=11): 217 -member(A,B) | member(A,C) | -member(f14(B,C),C). [back_unit_del(80),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. given #37 (I,wt=11): 218 -member(A,B) | member(A,C) | member(f14(B,C),B). [back_unit_del(79),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. given #38 (I,wt=9): 219 -member(A,B) | member(A,C) | -subset(B,C). [back_unit_del(77),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. given #39 (I,wt=8): 220 subset(A,B) | -member(f13(A,B),B). [back_unit_del(76),unit_del(a,112),unit_del(b,112)]. given #40 (I,wt=8): 221 subset(A,B) | member(f13(A,B),A). [back_unit_del(75),unit_del(a,112),unit_del(b,112)]. given #41 (I,wt=16): 222 member(A,B) | -member(A,C) | -member(f11(C,B),B) | member(f12(C,B),B). [back_unit_del(73),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. given #42 (I,wt=16): 223 member(A,B) | -member(A,C) | -member(f11(C,B),B) | -member(f12(C,B),C). [back_unit_del(72),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. given #43 (I,wt=16): 224 member(A,B) | -member(A,C) | member(f11(C,B),C) | member(f12(C,B),B). [back_unit_del(70),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. given #44 (I,wt=16): 225 member(A,B) | -member(A,C) | member(f11(C,B),C) | -member(f12(C,B),C). [back_unit_del(69),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. given #45 (I,wt=9): 226 member(A,B) | -member(A,C) | B != C. [back_unit_del(64),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. given #46 (I,wt=16): 227 member(A,B) | -member(A,C) | -member(f9(B,C),C) | member(f10(B,C),C). [back_unit_del(63),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. given #47 (I,wt=16): 228 member(A,B) | -member(A,C) | -member(f9(B,C),C) | -member(f10(B,C),B). [back_unit_del(62),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. given #48 (I,wt=16): 229 member(A,B) | -member(A,C) | member(f9(B,C),B) | member(f10(B,C),C). [back_unit_del(60),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. given #49 (I,wt=16): 230 member(A,B) | -member(A,C) | member(f9(B,C),B) | -member(f10(B,C),B). [back_unit_del(59),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. given #50 (I,wt=9): 231 member(A,B) | -member(A,C) | C != B. [back_unit_del(54),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. given #51 (I,wt=13): 232 A = B | -member(f7(B,A),A) | member(f8(B,A),A). [back_unit_del(53),unit_del(a,112),unit_del(b,112)]. given #52 (I,wt=13): 233 A = B | -member(f7(B,A),A) | -member(f8(B,A),B). [back_unit_del(52),unit_del(a,112),unit_del(b,112)]. given #53 (I,wt=13): 234 A = B | member(f7(B,A),B) | member(f8(B,A),A). [back_unit_del(50),unit_del(a,112),unit_del(b,112)]. given #54 (I,wt=13): 235 A = B | member(f7(B,A),B) | -member(f8(B,A),B). [back_unit_del(49),unit_del(a,112),unit_del(b,112)]. given #55 (I,wt=5): 236 ilf_type(f6(A),subset_type(A)). [back_unit_del(44),unit_del(a,112)]. given #56 (I,wt=9): 237 ilf_type(A,member_type(power_set(B))) | -ilf_type(A,subset_type(B)). [back_unit_del(43),unit_del(a,112),unit_del(b,112)]. given #57 (I,wt=9): 238 ilf_type(A,subset_type(B)) | -ilf_type(A,member_type(power_set(B))). [back_unit_del(42),unit_del(a,112),unit_del(b,112)]. given #58 (I,wt=7): 239 unordered_pair(A,B) = unordered_pair(B,A). [back_unit_del(40),unit_del(a,112),unit_del(b,112)]. given #59 (I,wt=6): 240 subset(A,B) | A != B. [back_unit_del(35),unit_del(a,112),unit_del(b,112)]. given #60 (I,wt=6): 241 subset(A,B) | B != A. [back_unit_del(34),unit_del(a,112),unit_del(b,112)]. given #61 (I,wt=9): 242 A = B | -subset(B,A) | -subset(A,B). [back_unit_del(33),unit_del(a,112),unit_del(b,112)]. given #62 (I,wt=7): 243 ilf_type(f5(A,B),relation_type(B,A)). [back_unit_del(32),unit_del(a,112),unit_del(b,112)]. given #63 (I,wt=11): 244 -ilf_type(A,relation_type(B,C)) | ilf_type(A,subset_type(cross_product(B,C))). [back_unit_del(31),unit_del(a,112),unit_del(b,112)]. given #64 (I,wt=11): 245 -ilf_type(A,subset_type(cross_product(B,C))) | ilf_type(A,relation_type(B,C)). [back_unit_del(30),unit_del(a,112),unit_del(b,112)]. given #65 (I,wt=13): 246 unordered_pair(unordered_pair(A,B),singleton(A)) = C | ordered_pair(A,B) != C. [back_unit_del(28),unit_del(a,112),unit_del(b,112),unit_del(c,112)]. given #66 (I,wt=13): 248 -member(f3(A,B),B) | member(f4(A,B),B) | B = A. [back_unit_del(26),unit_del(a,112),unit_del(b,112)]. given #67 (I,wt=13): 249 -member(f3(A,B),B) | -member(f4(A,B),A) | B = A. [back_unit_del(25),unit_del(a,112),unit_del(b,112)]. given #68 (I,wt=13): 250 member(f3(A,B),A) | member(f4(A,B),B) | B = A. [back_unit_del(23),unit_del(a,112),unit_del(b,112)]. given #69 (I,wt=13): 251 member(f3(A,B),A) | -member(f4(A,B),A) | B = A. [back_unit_del(22),unit_del(a,112),unit_del(b,112)]. given #70 (I,wt=12): 252 -ilf_type(A,binary_relation_type) | -member(ordered_pair(B,C),A) | member(B,domain_of(A)). [back_unit_del(17),unit_del(a,112),unit_del(b,112)]. given #71 (I,wt=15): 253 -ilf_type(A,binary_relation_type) | member(ordered_pair(f2(A,B),B),A) | -member(ordered_pair(C,B),A). [back_unit_del(15),unit_del(b,112),unit_del(d,112)]. given #72 (I,wt=14): 254 -ilf_type(A,binary_relation_type) | member(ordered_pair(f1(A,B),B),A) | -member(B,range_of(A)). [back_unit_del(13),unit_del(b,112)]. given #73 (I,wt=12): 255 -ilf_type(A,binary_relation_type) | member(B,range_of(A)) | -member(ordered_pair(C,B),A). [back_unit_del(11),unit_del(b,112),unit_del(d,112)]. given #74 (A,wt=11): 256 ilf_type(c3,binary_relation_type) | member(ordered_pair(f25(f17(c3)),f17(c3)),c4). [resolve(119,a,116,a)]. given #75 (F,wt=4): 260 range_of(c4) != c3. [back_rewrite(117),rewrite([258(4)])]. given #76 (T,wt=4): 282 member(A,power_set(A)). [resolve(216,b,215,b),merge(b)]. given #77 (T,wt=5): 259 ilf_type(range_of(c4),subset_type(c3)). [back_rewrite(257),rewrite([258(4)])]. given #78 (T,wt=5): 263 ilf_type(domain_of(c4),subset_type(c2)). [back_rewrite(261),rewrite([262(4)])]. given #79 (T,wt=5): 420 ilf_type(c3,binary_relation_type) | -empty(c4). [resolve(256,b,206,a)]. given #80 (A,wt=7): 258 range(c2,c3,c4) = range_of(c4). [resolve(202,a,113,a)]. given #81 (T,wt=5): 441 ilf_type(A,member_type(power_set(A))). [resolve(282,a,212,c),unit_del(a,213)]. given #82 (T,wt=4): 451 ilf_type(A,subset_type(A)). [resolve(441,a,238,b)]. given #83 (T,wt=5): 453 ilf_type(cross_product(A,B),binary_relation_type). [resolve(451,a,129,a)]. given #84 (T,wt=6): 265 empty(A) | member(f24(A),A). [resolve(207,b,205,a)]. given #85 (A,wt=7): 262 domain(c2,c3,c4) = domain_of(c4). [resolve(204,a,113,a)]. given #86 (T,wt=6): 275 empty(A) | member(f16(A),A). [resolve(211,c,210,b),merge(c)]. given #87 (T,wt=6): 288 member(A,power_set(B)) | -empty(A). [resolve(216,b,206,a)]. given #88 (T,wt=6): 358 ilf_type(f6(cross_product(A,B)),binary_relation_type). [resolve(236,a,129,a)]. given #89 (T,wt=6): 359 ilf_type(f6(A),member_type(power_set(A))). [resolve(237,b,236,a)]. given #90 (A,wt=7): 264 member(f24(A),A) | ilf_type(A,binary_relation_type). [resolve(205,a,119,a)]. given #91 (T,wt=5): 499 member(f6(A),power_set(A)). [resolve(359,a,211,c),unit_del(a,213)]. given #92 (T,wt=6): 360 ilf_type(f16(power_set(A)),subset_type(A)). [resolve(238,b,210,b),unit_del(b,213)]. given #93 (T,wt=6): 369 ilf_type(c4,subset_type(cross_product(c2,c3))). [resolve(244,a,113,a)]. given #94 (T,wt=3): 540 ilf_type(c4,binary_relation_type). [resolve(369,a,129,a)]. given #95 (A,wt=20): 266 empty(A) | -ilf_type(A,subset_type(cross_product(B,C))) | ordered_pair(f18(A,f23(A)),f19(A,f23(A))) = f23(A). [resolve(207,b,131,b)]. given #96 (T,wt=6): 444 member(f24(power_set(A)),power_set(A)). [resolve(282,a,205,a)]. given #97 (T,wt=6): 449 ilf_type(range_of(c4),member_type(power_set(c3))). [resolve(259,a,237,b)]. given #98 (T,wt=5): 568 member(range_of(c4),power_set(c3)). [resolve(449,a,211,c),unit_del(a,213)]. given #99 (T,wt=6): 450 ilf_type(domain_of(c4),member_type(power_set(c2))). [resolve(263,a,237,b)]. given #100 (A,wt=20): 267 empty(A) | ordered_pair(f18(A,f23(A)),f19(A,f23(A))) = f23(A) | f17(A) != ordered_pair(B,C). [resolve(207,b,127,a)]. given #101 (T,wt=5): 588 member(domain_of(c4),power_set(c2)). [resolve(450,a,211,c),unit_del(a,213)]. given #102 (T,wt=7): 276 empty(A) | ilf_type(f23(A),member_type(A)). [resolve(212,c,207,b),merge(c)]. given #103 (T,wt=6): 608 ilf_type(f23(power_set(A)),subset_type(A)). [resolve(276,b,238,b),unit_del(a,213)]. given #104 (T,wt=7): 361 subset(unordered_pair(A,B),unordered_pair(B,A)). [resolve(240,b,239,a)]. given #105 (A,wt=18): 268 empty(A) | ordered_pair(f18(A,f23(A)),f19(A,f23(A))) = f23(A) | member(f17(A),A). [resolve(207,b,125,a)]. given #106 (T,wt=7): 365 ilf_type(domain_of(f5(A,B)),subset_type(B)). [resolve(243,a,203,a),rewrite([364(2)])]. given #107 (T,wt=7): 367 ilf_type(range_of(f5(A,B)),subset_type(A)). [resolve(243,a,201,a),rewrite([366(2)])]. given #108 (T,wt=7): 421 ilf_type(c3,binary_relation_type) | member(f24(c4),c4). [resolve(256,b,205,a)]. given #109 (T,wt=7): 429 member(A,B) | power_set(A) != B. [resolve(282,a,231,b)]. given #110 (A,wt=17): 269 empty(A) | ordered_pair(f18(A,f23(A)),f19(A,f23(A))) = f23(A) | -ilf_type(A,binary_relation_type). [resolve(207,b,123,a)]. given #111 (T,wt=7): 452 ilf_type(cross_product(A,B),relation_type(A,B)). [resolve(451,a,245,a)]. given #112 (T,wt=7): 469 empty(A) | ilf_type(f24(A),member_type(A)). [resolve(265,b,212,c),merge(b)]. given #113 (T,wt=6): 664 ilf_type(f24(power_set(A)),subset_type(A)). [resolve(469,b,238,b),unit_del(a,213)]. given #114 (T,wt=7): 528 -member(A,f6(B)) | member(A,B). [resolve(499,a,214,c)]. given #115 (A,wt=10): 270 empty(c3) | member(ordered_pair(f25(f23(c3)),f23(c3)),c4). [resolve(207,b,116,a)]. given #116 (T,wt=4): 695 empty(c3) | -empty(c4). [resolve(270,b,206,a)]. given #117 (T,wt=6): 696 empty(c3) | member(f24(c4),c4). [resolve(270,b,205,a)]. given #118 (T,wt=7): 537 ilf_type(f16(power_set(A)),member_type(power_set(A))). [resolve(360,a,237,b)]. given #119 (T,wt=6): 719 member(f16(power_set(A)),power_set(A)). [resolve(537,a,211,c),unit_del(a,213)]. given #120 (A,wt=20): 271 ordered_pair(f20(A,f23(A)),f21(A,f23(A))) = f23(A) | f22(A) != ordered_pair(B,C) | empty(A). [resolve(208,a,207,b)]. given #121 (T,wt=7): 538 ilf_type(f16(power_set(cross_product(A,B))),binary_relation_type). [resolve(360,a,129,a)]. given #122 (T,wt=7): 539 ilf_type(c4,member_type(power_set(cross_product(c2,c3)))). [resolve(369,a,237,b)]. given #123 (T,wt=6): 738 member(c4,power_set(cross_product(c2,c3))). [resolve(539,a,211,c),unit_del(a,213)]. given #124 (T,wt=7): 561 ilf_type(f24(power_set(A)),member_type(power_set(A))). [resolve(444,a,212,c),unit_del(a,213)]. given #125 (A,wt=21): 272 ordered_pair(f20(A,f17(A)),f21(A,f17(A))) = f17(A) | f22(A) != ordered_pair(B,C) | ilf_type(A,binary_relation_type). [resolve(208,a,119,a)]. given #126 (T,wt=7): 580 -member(A,range_of(c4)) | member(A,c3). [resolve(568,a,214,c)]. given #127 (T,wt=7): 600 -member(A,domain_of(c4)) | member(A,c2). [resolve(588,a,214,c)]. given #128 (T,wt=7): 611 ilf_type(f23(power_set(A)),member_type(power_set(A))). [resolve(608,a,237,b)]. given #129 (T,wt=6): 776 member(f23(power_set(A)),power_set(A)). [resolve(611,a,211,c),unit_del(a,213)]. given #130 (A,wt=18): 273 ordered_pair(f20(A,f23(A)),f21(A,f23(A))) = f23(A) | member(f22(A),A) | empty(A). [resolve(209,a,207,b)]. given #131 (T,wt=7): 612 ilf_type(f23(power_set(cross_product(A,B))),binary_relation_type). [resolve(608,a,129,a)]. given #132 (T,wt=7): 661 ilf_type(domain_of(cross_product(A,B)),subset_type(A)). [resolve(452,a,203,a),rewrite([660(2)])]. given #133 (T,wt=7): 663 ilf_type(range_of(cross_product(A,B)),subset_type(B)). [resolve(452,a,201,a),rewrite([662(2)])]. given #134 (T,wt=7): 667 ilf_type(f24(power_set(cross_product(A,B))),binary_relation_type). [resolve(664,a,129,a)]. given #135 (A,wt=19): 274 ordered_pair(f20(A,f17(A)),f21(A,f17(A))) = f17(A) | member(f22(A),A) | ilf_type(A,binary_relation_type). [resolve(209,a,119,a)]. given #136 (T,wt=7): 677 empty(c3) | member(f23(c3),range_of(c4)). [resolve(270,b,255,c),unit_del(b,540)]. given #137 (T,wt=5): 863 empty(c3) | -empty(range_of(c4)). [resolve(677,b,206,a)]. given #138 (T,wt=8): 280 -member(A,f23(power_set(B))) | member(A,B). [resolve(214,c,207,b),unit_del(c,213)]. given #139 (T,wt=8): 289 member(A,power_set(B)) | member(f24(A),A). [resolve(216,b,205,a)]. given #140 (A,wt=10): 277 empty(A) | ilf_type(f17(A),member_type(A)) | ilf_type(A,binary_relation_type). [resolve(212,c,119,a)]. given #141 (T,wt=8): 368 ilf_type(f5(A,B),subset_type(cross_product(B,A))). [resolve(244,a,243,a)]. given #142 (T,wt=5): 951 ilf_type(f5(A,B),binary_relation_type). [resolve(368,a,129,a)]. given #143 (T,wt=8): 370 ilf_type(f6(cross_product(A,B)),relation_type(A,B)). [resolve(245,a,236,a)]. given #144 (T,wt=8): 440 member(A,B) | -member(power_set(A),power_set(B)). [resolve(282,a,214,a)]. given #145 (A,wt=10): 278 member(f23(A),B) | -member(A,power_set(B)) | empty(A). [resolve(214,a,207,b)]. given #146 (T,wt=8): 467 -member(A,f24(power_set(B))) | member(A,B). [resolve(265,b,214,c),unit_del(a,213)]. given #147 (T,wt=8): 490 -member(A,f16(power_set(B))) | member(A,B). [resolve(275,b,214,c),unit_del(a,213)]. given #148 (T,wt=8): 517 member(f6(A),B) | power_set(A) != B. [resolve(499,a,231,b)]. given #149 (T,wt=8): 544 ilf_type(c3,binary_relation_type) | member(f17(c3),range_of(c4)). [back_unit_del(402),unit_del(b,540)]. given #150 (A,wt=11): 279 member(f17(A),B) | -member(A,power_set(B)) | ilf_type(A,binary_relation_type). [resolve(214,a,119,a)]. given #151 (T,wt=6): 1004 ilf_type(c3,binary_relation_type) | -empty(range_of(c4)). [resolve(544,b,206,a)]. given #152 (T,wt=8): 569 member(range_of(c4),A) | power_set(c3) != A. [resolve(568,a,231,b)]. given #153 (T,wt=8): 589 member(domain_of(c4),A) | power_set(c2) != A. [resolve(588,a,231,b)]. given #154 (T,wt=8): 635 ilf_type(domain_of(f5(A,B)),member_type(power_set(B))). [resolve(365,a,237,b)]. given #155 (A,wt=12): 281 -member(A,f17(power_set(B))) | member(A,B) | ilf_type(power_set(B),binary_relation_type). [resolve(214,c,119,a)]. given #156 (T,wt=7): 1017 member(domain_of(f5(A,B)),power_set(B)). [resolve(635,a,211,c),unit_del(a,213)]. given #157 (T,wt=8): 636 ilf_type(domain_of(f5(A,cross_product(B,C))),binary_relation_type). [resolve(365,a,129,a)]. given #158 (T,wt=8): 639 ilf_type(range_of(f5(A,B)),member_type(power_set(A))). [resolve(367,a,237,b)]. given #159 (T,wt=7): 1049 member(range_of(f5(A,B)),power_set(A)). [resolve(639,a,211,c),unit_del(a,213)]. given #160 (A,wt=14): 283 member(power_set(A),power_set(B)) | -member(C,f15(power_set(A),B)) | member(C,A). [resolve(216,b,214,c)]. given #161 (T,wt=8): 640 ilf_type(range_of(f5(cross_product(A,B),C)),binary_relation_type). [resolve(367,a,129,a)]. given #162 (T,wt=8): 668 member(f16(f6(A)),A) | empty(f6(A)). [resolve(528,a,275,b)]. given #163 (T,wt=5): 1109 empty(f6(A)) | -empty(A). [resolve(668,a,206,a)]. given #164 (T,wt=7): 1110 empty(f6(A)) | member(f24(A),A). [resolve(668,a,205,a)]. given #165 (A,wt=13): 284 member(A,power_set(B)) | member(f15(A,B),C) | -member(A,power_set(C)). [resolve(216,b,214,a)]. given #166 (T,wt=8): 670 member(f24(f6(A)),A) | empty(f6(A)). [resolve(528,a,265,b)]. given #167 (T,wt=8): 675 member(f23(f6(A)),A) | empty(f6(A)). [resolve(528,a,207,b)]. given #168 (T,wt=8): 679 empty(c3) | member(f25(f23(c3)),domain_of(c4)). [resolve(270,b,252,b),unit_del(b,540)]. given #169 (T,wt=5): 1238 empty(c3) | -empty(domain_of(c4)). [resolve(679,b,206,a)]. given #170 (A,wt=12): 285 member(A,power_set(B)) | empty(A) | ilf_type(f15(A,B),member_type(A)). [resolve(216,b,212,c)]. given #171 (T,wt=7): 1222 empty(c3) | member(f25(f23(c3)),c2). [resolve(679,b,600,a)]. given #172 (T,wt=4): 1308 empty(c3) | -empty(c2). [resolve(1222,b,206,a)]. given #173 (T,wt=6): 1309 empty(c3) | member(f24(c2),c2). [resolve(1222,b,205,a)]. given #174 (T,wt=8): 750 -member(A,c4) | member(A,cross_product(c2,c3)). [resolve(738,a,214,c)]. given #175 (A,wt=23): 286 member(A,power_set(B)) | ordered_pair(f20(A,f15(A,B)),f21(A,f15(A,B))) = f15(A,B) | member(f22(A),A). [resolve(216,b,209,a)]. given #176 (T,wt=8): 758 member(f16(range_of(c4)),c3) | empty(range_of(c4)). [resolve(580,a,275,b)]. given #177 (T,wt=5): 1445 empty(range_of(c4)) | -empty(c3). [resolve(758,a,206,a)]. given #178 (T,wt=7): 1446 empty(range_of(c4)) | member(f24(c3),c3). [resolve(758,a,205,a)]. given #179 (T,wt=8): 760 member(f24(range_of(c4)),c3) | empty(range_of(c4)). [resolve(580,a,265,b)]. given #180 (A,wt=25): 287 member(A,power_set(B)) | ordered_pair(f20(A,f15(A,B)),f21(A,f15(A,B))) = f15(A,B) | f22(A) != ordered_pair(C,D). [resolve(216,b,208,a)]. given #181 (T,wt=8): 765 member(f23(range_of(c4)),c3) | empty(range_of(c4)). [resolve(580,a,207,b)]. given #182 (T,wt=8): 767 member(f16(domain_of(c4)),c2) | empty(domain_of(c4)). [resolve(600,a,275,b)]. given #183 (T,wt=5): 1526 empty(domain_of(c4)) | -empty(c2). [resolve(767,a,206,a)]. given #184 (T,wt=7): 1527 empty(domain_of(c4)) | member(f24(c2),c2). [resolve(767,a,205,a)]. given #185 (A,wt=25): 290 member(A,power_set(B)) | -ilf_type(A,subset_type(cross_product(C,D))) | ordered_pair(f18(A,f15(A,B)),f19(A,f15(A,B))) = f15(A,B). [resolve(216,b,131,b)]. given #186 (T,wt=8): 769 member(f24(domain_of(c4)),c2) | empty(domain_of(c4)). [resolve(600,a,265,b)]. given #187 (T,wt=8): 774 member(f23(domain_of(c4)),c2) | empty(domain_of(c4)). [resolve(600,a,207,b)]. given #188 (T,wt=8): 821 ilf_type(domain_of(cross_product(A,B)),member_type(power_set(A))). [resolve(661,a,237,b)]. given #189 (T,wt=7): 1599 member(domain_of(cross_product(A,B)),power_set(A)). [resolve(821,a,211,c),unit_del(a,213)]. given #190 (A,wt=25): 291 member(A,power_set(B)) | ordered_pair(f18(A,f15(A,B)),f19(A,f15(A,B))) = f15(A,B) | f17(A) != ordered_pair(C,D). [resolve(216,b,127,a)]. given #191 (T,wt=8): 822 ilf_type(domain_of(cross_product(cross_product(A,B),C)),binary_relation_type). [resolve(661,a,129,a)]. given #192 (T,wt=8): 825 ilf_type(range_of(cross_product(A,B)),member_type(power_set(B))). [resolve(663,a,237,b)]. given #193 (T,wt=7): 1622 member(range_of(cross_product(A,B)),power_set(B)). [resolve(825,a,211,c),unit_del(a,213)]. given #194 (T,wt=8): 826 ilf_type(range_of(cross_product(A,cross_product(B,C))),binary_relation_type). [resolve(663,a,129,a)]. given #195 (A,wt=23): 292 member(A,power_set(B)) | ordered_pair(f18(A,f15(A,B)),f19(A,f15(A,B))) = f15(A,B) | member(f17(A),A). [resolve(216,b,125,a)]. given #196 (T,wt=8): 864 empty(c3) | member(f24(range_of(c4)),range_of(c4)). [resolve(677,b,205,a)]. given #197 (T,wt=7): 1725 empty(c3) | member(f24(range_of(c4)),c3). [resolve(864,b,580,a)]. given #198 (T,wt=8): 953 ilf_type(domain_of(f6(cross_product(A,B))),subset_type(A)). [resolve(370,a,203,a),rewrite([952(3)])]. given #199 (T,wt=8): 955 ilf_type(range_of(f6(cross_product(A,B))),subset_type(B)). [resolve(370,a,201,a),rewrite([954(3)])]. given #200 (A,wt=22): 293 member(A,power_set(B)) | ordered_pair(f18(A,f15(A,B)),f19(A,f15(A,B))) = f15(A,B) | -ilf_type(A,binary_relation_type). [resolve(216,b,123,a)]. given #201 (T,wt=8): 956 member(f23(c4),cross_product(c2,c3)) | empty(c4). [resolve(278,b,738,a)]. given #202 (T,wt=6): 1791 empty(c4) | -empty(cross_product(c2,c3)). [resolve(956,a,206,a)]. given #203 (T,wt=8): 1239 empty(c3) | member(f24(domain_of(c4)),domain_of(c4)). [resolve(679,b,205,a)]. given #204 (T,wt=7): 1797 empty(c3) | member(f24(domain_of(c4)),c2). [resolve(1239,b,600,a)]. given #205 (A,wt=14): 294 member(c3,power_set(A)) | member(ordered_pair(f25(f15(c3,A)),f15(c3,A)),c4). [resolve(216,b,116,a)]. given #206 (T,wt=6): 1854 member(c3,power_set(A)) | -empty(c4). [resolve(294,b,206,a)]. given #207 (T,wt=8): 1333 member(f24(c4),cross_product(c2,c3)) | empty(c3). [resolve(750,a,696,b)]. given #208 (T,wt=6): 1875 empty(c3) | -empty(cross_product(c2,c3)). [resolve(1333,a,206,a)]. given #209 (T,wt=8): 1339 member(f16(c4),cross_product(c2,c3)) | empty(c4). [resolve(750,a,275,b)]. given #210 (A,wt=15): 295 member(power_set(power_set(A)),power_set(A)) | -member(power_set(power_set(A)),f15(power_set(power_set(A)),A)). [factor(283,a,c)]. given #211 (T,wt=8): 1342 member(f24(c4),cross_product(c2,c3)) | empty(c4). [resolve(750,a,265,b)]. given #212 (T,wt=8): 1757 empty(c3) | ilf_type(f24(range_of(c4)),member_type(c3)). [resolve(1725,b,212,c),merge(b)]. given #213 (T,wt=8): 1855 member(c3,power_set(A)) | member(f24(c4),c4). [resolve(294,b,205,a)]. given #214 (T,wt=8): 1958 member(f24(c4),c4) | -member(f24(c4),c3). [factor(1930,a,c)]. given #215 (A,wt=14): 296 member(f15(A,B),C) | -member(f14(A,C),C) | member(A,power_set(B)). [resolve(217,a,216,b)]. given #216 (T,wt=9): 316 member(f23(A),B) | B != A | empty(A). [resolve(226,b,207,b)]. given #217 (T,wt=9): 331 member(f23(A),B) | A != B | empty(A). [resolve(231,b,207,b)]. given #218 (T,wt=9): 439 member(A,B) | -member(f14(power_set(A),B),B). [resolve(282,a,217,a)]. given #219 (T,wt=9): 455 empty(A) | member(f24(A),B) | A != B. [resolve(265,b,231,b)]. given #220 (A,wt=11): 297 member(f23(A),B) | -member(f14(A,B),B) | empty(A). [resolve(217,a,207,b)]. given #221 (T,wt=9): 460 empty(A) | member(f24(A),B) | B != A. [resolve(265,b,226,b)]. given #222 (T,wt=9): 478 empty(A) | member(f16(A),B) | A != B. [resolve(275,b,231,b)]. given #223 (T,wt=9): 483 empty(A) | member(f16(A),B) | B != A. [resolve(275,b,226,b)]. given #224 (T,wt=9): 529 member(f6(A),B) | -member(power_set(A),power_set(B)). [resolve(499,a,214,a)]. given #225 (A,wt=12): 298 member(f17(A),B) | -member(f14(A,B),B) | ilf_type(A,binary_relation_type). [resolve(217,a,119,a)]. given #226 (T,wt=9): 536 ilf_type(f16(power_set(cross_product(A,B))),relation_type(A,B)). [resolve(360,a,245,a)]. given #227 (T,wt=9): 542 ilf_type(c3,binary_relation_type) | member(f25(f17(c3)),domain_of(c4)). [back_unit_del(404),unit_del(b,540)]. given #228 (T,wt=6): 2001 ilf_type(c3,binary_relation_type) | -empty(domain_of(c4)). [resolve(542,b,206,a)]. given #229 (T,wt=8): 1985 ilf_type(c3,binary_relation_type) | member(f25(f17(c3)),c2). [resolve(542,b,600,a)]. given #230 (A,wt=14): 299 member(f15(A,B),C) | member(f14(A,C),A) | member(A,power_set(B)). [resolve(218,a,216,b)]. given #231 (T,wt=5): 2022 ilf_type(c3,binary_relation_type) | -empty(c2). [resolve(1985,b,206,a)]. given #232 (T,wt=7): 2023 ilf_type(c3,binary_relation_type) | member(f24(c2),c2). [resolve(1985,b,205,a)]. given #233 (T,wt=9): 549 member(f24(power_set(A)),B) | power_set(A) != B. [resolve(444,a,231,b)]. given #234 (T,wt=9): 581 member(range_of(c4),A) | -member(power_set(c3),power_set(A)). [resolve(568,a,214,a)]. given #235 (A,wt=11): 300 member(f23(A),B) | member(f14(A,B),A) | empty(A). [resolve(218,a,207,b)]. given #236 (T,wt=9): 601 member(domain_of(c4),A) | -member(power_set(c2),power_set(A)). [resolve(588,a,214,a)]. given #237 (T,wt=9): 610 ilf_type(f23(power_set(cross_product(A,B))),relation_type(A,B)). [resolve(608,a,245,a)]. given #238 (T,wt=9): 666 ilf_type(f24(power_set(cross_product(A,B))),relation_type(A,B)). [resolve(664,a,245,a)]. given #239 (T,wt=9): 671 member(f24(f6(A)),A) | ilf_type(f6(A),binary_relation_type). [resolve(528,a,264,a)]. given #240 (A,wt=12): 301 member(f17(A),B) | member(f14(A,B),A) | ilf_type(A,binary_relation_type). [resolve(218,a,119,a)]. given #241 (T,wt=6): 2253 ilf_type(f6(A),binary_relation_type) | -empty(A). [resolve(671,a,206,a)]. given #242 (T,wt=8): 2254 ilf_type(f6(A),binary_relation_type) | member(f24(A),A). [resolve(671,a,205,a)]. given #243 (T,wt=9): 676 member(f17(f6(A)),A) | ilf_type(f6(A),binary_relation_type). [resolve(528,a,119,a)]. given #244 (T,wt=9): 701 empty(c3) | member(f24(c4),A) | c4 != A. [resolve(696,b,231,b)]. given #245 (A,wt=11): 302 member(f13(A,B),A) | -member(C,A) | member(C,B). [resolve(221,a,219,c)]. given #246 (T,wt=9): 720 member(f16(power_set(A)),B) | power_set(A) != B. [resolve(719,a,231,b)]. given #247 (T,wt=9): 739 member(c4,A) | power_set(cross_product(c2,c3)) != A. [resolve(738,a,231,b)]. given #248 (T,wt=9): 761 member(f24(range_of(c4)),c3) | ilf_type(range_of(c4),binary_relation_type). [resolve(580,a,264,a)]. given #249 (T,wt=6): 2485 ilf_type(range_of(c4),binary_relation_type) | -empty(c3). [resolve(761,a,206,a)]. given #250 (A,wt=19): 303 member(f15(A,B),C) | -member(f11(A,C),C) | member(f12(A,C),C) | member(A,power_set(B)). [resolve(222,b,216,b)]. given #251 (T,wt=8): 2486 ilf_type(range_of(c4),binary_relation_type) | member(f24(c3),c3). [resolve(761,a,205,a)]. given #252 (T,wt=9): 766 member(f17(range_of(c4)),c3) | ilf_type(range_of(c4),binary_relation_type). [resolve(580,a,119,a)]. given #253 (T,wt=9): 770 member(f24(domain_of(c4)),c2) | ilf_type(domain_of(c4),binary_relation_type). [resolve(600,a,264,a)]. given #254 (T,wt=6): 2553 ilf_type(domain_of(c4),binary_relation_type) | -empty(c2). [resolve(770,a,206,a)]. given #255 (A,wt=16): 304 member(f23(A),B) | -member(f11(A,B),B) | member(f12(A,B),B) | empty(A). [resolve(222,b,207,b)]. given #256 (T,wt=8): 2554 ilf_type(domain_of(c4),binary_relation_type) | member(f24(c2),c2). [resolve(770,a,205,a)]. given #257 (T,wt=9): 775 member(f17(domain_of(c4)),c2) | ilf_type(domain_of(c4),binary_relation_type). [resolve(600,a,119,a)]. given #258 (T,wt=9): 777 member(f23(power_set(A)),B) | power_set(A) != B. [resolve(776,a,231,b)]. given #259 (T,wt=9): 910 member(f24(A),A) | ilf_type(A,member_type(power_set(B))). [resolve(289,a,212,c),unit_del(b,213)]. given #260 (A,wt=17): 305 member(f17(A),B) | -member(f11(A,B),B) | member(f12(A,B),B) | ilf_type(A,binary_relation_type). [resolve(222,b,119,a)]. given #261 (T,wt=7): 2628 ilf_type(A,member_type(power_set(B))) | -empty(A). [resolve(910,a,206,a)]. given #262 (T,wt=9): 950 ilf_type(f5(A,B),member_type(power_set(cross_product(B,A)))). [resolve(368,a,237,b)]. given #263 (T,wt=8): 2638 member(f5(A,B),power_set(cross_product(B,A))). [resolve(950,a,211,c),unit_del(a,213)]. given #264 (T,wt=9): 1005 ilf_type(c3,binary_relation_type) | member(f24(range_of(c4)),range_of(c4)). [resolve(544,b,205,a)]. given #265 (A,wt=19): 306 member(f15(A,B),C) | -member(f11(A,C),C) | -member(f12(A,C),A) | member(A,power_set(B)). [resolve(223,b,216,b)]. given #266 (T,wt=8): 2661 ilf_type(c3,binary_relation_type) | member(f24(range_of(c4)),c3). [resolve(1005,b,580,a)]. given #267 (T,wt=9): 1041 -member(A,domain_of(f5(B,C))) | member(A,C). [resolve(1017,a,214,c)]. given #268 (T,wt=9): 1063 -member(A,range_of(f5(B,C))) | member(A,B). [resolve(1049,a,214,c)]. given #269 (T,wt=9): 1116 empty(f6(domain_of(c4))) | member(f24(domain_of(c4)),c2). [resolve(1110,b,600,a)]. given #270 (A,wt=16): 307 member(f23(A),B) | -member(f11(A,B),B) | -member(f12(A,B),A) | empty(A). [resolve(223,b,207,b)]. given #271 (T,wt=6): 2768 empty(f6(domain_of(c4))) | -empty(c2). [resolve(1116,b,206,a)]. given #272 (T,wt=8): 2769 empty(f6(domain_of(c4))) | member(f24(c2),c2). [resolve(1116,b,205,a)]. given #273 (T,wt=9): 1117 empty(f6(range_of(c4))) | member(f24(range_of(c4)),c3). [resolve(1110,b,580,a)]. given #274 (T,wt=6): 2812 empty(f6(range_of(c4))) | -empty(c3). [resolve(1117,b,206,a)]. given #275 (A,wt=17): 308 member(f17(A),B) | -member(f11(A,B),B) | -member(f12(A,B),A) | ilf_type(A,binary_relation_type). [resolve(223,b,119,a)]. given #276 (T,wt=8): 2813 empty(f6(range_of(c4))) | member(f24(c3),c3). [resolve(1117,b,205,a)]. given #277 (T,wt=9): 1118 empty(f6(f6(A))) | member(f24(f6(A)),A). [resolve(1110,b,528,a)]. given #278 (T,wt=6): 2876 empty(f6(f6(A))) | -empty(A). [resolve(1118,b,206,a)]. given #279 (T,wt=8): 2877 empty(f6(f6(A))) | member(f24(A),A). [resolve(1118,b,205,a)]. given #280 (A,wt=19): 309 member(f15(A,B),C) | member(f11(A,C),A) | member(f12(A,C),C) | member(A,power_set(B)). [resolve(224,b,216,b)]. given #281 (T,wt=9): 1314 empty(c3) | member(f24(c2),A) | c2 != A. [resolve(1309,b,231,b)]. given #282 (T,wt=9): 1332 member(f24(c4),cross_product(c2,c3)) | empty(f6(c4)). [resolve(750,a,1110,b)]. given #283 (T,wt=7): 3043 empty(f6(c4)) | -empty(cross_product(c2,c3)). [resolve(1332,a,206,a)]. given #284 (T,wt=9): 1337 member(f24(c4),cross_product(c2,c3)) | ilf_type(c3,binary_relation_type). [resolve(750,a,421,b)]. given #285 (A,wt=16): 310 member(f23(A),B) | member(f11(A,B),A) | member(f12(A,B),B) | empty(A). [resolve(224,b,207,b)]. given #286 (T,wt=7): 3065 ilf_type(c3,binary_relation_type) | -empty(cross_product(c2,c3)). [resolve(1337,a,206,a)]. given #287 (T,wt=9): 1614 -member(A,domain_of(cross_product(B,C))) | member(A,B). [resolve(1599,a,214,c)]. given #288 (T,wt=9): 1637 -member(A,range_of(cross_product(B,C))) | member(A,C). [resolve(1622,a,214,c)]. given #289 (T,wt=9): 1768 ilf_type(domain_of(f6(cross_product(A,B))),member_type(power_set(A))). [resolve(953,a,237,b)]. given #290 (A,wt=17): 311 member(f17(A),B) | member(f11(A,B),A) | member(f12(A,B),B) | ilf_type(A,binary_relation_type). [resolve(224,b,119,a)]. given #291 (T,wt=8): 3215 member(domain_of(f6(cross_product(A,B))),power_set(A)). [resolve(1768,a,211,c),unit_del(a,213)]. given #292 (T,wt=9): 1769 ilf_type(domain_of(f6(cross_product(cross_product(A,B),C))),binary_relation_type). [resolve(953,a,129,a)]. given #293 (T,wt=9): 1773 ilf_type(range_of(f6(cross_product(A,B))),member_type(power_set(B))). [resolve(955,a,237,b)]. given #294 (T,wt=8): 3327 member(range_of(f6(cross_product(A,B))),power_set(B)). [resolve(1773,a,211,c),unit_del(a,213)]. given #295 (A,wt=19): 312 member(f15(A,B),C) | member(f11(A,C),A) | -member(f12(A,C),A) | member(A,power_set(B)). [resolve(225,b,216,b)]. given #296 (T,wt=9): 1774 ilf_type(range_of(f6(cross_product(A,cross_product(B,C)))),binary_relation_type). [resolve(955,a,129,a)]. given #297 (T,wt=9): 1932 member(f24(c4),c4) | ilf_type(c3,member_type(power_set(A))). [resolve(1855,a,212,c),unit_del(b,213)]. given #298 (T,wt=7): 3371 ilf_type(c3,member_type(power_set(A))) | -empty(c4). [resolve(1932,a,206,a)]. given #299 (T,wt=9): 1982 ilf_type(domain_of(f16(power_set(cross_product(A,B)))),subset_type(A)). [resolve(536,a,203,a),rewrite([1981(4)])]. given #300 (A,wt=16): 313 member(f23(A),B) | member(f11(A,B),A) | -member(f12(A,B),A) | empty(A). [resolve(225,b,207,b)]. given #301 (T,wt=9): 1984 ilf_type(range_of(f16(power_set(cross_product(A,B)))),subset_type(B)). [resolve(536,a,201,a),rewrite([1983(4)])]. given #302 (T,wt=9): 2002 ilf_type(c3,binary_relation_type) | member(f24(domain_of(c4)),domain_of(c4)). [resolve(542,b,205,a)]. given #303 (T,wt=8): 3390 ilf_type(c3,binary_relation_type) | member(f24(domain_of(c4)),c2). [resolve(2002,b,600,a)]. given #304 (T,wt=9): 2053 member(f14(A,B),A) | member(A,power_set(B)). [resolve(299,a,215,b),merge(c)]. given #305 (A,wt=17): 314 member(f17(A),B) | member(f11(A,B),A) | -member(f12(A,B),A) | ilf_type(A,binary_relation_type). [resolve(225,b,119,a)]. given #306 (T,wt=9): 2168 member(f14(A,B),A) | empty(A) | -empty(B). [resolve(300,a,206,a)]. given #307 (T,wt=9): 2216 ilf_type(domain_of(f23(power_set(cross_product(A,B)))),subset_type(A)). [resolve(610,a,203,a),rewrite([2215(4)])]. given #308 (T,wt=9): 2218 ilf_type(range_of(f23(power_set(cross_product(A,B)))),subset_type(B)). [resolve(610,a,201,a),rewrite([2217(4)])]. given #309 (T,wt=9): 2220 ilf_type(domain_of(f24(power_set(cross_product(A,B)))),subset_type(A)). [resolve(666,a,203,a),rewrite([2219(4)])]. given #310 (A,wt=12): 315 member(f15(A,B),C) | C != A | member(A,power_set(B)). [resolve(226,b,216,b)]. given #311 (T,wt=9): 2222 ilf_type(range_of(f24(power_set(cross_product(A,B)))),subset_type(B)). [resolve(666,a,201,a),rewrite([2221(4)])]. given #312 (T,wt=10): 317 member(f17(A),B) | B != A | ilf_type(A,binary_relation_type). [resolve(226,b,119,a)]. given #313 (T,wt=10): 332 member(f17(A),B) | A != B | ilf_type(A,binary_relation_type). [resolve(231,b,119,a)]. given #314 (T,wt=10): 350 A = B | member(f7(B,A),B) | -empty(A). [resolve(234,c,206,a)]. given #315 (A,wt=19): 318 member(f15(A,B),C) | -member(f9(C,A),A) | member(f10(C,A),A) | member(A,power_set(B)). [resolve(227,b,216,b)]. given #316 (T,wt=10): 371 unordered_pair(unordered_pair(A,B),singleton(A)) = ordered_pair(A,B). [xx_res(246,b)]. given #317 (T,wt=10): 389 member(f3(A,B),A) | B = A | -empty(B). [resolve(250,b,206,a)]. given #318 (T,wt=10): 438 member(A,B) | member(f14(power_set(A),B),power_set(A)). [resolve(282,a,218,a)]. given #319 (T,wt=9): 3528 member(A,A) | -member(A,f14(power_set(A),A)). [factor(3519,a,c)]. given #320 (A,wt=16): 319 member(f23(A),B) | -member(f9(B,A),A) | member(f10(B,A),A) | empty(A). [resolve(227,b,207,b)]. given #321 (T,wt=10): 468 empty(A) | member(f24(A),B) | -member(A,power_set(B)). [resolve(265,b,214,a)]. given #322 (T,wt=10): 476 empty(c3) | member(ordered_pair(f25(f24(c3)),f24(c3)),c4). [resolve(265,b,116,a)]. given #323 (T,wt=7): 3574 empty(c3) | member(f24(c3),range_of(c4)). [resolve(476,b,255,c),unit_del(b,540)]. given #324 (T,wt=8): 3576 empty(c3) | member(f25(f24(c3)),domain_of(c4)). [resolve(476,b,252,b),unit_del(b,540)]. given #325 (A,wt=17): 320 member(f17(A),B) | -member(f9(B,A),A) | member(f10(B,A),A) | ilf_type(A,binary_relation_type). [resolve(227,b,119,a)]. given #326 (T,wt=7): 3617 empty(c3) | member(f25(f24(c3)),c2). [resolve(3576,b,600,a)]. given #327 (T,wt=10): 491 empty(A) | member(f16(A),B) | -member(A,power_set(B)). [resolve(275,b,214,a)]. given #328 (T,wt=10): 498 empty(c3) | member(ordered_pair(f25(f16(c3)),f16(c3)),c4). [resolve(275,b,116,a)]. given #329 (T,wt=7): 3697 empty(c3) | member(f16(c3),range_of(c4)). [resolve(498,b,255,c),unit_del(b,540)]. given #330 (A,wt=19): 321 member(f15(A,B),C) | -member(f9(C,A),A) | -member(f10(C,A),C) | member(A,power_set(B)). [resolve(228,b,216,b)]. given #331 (T,wt=8): 3699 empty(c3) | member(f25(f16(c3)),domain_of(c4)). [resolve(498,b,252,b),unit_del(b,540)]. given #332 (T,wt=7): 3744 empty(c3) | member(f25(f16(c3)),c2). [resolve(3699,b,600,a)]. given #333 (T,wt=10): 501 ilf_type(A,binary_relation_type) | member(f24(A),B) | A != B. [resolve(264,a,231,b)]. given #334 (T,wt=10): 506 ilf_type(A,binary_relation_type) | member(f24(A),B) | B != A. [resolve(264,a,226,b)]. given #335 (A,wt=16): 322 member(f23(A),B) | -member(f9(B,A),A) | -member(f10(B,A),B) | empty(A). [resolve(228,b,207,b)]. given #336 (T,wt=10): 527 member(f6(A),B) | -member(f14(power_set(A),B),B). [resolve(499,a,217,a)]. given #337 (T,wt=10): 560 member(f24(power_set(A)),B) | -member(power_set(A),power_set(B)). [resolve(444,a,214,a)]. given #338 (T,wt=10): 579 member(range_of(c4),A) | -member(f14(power_set(c3),A),A). [resolve(568,a,217,a)]. given #339 (T,wt=10): 599 member(domain_of(c4),A) | -member(f14(power_set(c2),A),A). [resolve(588,a,217,a)]. given #340 (A,wt=17): 323 member(f17(A),B) | -member(f9(B,A),A) | -member(f10(B,A),B) | ilf_type(A,binary_relation_type). [resolve(228,b,119,a)]. given #341 (T,wt=10): 613 -member(A,unordered_pair(B,C)) | member(A,unordered_pair(C,B)). [resolve(361,a,219,c)]. given #342 (T,wt=10): 634 ilf_type(domain_of(f5(A,cross_product(B,C))),relation_type(B,C)). [resolve(365,a,245,a)]. given #343 (T,wt=10): 638 ilf_type(range_of(f5(cross_product(A,B),C)),relation_type(A,B)). [resolve(367,a,245,a)]. given #344 (T,wt=10): 641 ilf_type(c3,binary_relation_type) | member(f24(c4),A) | c4 != A. [resolve(421,b,231,b)]. given #345 (A,wt=19): 324 member(f15(A,B),C) | member(f9(C,A),C) | member(f10(C,A),A) | member(A,power_set(B)). [resolve(229,b,216,b)]. given #346 (T,wt=10): 712 empty(c3) | member(f24(c4),A) | -member(c4,power_set(A)). [resolve(696,b,214,a)]. given #347 (T,wt=10): 731 member(f16(power_set(A)),B) | -member(power_set(A),power_set(B)). [resolve(719,a,214,a)]. given #348 (T,wt=10): 751 member(c4,A) | -member(power_set(cross_product(c2,c3)),power_set(A)). [resolve(738,a,214,a)]. given #349 (T,wt=10): 788 member(f23(power_set(A)),B) | -member(power_set(A),power_set(B)). [resolve(776,a,214,a)]. given #350 (A,wt=16): 325 member(f23(A),B) | member(f9(B,A),B) | member(f10(B,A),A) | empty(A). [resolve(229,b,207,b)]. given #351 (T,wt=10): 820 ilf_type(domain_of(cross_product(cross_product(A,B),C)),relation_type(A,B)). [resolve(661,a,245,a)]. given #352 (T,wt=10): 824 ilf_type(range_of(cross_product(A,cross_product(B,C))),relation_type(B,C)). [resolve(663,a,245,a)]. given #353 (T,wt=10): 848 empty(c3) | member(f23(c3),A) | range_of(c4) != A. [resolve(677,b,231,b)]. given #354 (T,wt=10): 869 member(f16(f23(power_set(A))),A) | empty(f23(power_set(A))). [resolve(280,a,275,b)]. given #355 (A,wt=17): 326 member(f17(A),B) | member(f9(B,A),B) | member(f10(B,A),A) | ilf_type(A,binary_relation_type). [resolve(229,b,119,a)]. given #356 (T,wt=6): 4105 empty(f23(power_set(A))) | -empty(A). [resolve(869,a,206,a)]. given #357 (T,wt=8): 4106 empty(f23(power_set(A))) | member(f24(A),A). [resolve(869,a,205,a)]. given #358 (T,wt=10): 873 member(f24(f23(power_set(A))),A) | empty(f23(power_set(A))). [resolve(280,a,265,b)]. given #359 (T,wt=10): 878 member(f23(f23(power_set(A))),A) | empty(f23(power_set(A))). [resolve(280,a,207,b)]. given #360 (A,wt=19): 327 member(f15(A,B),C) | member(f9(C,A),C) | -member(f10(C,A),C) | member(A,power_set(B)). [resolve(230,b,216,b)]. given #361 (T,wt=10): 921 member(domain_of(c4),power_set(A)) | member(f24(domain_of(c4)),c2). [resolve(289,b,600,a)]. given #362 (T,wt=7): 4362 member(domain_of(c4),power_set(A)) | -empty(c2). [resolve(921,b,206,a)]. given #363 (T,wt=9): 4363 member(domain_of(c4),power_set(A)) | member(f24(c2),c2). [resolve(921,b,205,a)]. given #364 (T,wt=10): 922 member(range_of(c4),power_set(A)) | member(f24(range_of(c4)),c3). [resolve(289,b,580,a)]. given #365 (A,wt=16): 328 member(f23(A),B) | member(f9(B,A),B) | -member(f10(B,A),B) | empty(A). [resolve(230,b,207,b)]. given #366 (T,wt=7): 4443 member(range_of(c4),power_set(A)) | -empty(c3). [resolve(922,b,206,a)]. given #367 (T,wt=9): 4444 member(range_of(c4),power_set(A)) | member(f24(c3),c3). [resolve(922,b,205,a)]. given #368 (T,wt=10): 923 member(f6(A),power_set(B)) | member(f24(f6(A)),A). [resolve(289,b,528,a)]. given #369 (T,wt=7): 4553 member(f6(A),power_set(B)) | -empty(A). [resolve(923,b,206,a)]. given #370 (A,wt=17): 329 member(f17(A),B) | member(f9(B,A),B) | -member(f10(B,A),B) | ilf_type(A,binary_relation_type). [resolve(230,b,119,a)]. given #371 (T,wt=9): 4554 member(f6(A),power_set(B)) | member(f24(A),A). [resolve(923,b,205,a)]. given #372 (T,wt=10): 948 ilf_type(power_set(A),binary_relation_type) | ilf_type(f17(power_set(A)),subset_type(A)). [resolve(277,b,238,b),unit_del(a,213)]. given #373 (T,wt=10): 957 member(f23(f16(power_set(A))),A) | empty(f16(power_set(A))). [resolve(278,b,719,a)]. given #374 (T,wt=6): 4665 empty(f16(power_set(A))) | -empty(A). [resolve(957,a,206,a)]. given #375 (A,wt=12): 330 member(f15(A,B),C) | A != C | member(A,power_set(B)). [resolve(231,b,216,b)]. given #376 (T,wt=8): 4666 empty(f16(power_set(A))) | member(f24(A),A). [resolve(957,a,205,a)]. given #377 (T,wt=10): 958 member(f23(f24(power_set(A))),A) | empty(f24(power_set(A))). [resolve(278,b,444,a)]. given #378 (T,wt=6): 4746 empty(f24(power_set(A))) | -empty(A). [resolve(958,a,206,a)]. given #379 (T,wt=8): 4747 empty(f24(power_set(A))) | member(f24(A),A). [resolve(958,a,205,a)]. given #380 (A,wt=16): 333 A = B | member(f7(B,A),B) | member(f8(B,A),C) | A != C. [resolve(234,c,231,b)]. given #381 (T,wt=10): 967 member(f16(f24(power_set(A))),A) | empty(f24(power_set(A))). [resolve(467,a,275,b)]. given #382 (T,wt=10): 971 member(f24(f24(power_set(A))),A) | empty(f24(power_set(A))). [resolve(467,a,265,b)]. given #383 (T,wt=10): 978 member(f16(f16(power_set(A))),A) | empty(f16(power_set(A))). [resolve(490,a,275,b)]. given #384 (T,wt=10): 982 member(f24(f16(power_set(A))),A) | empty(f16(power_set(A))). [resolve(490,a,265,b)]. given #385 (A,wt=23): 334 A = B | member(f7(B,A),B) | member(f8(B,A),C) | member(f9(C,A),C) | -member(f10(C,A),C). [resolve(234,c,230,b)]. given #386 (T,wt=10): 1030 member(domain_of(f5(A,B)),C) | power_set(B) != C. [resolve(1017,a,231,b)]. given #387 (T,wt=10): 1052 member(range_of(f5(A,B)),C) | power_set(A) != C. [resolve(1049,a,231,b)]. given #388 (T,wt=10): 1081 empty(f6(domain_of(c4))) | member(f16(f6(domain_of(c4))),c2). [resolve(668,a,600,a)]. given #389 (T,wt=10): 1082 empty(f6(range_of(c4))) | member(f16(f6(range_of(c4))),c3). [resolve(668,a,580,a)]. given #390 (A,wt=23): 335 A = B | member(f7(B,A),B) | member(f8(B,A),C) | member(f9(C,A),C) | member(f10(C,A),A). [resolve(234,c,229,b)]. given #391 (T,wt=10): 1083 empty(f6(f6(A))) | member(f16(f6(f6(A))),A). [resolve(668,a,528,a)]. given #392 (T,wt=10): 1125 empty(f6(A)) | member(f24(A),B) | A != B. [resolve(1110,b,231,b)]. given #393 (T,wt=10): 1130 empty(f6(A)) | member(f24(A),B) | B != A. [resolve(1110,b,226,b)]. given #394 (T,wt=10): 1154 empty(f6(domain_of(c4))) | member(f24(f6(domain_of(c4))),c2). [resolve(670,a,600,a)]. given #395 (A,wt=23): 336 A = B | member(f7(B,A),B) | member(f8(B,A),C) | -member(f9(C,A),A) | -member(f10(C,A),C). [resolve(234,c,228,b)]. given #396 (T,wt=10): 1155 empty(f6(range_of(c4))) | member(f24(f6(range_of(c4))),c3). [resolve(670,a,580,a)]. given #397 (T,wt=10): 1156 empty(f6(f6(A))) | member(f24(f6(f6(A))),A). [resolve(670,a,528,a)]. given #398 (T,wt=10): 1188 empty(f6(domain_of(c4))) | member(f23(f6(domain_of(c4))),c2). [resolve(675,a,600,a)]. given #399 (T,wt=10): 1189 empty(f6(range_of(c4))) | member(f23(f6(range_of(c4))),c3). [resolve(675,a,580,a)]. given #400 (A,wt=23): 337 A = B | member(f7(B,A),B) | member(f8(B,A),C) | -member(f9(C,A),A) | member(f10(C,A),A). [resolve(234,c,227,b)]. given #401 (T,wt=10): 1190 empty(f6(f6(A))) | member(f23(f6(f6(A))),A). [resolve(675,a,528,a)]. given #402 (T,wt=10): 1293 empty(c3) | member(f25(f23(c3)),A) | c2 != A. [resolve(1222,b,231,b)]. given #403 (T,wt=10): 1305 empty(c3) | empty(c2) | ilf_type(f25(f23(c3)),member_type(c2)). [resolve(1222,b,212,c)]. given #404 (T,wt=10): 1325 empty(c3) | member(f24(c2),A) | -member(c2,power_set(A)). [resolve(1309,b,214,a)]. given #405 (A,wt=16): 338 A = B | member(f7(B,A),B) | member(f8(B,A),C) | C != A. [resolve(234,c,226,b)]. given #406 (T,wt=10): 1334 member(f23(f6(c4)),cross_product(c2,c3)) | empty(f6(c4)). [resolve(750,a,675,a)]. given #407 (T,wt=10): 1335 member(f24(f6(c4)),cross_product(c2,c3)) | empty(f6(c4)). [resolve(750,a,670,a)]. given #408 (T,wt=10): 1336 member(f16(f6(c4)),cross_product(c2,c3)) | empty(f6(c4)). [resolve(750,a,668,a)]. given #409 (T,wt=10): 1338 member(f24(c4),cross_product(c2,c3)) | member(c4,power_set(A)). [resolve(750,a,289,b)]. given #410 (A,wt=23): 339 A = B | member(f7(B,A),B) | member(f8(B,A),C) | member(f11(A,C),A) | -member(f12(A,C),A). [resolve(234,c,225,b)]. given #411 (T,wt=8): 5398 member(c4,power_set(A)) | -empty(cross_product(c2,c3)). [resolve(1338,a,206,a)]. given #412 (T,wt=10): 1452 empty(range_of(c4)) | member(f24(c3),A) | c3 != A. [resolve(1446,b,231,b)]. given #413 (T,wt=10): 1532 empty(domain_of(c4)) | member(f24(c2),A) | c2 != A. [resolve(1527,b,231,b)]. given #414 (T,wt=10): 1603 member(domain_of(cross_product(A,B)),C) | power_set(A) != C. [resolve(1599,a,231,b)]. given #415 (A,wt=23): 340 A = B | member(f7(B,A),B) | member(f8(B,A),C) | member(f11(A,C),A) | member(f12(A,C),C). [resolve(234,c,224,b)]. given #416 (T,wt=10): 1626 member(range_of(cross_product(A,B)),C) | power_set(B) != C. [resolve(1622,a,231,b)]. given #417 (T,wt=10): 1745 empty(c3) | member(f24(range_of(c4)),A) | c3 != A. [resolve(1725,b,231,b)]. given #418 (T,wt=10): 1792 empty(c4) | member(f24(cross_product(c2,c3)),cross_product(c2,c3)). [resolve(956,a,205,a)]. given #419 (T,wt=10): 1816 empty(c3) | member(f24(domain_of(c4)),A) | c2 != A. [resolve(1797,b,231,b)]. given #420 (A,wt=23): 341 A = B | member(f7(B,A),B) | member(f8(B,A),C) | -member(f11(A,C),C) | -member(f12(A,C),A). [resolve(234,c,223,b)]. given #421 (T,wt=10): 1828 empty(c3) | empty(c2) | ilf_type(f24(domain_of(c4)),member_type(c2)). [resolve(1797,b,212,c)]. given #422 (T,wt=10): 1836 member(c3,power_set(A)) | member(f15(c3,A),range_of(c4)). [resolve(294,b,255,c),unit_del(b,540)]. given #423 (T,wt=5): 5560 member(c3,power_set(range_of(c4))). [resolve(1836,b,215,b),merge(b)]. given #424 (T,wt=6): 5585 ilf_type(c3,member_type(power_set(range_of(c4)))). [resolve(5560,a,212,c),unit_del(a,213)]. given #425 (A,wt=23): 342 A = B | member(f7(B,A),B) | member(f8(B,A),C) | -member(f11(A,C),C) | member(f12(A,C),C). [resolve(234,c,222,b)]. given #426 (T,wt=5): 5592 ilf_type(c3,subset_type(range_of(c4))). [resolve(5585,a,238,b)]. given #427 (T,wt=7): 5565 member(c3,power_set(A)) | -empty(range_of(c4)). [resolve(1836,b,206,a)]. given #428 (T,wt=7): 5583 -member(A,c3) | member(A,range_of(c4)). [resolve(5560,a,214,c)]. given #429 (T,wt=8): 5572 member(c3,A) | power_set(range_of(c4)) != A. [resolve(5560,a,231,b)]. given #430 (A,wt=18): 343 A = B | member(f7(B,A),B) | member(f8(B,A),C) | member(f14(A,C),A). [resolve(234,c,218,a)]. given #431 (T,wt=8): 5607 member(f24(c3),range_of(c4)) | empty(range_of(c4)). [resolve(5583,a,1446,b)]. given #432 (T,wt=8): 5611 member(f24(c3),range_of(c4)) | empty(f6(c3)). [resolve(5583,a,1110,b)]. given #433 (T,wt=6): 5793 empty(f6(c3)) | -empty(range_of(c4)). [resolve(5611,a,206,a)]. given #434 (T,wt=8): 5657 member(f24(c3),range_of(c4)) | ilf_type(c3,binary_relation_type). [resolve(5583,a,264,a)]. given #435 (A,wt=18): 344 A = B | member(f7(B,A),B) | member(f8(B,A),C) | -member(f14(A,C),C). [resolve(234,c,217,a)]. given #436 (T,wt=9): 5584 member(c3,A) | -member(power_set(range_of(c4)),power_set(A)). [resolve(5560,a,214,a)]. given #437 (T,wt=9): 5597 member(f24(c3),range_of(c4)) | empty(f24(power_set(c3))). [resolve(5583,a,4747,b)]. given #438 (T,wt=7): 5842 empty(f24(power_set(c3))) | -empty(range_of(c4)). [resolve(5597,a,206,a)]. given #439 (T,wt=9): 5598 member(f24(c3),range_of(c4)) | empty(f16(power_set(c3))). [resolve(5583,a,4666,b)]. given #440 (A,wt=19): 345 power_set(A) = B | member(f7(B,power_set(A)),B) | -member(C,f8(B,power_set(A))) | member(C,A). [resolve(234,c,214,c)]. given #441 (T,wt=7): 5864 empty(f16(power_set(c3))) | -empty(range_of(c4)). [resolve(5598,a,206,a)]. given #442 (T,wt=9): 5601 member(f24(c3),range_of(c4)) | empty(f23(power_set(c3))). [resolve(5583,a,4106,b)]. given #443 (T,wt=7): 5955 empty(f23(power_set(c3))) | -empty(range_of(c4)). [resolve(5601,a,206,a)]. given #444 (T,wt=9): 5602 member(f24(c3),range_of(c4)) | empty(f6(f6(c3))). [resolve(5583,a,2877,b)]. given #445 (A,wt=17): 346 A = B | member(f7(B,A),B) | member(f8(B,A),C) | -member(A,power_set(C)). [resolve(234,c,214,a)]. given #446 (T,wt=7): 5977 empty(f6(f6(c3))) | -empty(range_of(c4)). [resolve(5602,a,206,a)]. given #447 (T,wt=9): 5603 member(f24(c3),range_of(c4)) | empty(f6(range_of(c4))). [resolve(5583,a,2813,b)]. given #448 (T,wt=9): 5604 member(f24(c3),range_of(c4)) | ilf_type(range_of(c4),binary_relation_type). [resolve(5583,a,2486,b)]. given #449 (T,wt=9): 5605 member(f24(c3),range_of(c4)) | ilf_type(f6(c3),binary_relation_type). [resolve(5583,a,2254,b)]. given #450 (A,wt=16): 347 A = B | member(f7(B,A),B) | empty(A) | ilf_type(f8(B,A),member_type(A)). [resolve(234,c,212,c)]. given #451 (T,wt=7): 6100 ilf_type(f6(c3),binary_relation_type) | -empty(range_of(c4)). [resolve(5605,a,206,a)]. given #452 (T,wt=9): 5625 member(f23(f6(c3)),range_of(c4)) | empty(f6(c3)). [resolve(5583,a,675,a)]. given #453 (T,wt=9): 5627 member(f24(f6(c3)),range_of(c4)) | empty(f6(c3)). [resolve(5583,a,670,a)]. given #454 (T,wt=9): 5628 member(f16(f6(c3)),range_of(c4)) | empty(f6(c3)). [resolve(5583,a,668,a)]. given #455 (A,wt=27): 348 A = B | member(f7(B,A),B) | ordered_pair(f20(A,f8(B,A)),f21(A,f8(B,A))) = f8(B,A) | member(f22(A),A). [resolve(234,c,209,a)]. given #456 (T,wt=9): 5652 member(f24(c3),range_of(c4)) | member(c3,power_set(A)). [resolve(5583,a,289,b)]. given #457 (T,wt=9): 5770 empty(range_of(c4)) | ilf_type(f24(c3),member_type(range_of(c4))). [resolve(5607,a,212,c),merge(b)]. given #458 (T,wt=9): 5794 empty(f6(c3)) | member(f24(range_of(c4)),range_of(c4)). [resolve(5611,a,205,a)]. given #459 (T,wt=8): 6352 empty(f6(c3)) | member(f24(range_of(c4)),c3). [resolve(5794,b,580,a)]. given #460 (A,wt=29): 349 A = B | member(f7(B,A),B) | ordered_pair(f20(A,f8(B,A)),f21(A,f8(B,A))) = f8(B,A) | f22(A) != ordered_pair(C,D). [resolve(234,c,208,a)]. given #461 (T,wt=10): 1876 empty(c3) | member(f24(cross_product(c2,c3)),cross_product(c2,c3)). [resolve(1333,a,205,a)]. given #462 (T,wt=10): 1930 member(f24(c4),c4) | -member(A,c3) | member(A,B). [resolve(1855,a,214,c)]. given #463 (T,wt=10): 1939 member(c3,power_set(A)) | member(f24(c4),cross_product(c2,c3)). [resolve(1855,b,750,a)]. given #464 (T,wt=8): 6510 member(c3,power_set(A)) | -empty(cross_product(c2,c3)). [resolve(1939,b,206,a)]. given #465 (A,wt=12): 351 A = B | member(f7(B,A),B) | member(f24(A),A). [resolve(234,c,205,a)]. given #466 (T,wt=9): 6559 A = B | member(f24(A),A) | -empty(B). [resolve(351,b,206,a)]. given #467 (T,wt=10): 2117 ilf_type(c3,binary_relation_type) | member(f24(c2),A) | c2 != A. [resolve(2023,b,231,b)]. given #468 (T,wt=10): 2290 member(f14(A,B),A) | ilf_type(A,binary_relation_type) | -empty(B). [resolve(301,a,206,a)]. given #469 (T,wt=10): 2330 ilf_type(f6(c4),binary_relation_type) | member(f24(c4),cross_product(c2,c3)). [resolve(2254,b,750,a)]. given #470 (A,wt=29): 352 A = B | member(f7(B,A),B) | -ilf_type(A,subset_type(cross_product(C,D))) | ordered_pair(f18(A,f8(B,A)),f19(A,f8(B,A))) = f8(B,A). [resolve(234,c,131,b)]. given #471 (T,wt=8): 6623 ilf_type(f6(c4),binary_relation_type) | -empty(cross_product(c2,c3)). [resolve(2330,b,206,a)]. given #472 (T,wt=10): 2331 ilf_type(f6(domain_of(c4)),binary_relation_type) | member(f24(domain_of(c4)),c2). [resolve(2254,b,600,a)]. given #473 (T,wt=7): 6665 ilf_type(f6(domain_of(c4)),binary_relation_type) | -empty(c2). [resolve(2331,b,206,a)]. given #474 (T,wt=9): 6666 ilf_type(f6(domain_of(c4)),binary_relation_type) | member(f24(c2),c2). [resolve(2331,b,205,a)]. given #475 (A,wt=29): 353 A = B | member(f7(B,A),B) | ordered_pair(f18(A,f8(B,A)),f19(A,f8(B,A))) = f8(B,A) | f17(A) != ordered_pair(C,D). [resolve(234,c,127,a)]. given #476 (T,wt=10): 2332 ilf_type(f6(range_of(c4)),binary_relation_type) | member(f24(range_of(c4)),c3). [resolve(2254,b,580,a)]. given #477 (T,wt=7): 6706 ilf_type(f6(range_of(c4)),binary_relation_type) | -empty(c3). [resolve(2332,b,206,a)]. given #478 (T,wt=9): 6707 ilf_type(f6(range_of(c4)),binary_relation_type) | member(f24(c3),c3). [resolve(2332,b,205,a)]. given #479 (T,wt=10): 2333 ilf_type(f6(f6(A)),binary_relation_type) | member(f24(f6(A)),A). [resolve(2254,b,528,a)]. given #480 (A,wt=27): 354 A = B | member(f7(B,A),B) | ordered_pair(f18(A,f8(B,A)),f19(A,f8(B,A))) = f8(B,A) | member(f17(A),A). [resolve(234,c,125,a)]. given #481 (T,wt=7): 6777 ilf_type(f6(f6(A)),binary_relation_type) | -empty(A). [resolve(2333,b,206,a)]. given #482 (T,wt=9): 6778 ilf_type(f6(f6(A)),binary_relation_type) | member(f24(A),A). [resolve(2333,b,205,a)]. given #483 (T,wt=10): 2455 member(f13(power_set(A),B),power_set(A)) | member(A,B). [resolve(302,b,282,a)]. given #484 (T,wt=9): 6943 member(A,A) | -member(A,f13(power_set(A),A)). [factor(6934,a,c)]. given #485 (A,wt=26): 355 A = B | member(f7(B,A),B) | ordered_pair(f18(A,f8(B,A)),f19(A,f8(B,A))) = f8(B,A) | -ilf_type(A,binary_relation_type). [resolve(234,c,123,a)]. given #486 (T,wt=10): 2653 -member(A,f5(B,C)) | member(A,cross_product(C,B)). [resolve(2638,a,214,c)]. given #487 (T,wt=10): 2885 empty(f6(f6(c4))) | member(f24(c4),cross_product(c2,c3)). [resolve(2877,b,750,a)]. given #488 (T,wt=8): 7035 empty(f6(f6(c4))) | -empty(cross_product(c2,c3)). [resolve(2885,b,206,a)]. given #489 (T,wt=10): 2886 empty(f6(f6(domain_of(c4)))) | member(f24(domain_of(c4)),c2). [resolve(2877,b,600,a)]. given #490 (A,wt=18): 356 c3 = A | member(f7(A,c3),A) | member(ordered_pair(f25(f8(A,c3)),f8(A,c3)),c4). [resolve(234,c,116,a)]. given #491 (T,wt=7): 7057 empty(f6(f6(domain_of(c4)))) | -empty(c2). [resolve(2886,b,206,a)]. given #492 (T,wt=9): 7058 empty(f6(f6(domain_of(c4)))) | member(f24(c2),c2). [resolve(2886,b,205,a)]. given #493 (T,wt=10): 2887 empty(f6(f6(range_of(c4)))) | member(f24(range_of(c4)),c3). [resolve(2877,b,580,a)]. given #494 (T,wt=7): 7123 empty(f6(f6(range_of(c4)))) | -empty(c3). [resolve(2887,b,206,a)]. given #495 (A,wt=19): 357 power_set(A) = A | member(f7(A,power_set(A)),A) | -member(f7(A,power_set(A)),f8(A,power_set(A))). [factor(345,b,d)]. given #496 (T,wt=9): 7124 empty(f6(f6(range_of(c4)))) | member(f24(c3),c3). [resolve(2887,b,205,a)]. given #497 (T,wt=10): 2888 empty(f6(f6(f6(A)))) | member(f24(f6(A)),A). [resolve(2877,b,528,a)]. given #498 (T,wt=7): 7195 empty(f6(f6(f6(A)))) | -empty(A). [resolve(2888,b,206,a)]. given #499 (T,wt=9): 7196 empty(f6(f6(f6(A)))) | member(f24(A),A). [resolve(2888,b,205,a)]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 38 (0.00 of 0.84 sec). given #500 (A,wt=11): 362 A = B | -subset(A,B) | member(f13(B,A),B). [resolve(242,b,221,a)]. given #501 (T,wt=10): 3319 -member(A,domain_of(f6(cross_product(B,C)))) | member(A,B). [resolve(3215,a,214,c)]. given #502 (T,wt=10): 3343 -member(A,range_of(f6(cross_product(B,C)))) | member(A,C). [resolve(3327,a,214,c)]. given #503 (T,wt=10): 3379 ilf_type(domain_of(f16(power_set(cross_product(A,B)))),member_type(power_set(A))). [resolve(1982,a,237,b)]. given #504 (T,wt=9): 7385 member(domain_of(f16(power_set(cross_product(A,B)))),power_set(A)). [resolve(3379,a,211,c),unit_del(a,213)]. given #505 (A,wt=11): 363 A = B | -subset(B,A) | member(f13(A,B),A). [resolve(242,c,221,a)]. given #506 (T,wt=10): 3380 ilf_type(domain_of(f16(power_set(cross_product(cross_product(A,B),C)))),binary_relation_type). [resolve(1982,a,129,a)]. given #507 (T,wt=10): 3388 ilf_type(range_of(f16(power_set(cross_product(A,B)))),member_type(power_set(B))). [resolve(1984,a,237,b)]. given #508 (T,wt=9): 7412 member(range_of(f16(power_set(cross_product(A,B)))),power_set(B)). [resolve(3388,a,211,c),unit_del(a,213)]. given #509 (T,wt=10): 3389 ilf_type(range_of(f16(power_set(cross_product(A,cross_product(B,C))))),binary_relation_type). [resolve(1984,a,129,a)]. given #510 (A,wt=11): 364 domain(A,B,f5(B,A)) = domain_of(f5(B,A)). [resolve(243,a,204,a)]. given #511 (T,wt=10): 3478 ilf_type(domain_of(f23(power_set(cross_product(A,B)))),member_type(power_set(A))). [resolve(2216,a,237,b)]. given #512 (T,wt=9): 7439 member(domain_of(f23(power_set(cross_product(A,B)))),power_set(A)). [resolve(3478,a,211,c),unit_del(a,213)]. given #513 (T,wt=10): 3479 ilf_type(domain_of(f23(power_set(cross_product(cross_product(A,B),C)))),binary_relation_type). [resolve(2216,a,129,a)]. given #514 (T,wt=10): 3483 ilf_type(range_of(f23(power_set(cross_product(A,B)))),member_type(power_set(B))). [resolve(2218,a,237,b)]. given #515 (A,wt=11): 366 range(A,B,f5(B,A)) = range_of(f5(B,A)). [resolve(243,a,202,a)]. given #516 (T,wt=9): 7466 member(range_of(f23(power_set(cross_product(A,B)))),power_set(B)). [resolve(3483,a,211,c),unit_del(a,213)]. given #517 (T,wt=10): 3484 ilf_type(range_of(f23(power_set(cross_product(A,cross_product(B,C))))),binary_relation_type). [resolve(2218,a,129,a)]. given #518 (T,wt=10): 3488 ilf_type(domain_of(f24(power_set(cross_product(A,B)))),member_type(power_set(A))). [resolve(2220,a,237,b)]. given #519 (T,wt=9): 7493 member(domain_of(f24(power_set(cross_product(A,B)))),power_set(A)). [resolve(3488,a,211,c),unit_del(a,213)]. given #520 (A,wt=16): 372 member(f3(A,B),A) | B = A | member(f4(A,B),C) | B != C. [resolve(250,b,231,b)]. given #521 (T,wt=10): 3489 ilf_type(domain_of(f24(power_set(cross_product(cross_product(A,B),C)))),binary_relation_type). [resolve(2220,a,129,a)]. given #522 (T,wt=10): 3494 ilf_type(range_of(f24(power_set(cross_product(A,B)))),member_type(power_set(B))). [resolve(2222,a,237,b)]. given #523 (T,wt=9): 7520 member(range_of(f24(power_set(cross_product(A,B)))),power_set(B)). [resolve(3494,a,211,c),unit_del(a,213)]. given #524 (T,wt=10): 3495 ilf_type(range_of(f24(power_set(cross_product(A,cross_product(B,C))))),binary_relation_type). [resolve(2222,a,129,a)]. given #525 (A,wt=23): 373 member(f3(A,B),A) | B = A | member(f4(A,B),C) | member(f9(C,B),C) | -member(f10(C,B),C). [resolve(250,b,230,b)]. given #526 (T,wt=10): 3501 unordered_pair(singleton(A),unordered_pair(A,B)) = ordered_pair(A,B). [para(371(a,1),239(a,1)),flip(a)]. given #527 (T,wt=10): 3502 unordered_pair(unordered_pair(A,B),singleton(B)) = ordered_pair(B,A). [para(239(a,1),371(a,1,1))]. given #528 (T,wt=10): 3598 empty(c3) | member(f24(c3),A) | range_of(c4) != A. [resolve(3574,b,231,b)]. given #529 (T,wt=10): 3643 empty(c3) | member(f25(f24(c3)),A) | c2 != A. [resolve(3617,b,231,b)]. given #530 (A,wt=23): 374 member(f3(A,B),A) | B = A | member(f4(A,B),C) | member(f9(C,B),C) | member(f10(C,B),B). [resolve(250,b,229,b)]. given #531 (T,wt=10): 3655 empty(c3) | empty(c2) | ilf_type(f25(f24(c3)),member_type(c2)). [resolve(3617,b,212,c)]. given #532 (T,wt=10): 3721 empty(c3) | member(f16(c3),A) | range_of(c4) != A. [resolve(3697,b,231,b)]. given #533 (T,wt=10): 3766 empty(c3) | member(f25(f16(c3)),A) | c2 != A. [resolve(3744,b,231,b)]. given #534 (T,wt=10): 3778 empty(c3) | empty(c2) | ilf_type(f25(f16(c3)),member_type(c2)). [resolve(3744,b,212,c)]. given #535 (A,wt=23): 375 member(f3(A,B),A) | B = A | member(f4(A,B),C) | -member(f9(C,B),B) | -member(f10(C,B),C). [resolve(250,b,228,b)]. given #536 (T,wt=10): 3841 ilf_type(domain_of(domain_of(f5(A,cross_product(B,C)))),subset_type(B)). [resolve(634,a,203,a),rewrite([3840(4)])]. given #537 (T,wt=10): 3843 ilf_type(range_of(domain_of(f5(A,cross_product(B,C)))),subset_type(C)). [resolve(634,a,201,a),rewrite([3842(4)])]. given #538 (T,wt=10): 3845 ilf_type(domain_of(range_of(f5(cross_product(A,B),C))),subset_type(A)). [resolve(638,a,203,a),rewrite([3844(4)])]. given #539 (T,wt=10): 3847 ilf_type(range_of(range_of(f5(cross_product(A,B),C))),subset_type(B)). [resolve(638,a,201,a),rewrite([3846(4)])]. given #540 (A,wt=23): 376 member(f3(A,B),A) | B = A | member(f4(A,B),C) | -member(f9(C,B),B) | member(f10(C,B),B). [resolve(250,b,227,b)]. given #541 (T,wt=10): 4060 ilf_type(domain_of(domain_of(cross_product(cross_product(A,B),C))),subset_type(A)). [resolve(820,a,203,a),rewrite([4059(4)])]. given #542 (T,wt=10): 4062 ilf_type(range_of(domain_of(cross_product(cross_product(A,B),C))),subset_type(B)). [resolve(820,a,201,a),rewrite([4061(4)])]. given #543 (T,wt=10): 4064 ilf_type(domain_of(range_of(cross_product(A,cross_product(B,C)))),subset_type(B)). [resolve(824,a,203,a),rewrite([4063(4)])]. given #544 (T,wt=10): 4066 ilf_type(range_of(range_of(cross_product(A,cross_product(B,C)))),subset_type(C)). [resolve(824,a,201,a),rewrite([4065(4)])]. given #545 (A,wt=16): 377 member(f3(A,B),A) | B = A | member(f4(A,B),C) | C != B. [resolve(250,b,226,b)]. given #546 (T,wt=10): 4204 empty(f23(power_set(c4))) | member(f24(c4),cross_product(c2,c3)). [resolve(4106,b,750,a)]. given #547 (T,wt=8): 7737 empty(f23(power_set(c4))) | -empty(cross_product(c2,c3)). [resolve(4204,b,206,a)]. given #548 (T,wt=10): 4206 empty(f23(power_set(domain_of(c4)))) | member(f24(domain_of(c4)),c2). [resolve(4106,b,600,a)]. given #549 (T,wt=7): 7759 empty(f23(power_set(domain_of(c4)))) | -empty(c2). [resolve(4206,b,206,a)]. given #550 (A,wt=23): 378 member(f3(A,B),A) | B = A | member(f4(A,B),C) | member(f11(B,C),B) | -member(f12(B,C),B). [resolve(250,b,225,b)]. given #551 (T,wt=9): 7760 empty(f23(power_set(domain_of(c4)))) | member(f24(c2),c2). [resolve(4206,b,205,a)]. given #552 (T,wt=10): 4207 empty(f23(power_set(range_of(c4)))) | member(f24(range_of(c4)),c3). [resolve(4106,b,580,a)]. given #553 (T,wt=7): 7804 empty(f23(power_set(range_of(c4)))) | -empty(c3). [resolve(4207,b,206,a)]. given #554 (T,wt=9): 7805 empty(f23(power_set(range_of(c4)))) | member(f24(c3),c3). [resolve(4207,b,205,a)]. given #555 (A,wt=23): 379 member(f3(A,B),A) | B = A | member(f4(A,B),C) | member(f11(B,C),B) | member(f12(B,C),C). [resolve(250,b,224,b)]. given #556 (T,wt=10): 4208 empty(f23(power_set(f6(A)))) | member(f24(f6(A)),A). [resolve(4106,b,528,a)]. given #557 (T,wt=7): 7991 empty(f23(power_set(f6(A)))) | -empty(A). [resolve(4208,b,206,a)]. given #558 (T,wt=9): 7992 empty(f23(power_set(f6(A)))) | member(f24(A),A). [resolve(4208,b,205,a)]. given #559 (T,wt=10): 4382 member(f24(c2),c2) | ilf_type(domain_of(c4),member_type(power_set(A))). [resolve(4363,a,212,c),unit_del(b,213)]. given #560 (A,wt=23): 380 member(f3(A,B),A) | B = A | member(f4(A,B),C) | -member(f11(B,C),C) | -member(f12(B,C),B). [resolve(250,b,223,b)]. given #561 (T,wt=8): 8055 ilf_type(domain_of(c4),member_type(power_set(A))) | -empty(c2). [resolve(4382,a,206,a)]. given #562 (T,wt=10): 4468 member(f24(c3),c3) | ilf_type(range_of(c4),member_type(power_set(A))). [resolve(4444,a,212,c),unit_del(b,213)]. given #563 (T,wt=8): 8081 ilf_type(range_of(c4),member_type(power_set(A))) | -empty(c3). [resolve(4468,a,206,a)]. given #564 (T,wt=10): 4579 member(f24(A),A) | ilf_type(f6(A),member_type(power_set(B))). [resolve(4554,a,212,c),unit_del(b,213)]. given #565 (A,wt=23): 381 member(f3(A,B),A) | B = A | member(f4(A,B),C) | -member(f11(B,C),C) | member(f12(B,C),C). [resolve(250,b,222,b)]. given #566 (T,wt=8): 8124 ilf_type(f6(A),member_type(power_set(B))) | -empty(A). [resolve(4579,a,206,a)]. given #567 (T,wt=10): 4676 empty(f16(power_set(c4))) | member(f24(c4),cross_product(c2,c3)). [resolve(4666,b,750,a)]. given #568 (T,wt=8): 8150 empty(f16(power_set(c4))) | -empty(cross_product(c2,c3)). [resolve(4676,b,206,a)]. given #569 (T,wt=10): 4678 empty(f16(power_set(domain_of(c4)))) | member(f24(domain_of(c4)),c2). [resolve(4666,b,600,a)]. given #570 (A,wt=18): 382 member(f3(A,B),A) | B = A | member(f4(A,B),C) | member(f14(B,C),B). [resolve(250,b,218,a)]. given #571 (T,wt=7): 8172 empty(f16(power_set(domain_of(c4)))) | -empty(c2). [resolve(4678,b,206,a)]. given #572 (T,wt=9): 8173 empty(f16(power_set(domain_of(c4)))) | member(f24(c2),c2). [resolve(4678,b,205,a)]. given #573 (T,wt=10): 4679 empty(f16(power_set(range_of(c4)))) | member(f24(range_of(c4)),c3). [resolve(4666,b,580,a)]. given #574 (T,wt=7): 8322 empty(f16(power_set(range_of(c4)))) | -empty(c3). [resolve(4679,b,206,a)]. given #575 (A,wt=18): 383 member(f3(A,B),A) | B = A | member(f4(A,B),C) | -member(f14(B,C),C). [resolve(250,b,217,a)]. given #576 (T,wt=9): 8323 empty(f16(power_set(range_of(c4)))) | member(f24(c3),c3). [resolve(4679,b,205,a)]. given #577 (T,wt=10): 4680 empty(f16(power_set(f6(A)))) | member(f24(f6(A)),A). [resolve(4666,b,528,a)]. given #578 (T,wt=7): 8400 empty(f16(power_set(f6(A)))) | -empty(A). [resolve(4680,b,206,a)]. given #579 (T,wt=9): 8401 empty(f16(power_set(f6(A)))) | member(f24(A),A). [resolve(4680,b,205,a)]. given #580 (A,wt=19): 384 member(f3(A,power_set(B)),A) | power_set(B) = A | -member(C,f4(A,power_set(B))) | member(C,B). [resolve(250,b,214,c)]. given #581 (T,wt=10): 4757 empty(f24(power_set(c4))) | member(f24(c4),cross_product(c2,c3)). [resolve(4747,b,750,a)]. given #582 (T,wt=8): 8559 empty(f24(power_set(c4))) | -empty(cross_product(c2,c3)). [resolve(4757,b,206,a)]. given #583 (T,wt=10): 4759 empty(f24(power_set(domain_of(c4)))) | member(f24(domain_of(c4)),c2). [resolve(4747,b,600,a)]. given #584 (T,wt=7): 8581 empty(f24(power_set(domain_of(c4)))) | -empty(c2). [resolve(4759,b,206,a)]. given #585 (A,wt=17): 385 member(f3(A,B),A) | B = A | member(f4(A,B),C) | -member(B,power_set(C)). [resolve(250,b,214,a)]. given #586 (T,wt=9): 8582 empty(f24(power_set(domain_of(c4)))) | member(f24(c2),c2). [resolve(4759,b,205,a)]. given #587 (T,wt=10): 4760 empty(f24(power_set(range_of(c4)))) | member(f24(range_of(c4)),c3). [resolve(4747,b,580,a)]. given #588 (T,wt=7): 8707 empty(f24(power_set(range_of(c4)))) | -empty(c3). [resolve(4760,b,206,a)]. given #589 (T,wt=9): 8708 empty(f24(power_set(range_of(c4)))) | member(f24(c3),c3). [resolve(4760,b,205,a)]. given #590 (A,wt=16): 386 member(f3(A,B),A) | B = A | empty(B) | ilf_type(f4(A,B),member_type(B)). [resolve(250,b,212,c)]. given #591 (T,wt=10): 4761 empty(f24(power_set(f6(A)))) | member(f24(f6(A)),A). [resolve(4747,b,528,a)]. given #592 (T,wt=7): 8837 empty(f24(power_set(f6(A)))) | -empty(A). [resolve(4761,b,206,a)]. given #593 (T,wt=9): 8838 empty(f24(power_set(f6(A)))) | member(f24(A),A). [resolve(4761,b,205,a)]. given #594 (T,wt=10): 5566 member(c3,power_set(A)) | member(f24(range_of(c4)),range_of(c4)). [resolve(1836,b,205,a)]. given #595 (A,wt=27): 387 member(f3(A,B),A) | B = A | ordered_pair(f20(B,f4(A,B)),f21(B,f4(A,B))) = f4(A,B) | member(f22(B),B). [resolve(250,b,209,a)]. given #596 (T,wt=9): 8910 member(c3,power_set(A)) | member(f24(range_of(c4)),c3). [resolve(5566,b,580,a)]. given #597 (T,wt=10): 5582 member(c3,A) | -member(f14(power_set(range_of(c4)),A),A). [resolve(5560,a,217,a)]. given #598 (T,wt=10): 5599 member(f24(c3),range_of(c4)) | member(f6(c3),power_set(A)). [resolve(5583,a,4554,b)]. given #599 (T,wt=8): 9100 member(f6(c3),power_set(A)) | -empty(range_of(c4)). [resolve(5599,a,206,a)]. given #600 (A,wt=29): 388 member(f3(A,B),A) | B = A | ordered_pair(f20(B,f4(A,B)),f21(B,f4(A,B))) = f4(A,B) | f22(B) != ordered_pair(C,D). [resolve(250,b,208,a)]. given #601 (T,wt=10): 5600 member(f24(c3),range_of(c4)) | member(range_of(c4),power_set(A)). [resolve(5583,a,4444,b)]. given #602 (T,wt=10): 5606 member(f14(c3,A),range_of(c4)) | member(c3,power_set(A)). [resolve(5583,a,2053,a)]. given #603 (T,wt=10): 5610 member(f24(f6(c3)),range_of(c4)) | empty(f6(f6(c3))). [resolve(5583,a,1118,b)]. given #604 (T,wt=10): 5620 member(f24(c3),range_of(c4)) | ilf_type(c3,member_type(power_set(A))). [resolve(5583,a,910,a)]. given #605 (A,wt=12): 390 member(f3(A,B),A) | B = A | member(f24(B),B). [resolve(250,b,205,a)]. given #606 (T,wt=8): 9229 ilf_type(c3,member_type(power_set(A))) | -empty(range_of(c4)). [resolve(5620,a,206,a)]. given #607 (T,wt=10): 5624 member(f17(f6(c3)),range_of(c4)) | ilf_type(f6(c3),binary_relation_type). [resolve(5583,a,676,a)]. given #608 (T,wt=10): 5626 member(f24(f6(c3)),range_of(c4)) | ilf_type(f6(c3),binary_relation_type). [resolve(5583,a,671,a)]. given #609 (T,wt=10): 5843 empty(f24(power_set(c3))) | member(f24(range_of(c4)),range_of(c4)). [resolve(5597,a,205,a)]. given #610 (A,wt=29): 391 member(f3(A,B),A) | B = A | -ilf_type(B,subset_type(cross_product(C,D))) | ordered_pair(f18(B,f4(A,B)),f19(B,f4(A,B))) = f4(A,B). [resolve(250,b,131,b)]. given #611 (T,wt=9): 9373 empty(f24(power_set(c3))) | member(f24(range_of(c4)),c3). [resolve(5843,b,580,a)]. given #612 (T,wt=10): 5865 empty(f16(power_set(c3))) | member(f24(range_of(c4)),range_of(c4)). [resolve(5598,a,205,a)]. given #613 (T,wt=9): 9443 empty(f16(power_set(c3))) | member(f24(range_of(c4)),c3). [resolve(5865,b,580,a)]. given #614 (T,wt=10): 5956 empty(f23(power_set(c3))) | member(f24(range_of(c4)),range_of(c4)). [resolve(5601,a,205,a)]. given #615 (A,wt=29): 392 member(f3(A,B),A) | B = A | ordered_pair(f18(B,f4(A,B)),f19(B,f4(A,B))) = f4(A,B) | f17(B) != ordered_pair(C,D). [resolve(250,b,127,a)]. given #616 (T,wt=9): 9485 empty(f23(power_set(c3))) | member(f24(range_of(c4)),c3). [resolve(5956,b,580,a)]. given #617 (T,wt=10): 5978 empty(f6(f6(c3))) | member(f24(range_of(c4)),range_of(c4)). [resolve(5602,a,205,a)]. given #618 (T,wt=9): 9527 empty(f6(f6(c3))) | member(f24(range_of(c4)),c3). [resolve(5978,b,580,a)]. given #619 (T,wt=10): 6101 ilf_type(f6(c3),binary_relation_type) | member(f24(range_of(c4)),range_of(c4)). [resolve(5605,a,205,a)]. given #620 (A,wt=27): 393 member(f3(A,B),A) | B = A | ordered_pair(f18(B,f4(A,B)),f19(B,f4(A,B))) = f4(A,B) | member(f17(B),B). [resolve(250,b,125,a)]. given #621 (T,wt=9): 9569 ilf_type(f6(c3),binary_relation_type) | member(f24(range_of(c4)),c3). [resolve(6101,b,580,a)]. given #622 (T,wt=10): 6516 member(f24(c4),cross_product(c2,c3)) | -member(f24(c4),c3). [factor(6486,a,c)]. given #623 (T,wt=10): 6713 ilf_type(f6(range_of(c4)),binary_relation_type) | member(f24(c3),range_of(c4)). [resolve(6707,b,5583,a)]. given #624 (T,wt=10): 6877 ilf_type(f6(f6(c3)),binary_relation_type) | member(f24(c3),range_of(c4)). [resolve(6778,b,5583,a)]. given #625 (A,wt=26): 394 member(f3(A,B),A) | B = A | ordered_pair(f18(B,f4(A,B)),f19(B,f4(A,B))) = f4(A,B) | -ilf_type(B,binary_relation_type). [resolve(250,b,123,a)]. given #626 (T,wt=8): 9749 ilf_type(f6(f6(c3)),binary_relation_type) | -empty(range_of(c4)). [resolve(6877,b,206,a)]. given #627 (T,wt=10): 7082 c3 = A | member(f7(A,c3),A) | -empty(c4). [resolve(356,c,206,a)]. given #628 (T,wt=10): 7130 empty(f6(f6(range_of(c4)))) | member(f24(c3),range_of(c4)). [resolve(7124,b,5583,a)]. given #629 (T,wt=10): 7202 empty(f6(f6(f6(c3)))) | member(f24(c3),range_of(c4)). [resolve(7196,b,5583,a)]. given #630 (A,wt=18): 395 member(f3(A,c3),A) | c3 = A | member(ordered_pair(f25(f4(A,c3)),f4(A,c3)),c4). [resolve(250,b,116,a)]. given #631 (T,wt=8): 9792 empty(f6(f6(f6(c3)))) | -empty(range_of(c4)). [resolve(7202,b,206,a)]. given #632 (T,wt=10): 7551 unordered_pair(singleton(A),unordered_pair(B,A)) = ordered_pair(A,B). [para(239(a,1),3501(a,1,2))]. given #633 (T,wt=10): 7811 empty(f23(power_set(range_of(c4)))) | member(f24(c3),range_of(c4)). [resolve(7805,b,5583,a)]. given #634 (T,wt=10): 7998 empty(f23(power_set(f6(c3)))) | member(f24(c3),range_of(c4)). [resolve(7992,b,5583,a)]. given #635 (A,wt=19): 396 member(f3(A,power_set(A)),A) | power_set(A) = A | -member(f3(A,power_set(A)),f4(A,power_set(A))). [factor(384,a,d)]. given #636 (T,wt=8): 9859 empty(f23(power_set(f6(c3)))) | -empty(range_of(c4)). [resolve(7998,b,206,a)]. given #637 (T,wt=10): 8333 empty(f16(power_set(range_of(c4)))) | member(f24(c3),range_of(c4)). [resolve(8323,b,5583,a)]. given #638 (T,wt=10): 8407 empty(f16(power_set(f6(c3)))) | member(f24(c3),range_of(c4)). [resolve(8401,b,5583,a)]. given #639 (T,wt=8): 9901 empty(f16(power_set(f6(c3)))) | -empty(range_of(c4)). [resolve(8407,b,206,a)]. given #640 (A,wt=26): 397 -ilf_type(A,binary_relation_type) | member(ordered_pair(f1(A,f4(B,range_of(A))),f4(B,range_of(A))),A) | member(f3(B,range_of(A)),B) | range_of(A) = B. [resolve(254,c,250,b)]. given #641 (T,wt=10): 8714 empty(f24(power_set(range_of(c4)))) | member(f24(c3),range_of(c4)). [resolve(8708,b,5583,a)]. given #642 (T,wt=10): 8844 empty(f24(power_set(f6(c3)))) | member(f24(c3),range_of(c4)). [resolve(8838,b,5583,a)]. given #643 (T,wt=8): 9963 empty(f24(power_set(f6(c3)))) | -empty(range_of(c4)). [resolve(8844,b,206,a)]. given #644 (T,wt=10): 9053 member(f24(range_of(c4)),c3) | ilf_type(c3,member_type(power_set(A))). [resolve(8910,a,212,c),unit_del(b,213)]. given #645 (A,wt=26): 398 -ilf_type(A,binary_relation_type) | member(ordered_pair(f1(A,f8(B,range_of(A))),f8(B,range_of(A))),A) | range_of(A) = B | member(f7(B,range_of(A)),B). [resolve(254,c,234,c)]. given #646 (T,wt=10): 9128 member(f24(c3),range_of(c4)) | -member(f24(c3),f6(c3)). [factor(9120,a,c)]. given #647 (T,wt=10): 9817 member(f3(A,c3),A) | c3 = A | -empty(c4). [resolve(395,c,206,a)]. given #648 (T,wt=11): 465 empty(A) | member(f24(A),B) | member(f14(A,B),A). [resolve(265,b,218,a)]. given #649 (T,wt=11): 466 empty(A) | member(f24(A),B) | -member(f14(A,B),B). [resolve(265,b,217,a)]. given #650 (A,wt=21): 399 -ilf_type(A,binary_relation_type) | member(ordered_pair(f1(A,f15(range_of(A),B)),f15(range_of(A),B)),A) | member(range_of(A),power_set(B)). [resolve(254,c,216,b)]. given #651 (T,wt=11): 488 empty(A) | member(f16(A),B) | member(f14(A,B),A). [resolve(275,b,218,a)]. given #652 (T,wt=11): 489 empty(A) | member(f16(A),B) | -member(f14(A,B),B). [resolve(275,b,217,a)]. given #653 (T,wt=11): 513 ilf_type(A,binary_relation_type) | member(f24(A),B) | -member(A,power_set(B)). [resolve(264,a,214,a)]. given #654 (T,wt=11): 516 ilf_type(c3,binary_relation_type) | member(ordered_pair(f25(f24(c3)),f24(c3)),c4). [resolve(264,a,116,a)]. given #655 (A,wt=17): 400 -ilf_type(A,binary_relation_type) | member(ordered_pair(f1(A,f23(range_of(A))),f23(range_of(A))),A) | empty(range_of(A)). [resolve(254,c,207,b)]. given #656 (T,wt=9): 10339 ilf_type(c3,binary_relation_type) | member(f25(f24(c3)),domain_of(c4)). [resolve(516,b,252,b),unit_del(b,540)]. given #657 (T,wt=8): 10379 ilf_type(c3,binary_relation_type) | member(f25(f24(c3)),c2). [resolve(10339,b,600,a)]. given #658 (T,wt=11): 526 member(f6(A),B) | member(f14(power_set(A),B),power_set(A)). [resolve(499,a,218,a)]. given #659 (T,wt=9): 10470 member(f14(power_set(A),B),power_set(A)) | -empty(B). [resolve(526,a,206,a)]. given #660 (A,wt=18): 401 -ilf_type(A,binary_relation_type) | member(ordered_pair(f1(A,f17(range_of(A))),f17(range_of(A))),A) | ilf_type(range_of(A),binary_relation_type). [resolve(254,c,119,a)]. given #661 (T,wt=11): 559 member(f24(power_set(A)),B) | -member(f14(power_set(A),B),B). [resolve(444,a,217,a)]. given #662 (T,wt=11): 578 member(range_of(c4),A) | member(f14(power_set(c3),A),power_set(c3)). [resolve(568,a,218,a)]. given #663 (T,wt=11): 598 member(domain_of(c4),A) | member(f14(power_set(c2),A),power_set(c2)). [resolve(588,a,218,a)]. given #664 (T,wt=11): 652 ilf_type(c3,binary_relation_type) | member(f24(c4),A) | -member(c4,power_set(A)). [resolve(421,b,214,a)]. given #665 (A,wt=14): 405 ilf_type(c3,binary_relation_type) | member(ordered_pair(f25(f17(c3)),f17(c3)),A) | c4 != A. [resolve(256,b,231,b)]. given #666 (T,wt=11): 660 domain(A,B,cross_product(A,B)) = domain_of(cross_product(A,B)). [resolve(452,a,204,a)]. given #667 (T,wt=11): 662 range(A,B,cross_product(A,B)) = range_of(cross_product(A,B)). [resolve(452,a,202,a)]. given #668 (T,wt=11): 674 member(f15(f6(A),B),A) | member(f6(A),power_set(B)). [resolve(528,a,216,b)]. given #669 (T,wt=11): 678 empty(c3) | member(ordered_pair(f2(c4,f23(c3)),f23(c3)),c4). [resolve(270,b,253,c),unit_del(b,540)]. given #670 (A,wt=21): 406 ilf_type(c3,binary_relation_type) | member(ordered_pair(f25(f17(c3)),f17(c3)),A) | member(f9(A,c4),A) | -member(f10(A,c4),A). [resolve(256,b,230,b)]. given #671 (T,wt=9): 10762 empty(c3) | member(f2(c4,f23(c3)),domain_of(c4)). [resolve(678,b,252,b),unit_del(b,540)]. given #672 (T,wt=8): 10786 empty(c3) | member(f2(c4,f23(c3)),c2). [resolve(10762,b,600,a)]. given #673 (T,wt=11): 710 empty(c3) | member(f24(c4),A) | member(f14(c4,A),c4). [resolve(696,b,218,a)]. given #674 (T,wt=9): 10875 empty(c3) | member(f14(c4,A),c4) | -empty(A). [resolve(710,b,206,a)]. given #675 (A,wt=21): 407 ilf_type(c3,binary_relation_type) | member(ordered_pair(f25(f17(c3)),f17(c3)),A) | member(f9(A,c4),A) | member(f10(A,c4),c4). [resolve(256,b,229,b)]. given #676 (T,wt=11): 711 empty(c3) | member(f24(c4),A) | -member(f14(c4,A),A). [resolve(696,b,217,a)]. given #677 (T,wt=11): 730 member(f16(power_set(A)),B) | -member(f14(power_set(A),B),B). [resolve(719,a,217,a)]. given #678 (T,wt=11): 749 member(c4,A) | -member(f14(power_set(cross_product(c2,c3)),A),A). [resolve(738,a,217,a)]. given #679 (T,wt=11): 764 member(f15(range_of(c4),A),c3) | member(range_of(c4),power_set(A)). [resolve(580,a,216,b)]. given #680 (A,wt=21): 408 ilf_type(c3,binary_relation_type) | member(ordered_pair(f25(f17(c3)),f17(c3)),A) | -member(f9(A,c4),c4) | -member(f10(A,c4),A). [resolve(256,b,228,b)]. given #681 (T,wt=11): 773 member(f15(domain_of(c4),A),c2) | member(domain_of(c4),power_set(A)). [resolve(600,a,216,b)]. given #682 (T,wt=11): 787 member(f23(power_set(A)),B) | -member(f14(power_set(A),B),B). [resolve(776,a,217,a)]. given #683 (T,wt=11): 847 empty(c3) | member(ordered_pair(f1(c4,f23(c3)),f23(c3)),c4). [resolve(677,b,254,c),unit_del(b,540)]. given #684 (T,wt=9): 11048 empty(c3) | member(f1(c4,f23(c3)),domain_of(c4)). [resolve(847,b,252,b),unit_del(b,540)]. given #685 (A,wt=21): 409 ilf_type(c3,binary_relation_type) | member(ordered_pair(f25(f17(c3)),f17(c3)),A) | -member(f9(A,c4),c4) | member(f10(A,c4),c4). [resolve(256,b,227,b)]. given #686 (T,wt=8): 11068 empty(c3) | member(f1(c4,f23(c3)),c2). [resolve(11048,b,600,a)]. given #687 (T,wt=11): 859 empty(c3) | member(f23(c3),A) | -member(range_of(c4),power_set(A)). [resolve(677,b,214,a)]. given #688 (T,wt=11): 860 empty(c3) | empty(range_of(c4)) | ilf_type(f23(c3),member_type(range_of(c4))). [resolve(677,b,212,c)]. given #689 (T,wt=11): 874 member(f24(f23(power_set(A))),A) | ilf_type(f23(power_set(A)),binary_relation_type). [resolve(280,a,264,a)]. given #690 (A,wt=21): 410 ilf_type(c3,binary_relation_type) | member(ordered_pair(f25(f17(c3)),f17(c3)),A) | member(f11(c4,A),c4) | -member(f12(c4,A),c4). [resolve(256,b,225,b)]. given #691 (T,wt=7): 11161 ilf_type(f23(power_set(A)),binary_relation_type) | -empty(A). [resolve(874,a,206,a)]. given #692 (T,wt=9): 11162 ilf_type(f23(power_set(A)),binary_relation_type) | member(f24(A),A). [resolve(874,a,205,a)]. given #693 (T,wt=10): 11168 ilf_type(f23(power_set(c3)),binary_relation_type) | member(f24(c3),range_of(c4)). [resolve(11162,b,5583,a)]. given #694 (T,wt=8): 11227 ilf_type(f23(power_set(c3)),binary_relation_type) | -empty(range_of(c4)). [resolve(11168,b,206,a)]. given #695 (A,wt=21): 411 ilf_type(c3,binary_relation_type) | member(ordered_pair(f25(f17(c3)),f17(c3)),A) | member(f11(c4,A),c4) | member(f12(c4,A),A). [resolve(256,b,224,b)]. Low Water (keep, True_semantics): wt=65 given #696 (T,wt=11): 879 member(f17(f23(power_set(A))),A) | ilf_type(f23(power_set(A)),binary_relation_type). [resolve(280,a,119,a)]. given #697 (T,wt=11): 889 member(f24(A),A) | member(A,B) | power_set(C) != B. [resolve(289,a,231,b)]. given #698 (T,wt=11): 926 member(A,power_set(B)) | member(f24(A),C) | A != C. [resolve(289,b,231,b)]. given #699 (T,wt=11): 931 member(A,power_set(B)) | member(f24(A),C) | C != A. [resolve(289,b,226,b)]. given #700 (A,wt=21): 412 ilf_type(c3,binary_relation_type) | member(ordered_pair(f25(f17(c3)),f17(c3)),A) | -member(f11(c4,A),A) | -member(f12(c4,A),c4). [resolve(256,b,223,b)]. given #701 (T,wt=11): 972 member(f24(f24(power_set(A))),A) | ilf_type(f24(power_set(A)),binary_relation_type). [resolve(467,a,264,a)]. given #702 (T,wt=7): 11445 ilf_type(f24(power_set(A)),binary_relation_type) | -empty(A). [resolve(972,a,206,a)]. given #703 (T,wt=9): 11446 ilf_type(f24(power_set(A)),binary_relation_type) | member(f24(A),A). [resolve(972,a,205,a)]. given #704 (T,wt=10): 11452 ilf_type(f24(power_set(c3)),binary_relation_type) | member(f24(c3),range_of(c4)). [resolve(11446,b,5583,a)]. given #705 (A,wt=21): 413 ilf_type(c3,binary_relation_type) | member(ordered_pair(f25(f17(c3)),f17(c3)),A) | -member(f11(c4,A),A) | member(f12(c4,A),A). [resolve(256,b,222,b)]. Low Water (keep, True_semantics): wt=59 given #706 (T,wt=8): 11511 ilf_type(f24(power_set(c3)),binary_relation_type) | -empty(range_of(c4)). [resolve(11452,b,206,a)]. given #707 (T,wt=11): 976 member(f17(f24(power_set(A))),A) | ilf_type(f24(power_set(A)),binary_relation_type). [resolve(467,a,119,a)]. given #708 (T,wt=11): 983 member(f24(f16(power_set(A))),A) | ilf_type(f16(power_set(A)),binary_relation_type). [resolve(490,a,264,a)]. given #709 (T,wt=7): 11620 ilf_type(f16(power_set(A)),binary_relation_type) | -empty(A). [resolve(983,a,206,a)]. given #710 (A,wt=16): 414 ilf_type(c3,binary_relation_type) | member(ordered_pair(f25(f17(c3)),f17(c3)),A) | member(f14(c4,A),c4). [resolve(256,b,218,a)]. given #711 (T,wt=9): 11621 ilf_type(f16(power_set(A)),binary_relation_type) | member(f24(A),A). [resolve(983,a,205,a)]. given #712 (T,wt=10): 11678 ilf_type(c3,binary_relation_type) | member(f14(c4,A),c4) | -empty(A). [resolve(414,b,206,a)]. given #713 (T,wt=10): 11707 ilf_type(f16(power_set(c3)),binary_relation_type) | member(f24(c3),range_of(c4)). [resolve(11621,b,5583,a)]. given #714 (T,wt=8): 11766 ilf_type(f16(power_set(c3)),binary_relation_type) | -empty(range_of(c4)). [resolve(11707,b,206,a)]. given #715 (A,wt=16): 415 ilf_type(c3,binary_relation_type) | member(ordered_pair(f25(f17(c3)),f17(c3)),A) | -member(f14(c4,A),A). [resolve(256,b,217,a)]. Low Water (keep, True_semantics): wt=52 given #716 (T,wt=11): 987 member(f17(f16(power_set(A))),A) | ilf_type(f16(power_set(A)),binary_relation_type). [resolve(490,a,119,a)]. given #717 (T,wt=11): 989 ilf_type(c3,binary_relation_type) | member(f17(c3),A) | range_of(c4) != A. [resolve(544,b,231,b)]. given #718 (T,wt=11): 1042 member(domain_of(f5(A,B)),C) | -member(power_set(B),power_set(C)). [resolve(1017,a,214,a)]. given #719 (T,wt=11): 1064 member(range_of(f5(A,B)),C) | -member(power_set(A),power_set(C)). [resolve(1049,a,214,a)]. given #720 (A,wt=15): 416 ilf_type(c3,binary_relation_type) | member(ordered_pair(f25(f17(c3)),f17(c3)),A) | -member(c4,power_set(A)). [resolve(256,b,214,a)]. given #721 (T,wt=11): 1092 empty(f6(A)) | member(f16(f6(A)),B) | A != B. [resolve(668,a,231,b)]. given #722 (T,wt=11): 1097 empty(f6(A)) | member(f16(f6(A)),B) | B != A. [resolve(668,a,226,b)]. given #723 (T,wt=11): 1106 empty(f6(A)) | empty(A) | ilf_type(f16(f6(A)),member_type(A)). [resolve(668,a,212,c)]. given #724 (T,wt=11): 1119 empty(f6(f16(power_set(A)))) | member(f24(f16(power_set(A))),A). [resolve(1110,b,490,a)]. given #725 (A,wt=14): 417 ilf_type(c3,binary_relation_type) | empty(c4) | ilf_type(ordered_pair(f25(f17(c3)),f17(c3)),member_type(c4)). [resolve(256,b,212,c)]. given #726 (T,wt=7): 11885 empty(f6(f16(power_set(A)))) | -empty(A). [resolve(1119,b,206,a)]. given #727 (T,wt=9): 11886 empty(f6(f16(power_set(A)))) | member(f24(A),A). [resolve(1119,b,205,a)]. given #728 (T,wt=10): 11892 empty(f6(f16(power_set(c3)))) | member(f24(c3),range_of(c4)). [resolve(11886,b,5583,a)]. given #729 (T,wt=8): 11951 empty(f6(f16(power_set(c3)))) | -empty(range_of(c4)). [resolve(11892,b,206,a)]. given #730 (A,wt=31): 418 ilf_type(c3,binary_relation_type) | ordered_pair(f20(c4,ordered_pair(f25(f17(c3)),f17(c3))),f21(c4,ordered_pair(f25(f17(c3)),f17(c3)))) = ordered_pair(f25(f17(c3)),f17(c3)) | member(f22(c4),c4). [resolve(256,b,209,a)]. Low Water (keep, True_semantics): wt=43 given #731 (T,wt=11): 1120 empty(f6(f24(power_set(A)))) | member(f24(f24(power_set(A))),A). [resolve(1110,b,467,a)]. given #732 (T,wt=7): 12021 empty(f6(f24(power_set(A)))) | -empty(A). [resolve(1120,b,206,a)]. given #733 (T,wt=9): 12022 empty(f6(f24(power_set(A)))) | member(f24(A),A). [resolve(1120,b,205,a)]. given #734 (T,wt=10): 12028 empty(f6(f24(power_set(c3)))) | member(f24(c3),range_of(c4)). [resolve(12022,b,5583,a)]. given #735 (A,wt=33): 419 ilf_type(c3,binary_relation_type) | ordered_pair(f20(c4,ordered_pair(f25(f17(c3)),f17(c3))),f21(c4,ordered_pair(f25(f17(c3)),f17(c3)))) = ordered_pair(f25(f17(c3)),f17(c3)) | f22(c4) != ordered_pair(A,B). [resolve(256,b,208,a)]. given #736 (T,wt=8): 12087 empty(f6(f24(power_set(c3)))) | -empty(range_of(c4)). [resolve(12028,b,206,a)]. given #737 (T,wt=11): 1123 empty(f6(f23(power_set(A)))) | member(f24(f23(power_set(A))),A). [resolve(1110,b,280,a)]. given #738 (T,wt=7): 12141 empty(f6(f23(power_set(A)))) | -empty(A). [resolve(1123,b,206,a)]. given #739 (T,wt=9): 12142 empty(f6(f23(power_set(A)))) | member(f24(A),A). [resolve(1123,b,205,a)]. given #740 (A,wt=13): 426 -ilf_type(power_set(ordered_pair(A,B)),binary_relation_type) | member(B,range_of(power_set(ordered_pair(A,B)))). [resolve(282,a,255,c)]. given #741 (T,wt=10): 12148 empty(f6(f23(power_set(c3)))) | member(f24(c3),range_of(c4)). [resolve(12142,b,5583,a)]. given #742 (T,wt=8): 12207 empty(f6(f23(power_set(c3)))) | -empty(range_of(c4)). [resolve(12148,b,206,a)]. given #743 (T,wt=11): 1137 empty(f6(A)) | member(f24(A),B) | -member(A,power_set(B)). [resolve(1110,b,214,a)]. Low Water (keep, True_semantics): wt=41 given #744 (T,wt=11): 1144 empty(f6(c3)) | member(ordered_pair(f25(f24(c3)),f24(c3)),c4). [resolve(1110,b,116,a)]. given #745 (A,wt=19): 427 -ilf_type(power_set(ordered_pair(A,B)),binary_relation_type) | member(ordered_pair(f2(power_set(ordered_pair(A,B)),B),B),power_set(ordered_pair(A,B))). [resolve(282,a,253,c)]. given #746 (T,wt=5): 12336 empty(f6(c3)) | -empty(c4). [resolve(1144,b,206,a)]. given #747 (T,wt=7): 12337 empty(f6(c3)) | member(f24(c4),c4). [resolve(1144,b,205,a)]. given #748 (T,wt=9): 12320 empty(f6(c3)) | member(f25(f24(c3)),domain_of(c4)). [resolve(1144,b,252,b),unit_del(b,540)]. given #749 (T,wt=6): 12379 empty(f6(c3)) | -empty(domain_of(c4)). [resolve(12320,b,206,a)]. gi