============================== FOF-Prover9 =========================== FOF-Prover9 (32) version November-2006, November 2006. Process 3784 was started by mccune on cleo.thornwood, Wed Nov 22 11:23:39 2006 The command was "/home/mccune/bin/fof-prover9 -f SET660+3.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file SET660+3.in 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)))))))). Child search process 3785 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: Relation symbol precedence: lex([ empty, ilf_type, member, subset, =, relation_like ]). Function symbol precedence: lex([ 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 (T,wt=4): 279 member(A,power_set(A)). [resolve(216,b,215,b),merge(b)]. given #75 (T,wt=5): 259 ilf_type(range_of(c4),subset_type(c3)). [back_rewrite(257),rewrite(258(4))]. given #76 (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 #77 (F,wt=4): 260 range_of(c4) != c3. [back_rewrite(117),rewrite(258(4))]. given #78 (F,wt=5): 263 ilf_type(domain_of(c4),subset_type(c2)). [back_rewrite(261),rewrite(262(4))]. given #79 (T,wt=5): 381 ilf_type(A,member_type(power_set(A))). [resolve(279,a,212,c),unit_del(a,213)]. given #80 (T,wt=4): 414 ilf_type(A,subset_type(A)). [resolve(381,a,238,b)]. given #81 (A,wt=7): 258 range(c2,c3,c4) = range_of(c4). [resolve(202,a,113,a)]. given #82 (F,wt=5): 404 ilf_type(c3,binary_relation_type) | -empty(c4). [resolve(256,b,206,a)]. given #83 (F,wt=5): 416 ilf_type(cross_product(A,B),binary_relation_type). [resolve(414,a,129,a)]. given #84 (T,wt=6): 265 empty(A) | member(f24(A),A). [resolve(207,b,205,a)]. given #85 (T,wt=6): 272 empty(A) | member(f16(A),A). [resolve(211,c,210,b),merge(c)]. given #86 (A,wt=7): 262 domain(c2,c3,c4) = domain_of(c4). [resolve(204,a,113,a)]. given #87 (F,wt=6): 284 member(A,power_set(B)) | -empty(A). [resolve(216,b,206,a)]. given #88 (F,wt=6): 332 ilf_type(f6(cross_product(A,B)),binary_relation_type). [resolve(236,a,129,a)]. given #89 (T,wt=6): 333 ilf_type(f6(A),member_type(power_set(A))). [resolve(237,b,236,a)]. given #90 (T,wt=5): 454 member(f6(A),power_set(A)). [resolve(333,a,211,c),unit_del(a,213)]. given #91 (A,wt=7): 264 member(f24(A),A) | ilf_type(A,binary_relation_type). [resolve(205,a,119,a)]. given #92 (F,wt=6): 334 ilf_type(f16(power_set(A)),subset_type(A)). [resolve(238,b,210,b),unit_del(b,213)]. given #93 (F,wt=6): 346 ilf_type(c4,subset_type(cross_product(c2,c3))). [resolve(244,a,113,a)]. given #94 (T,wt=3): 489 ilf_type(c4,binary_relation_type). [resolve(346,a,129,a)]. given #95 (T,wt=6): 383 member(f24(power_set(A)),power_set(A)). [resolve(279,a,205,a)]. given #96 (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 #97 (F,wt=6): 387 ilf_type(range_of(c4),member_type(power_set(c3))). [resolve(259,a,237,b)]. given #98 (F,wt=5): 514 member(range_of(c4),power_set(c3)). [resolve(387,a,211,c),unit_del(a,213)]. given #99 (T,wt=6): 413 ilf_type(domain_of(c4),member_type(power_set(c2))). [resolve(263,a,237,b)]. given #100 (T,wt=5): 531 member(domain_of(c4),power_set(c2)). [resolve(413,a,211,c),unit_del(a,213)]. given #101 (A,wt=18): 267 empty(A) | ordered_pair(f18(A,f23(A)),f19(A,f23(A))) = f23(A) | member(f17(A),A). [resolve(207,b,125,a)]. given #102 (F,wt=7): 273 empty(A) | ilf_type(f23(A),member_type(A)). [resolve(212,c,207,b),merge(c)]. given #103 (F,wt=6): 558 ilf_type(f23(power_set(A)),subset_type(A)). [resolve(273,b,238,b),unit_del(a,213)]. given #104 (T,wt=7): 336 subset(unordered_pair(A,B),unordered_pair(B,A)). [resolve(240,b,239,a)]. given #105 (T,wt=7): 342 ilf_type(domain_of(f5(A,B)),subset_type(B)). [resolve(243,a,203,a),rewrite(341(2))]. given #106 (A,wt=17): 268 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 #107 (F,wt=7): 344 ilf_type(range_of(f5(A,B)),subset_type(A)). [resolve(243,a,201,a),rewrite(343(2))]. given #108 (F,wt=7): 405 ilf_type(c3,binary_relation_type) | member(f24(c4),c4). [resolve(256,b,205,a)]. given #109 (T,wt=7): 415 ilf_type(cross_product(A,B),relation_type(A,B)). [resolve(414,a,245,a)]. given #110 (T,wt=7): 430 empty(A) | ilf_type(f24(A),member_type(A)). [resolve(265,b,212,c),merge(b)]. given #111 (A,wt=10): 269 empty(c3) | member(ordered_pair(f25(f23(c3)),f23(c3)),c4). [resolve(207,b,116,a)]. given #112 (F,wt=4): 608 empty(c3) | -empty(c4). [resolve(269,b,206,a)]. given #113 (F,wt=6): 591 ilf_type(f24(power_set(A)),subset_type(A)). [resolve(430,b,238,b),unit_del(a,213)]. given #114 (T,wt=6): 609 empty(c3) | member(f24(c4),c4). [resolve(269,b,205,a)]. given #115 (T,wt=7): 465 -member(A,f6(B)) | member(A,B). [resolve(454,a,214,c)]. given #116 (A,wt=18): 270 ordered_pair(f20(A,f23(A)),f21(A,f23(A))) = f23(A) | member(f22(A),A) | empty(A). [resolve(209,a,207,b)]. given #117 (F,wt=7): 486 ilf_type(f16(power_set(A)),member_type(power_set(A))). [resolve(334,a,237,b)]. given #118 (F,wt=6): 647 member(f16(power_set(A)),power_set(A)). [resolve(486,a,211,c),unit_del(a,213)]. given #119 (T,wt=7): 487 ilf_type(f16(power_set(cross_product(A,B))),binary_relation_type). [resolve(334,a,129,a)]. given #120 (T,wt=7): 488 ilf_type(c4,member_type(power_set(cross_product(c2,c3)))). [resolve(346,a,237,b)]. given #121 (A,wt=19): 271 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 #122 (F,wt=6): 663 member(c4,power_set(cross_product(c2,c3))). [resolve(488,a,211,c),unit_del(a,213)]. given #123 (F,wt=7): 505 ilf_type(f24(power_set(A)),member_type(power_set(A))). [resolve(383,a,212,c),unit_del(a,213)]. given #124 (T,wt=7): 525 -member(A,range_of(c4)) | member(A,c3). [resolve(514,a,214,c)]. given #125 (T,wt=7): 542 -member(A,domain_of(c4)) | member(A,c2). [resolve(531,a,214,c)]. given #126 (A,wt=10): 274 empty(A) | ilf_type(f17(A),member_type(A)) | ilf_type(A,binary_relation_type). [resolve(212,c,119,a)]. given #127 (F,wt=7): 561 ilf_type(f23(power_set(A)),member_type(power_set(A))). [resolve(558,a,237,b)]. given #128 (F,wt=6): 699 member(f23(power_set(A)),power_set(A)). [resolve(561,a,211,c),unit_del(a,213)]. given #129 (T,wt=7): 562 ilf_type(f23(power_set(cross_product(A,B))),binary_relation_type). [resolve(558,a,129,a)]. given #130 (T,wt=7): 588 ilf_type(domain_of(cross_product(A,B)),subset_type(A)). [resolve(415,a,203,a),rewrite(587(2))]. given #131 (A,wt=10): 275 member(f23(A),B) | -member(A,power_set(B)) | empty(A). [resolve(214,a,207,b)]. given #132 (F,wt=7): 590 ilf_type(range_of(cross_product(A,B)),subset_type(B)). [resolve(415,a,201,a),rewrite(589(2))]. given #133 (F,wt=7): 592 empty(c3) | member(f23(c3),range_of(c4)). [resolve(269,b,255,c),unit_del(b,489)]. given #134 (T,wt=5): 743 empty(c3) | -empty(range_of(c4)). [resolve(592,b,206,a)]. given #135 (T,wt=7): 615 ilf_type(f24(power_set(cross_product(A,B))),binary_relation_type). [resolve(591,a,129,a)]. given #136 (A,wt=11): 276 member(f17(A),B) | -member(A,power_set(B)) | ilf_type(A,binary_relation_type). [resolve(214,a,119,a)]. given #137 (F,wt=7): 669 member(f22(A),A) | ilf_type(A,binary_relation_type). [resolve(271,a,121,a(flip)),merge(c)]. given #138 (F,wt=8): 277 -member(A,f23(power_set(B))) | member(A,B). [resolve(214,c,207,b),unit_del(c,213)]. given #139 (T,wt=8): 285 member(A,power_set(B)) | member(f24(A),A). [resolve(216,b,205,a)]. given #140 (T,wt=8): 345 ilf_type(f5(A,B),subset_type(cross_product(B,A))). [resolve(244,a,243,a)]. given #141 (A,wt=12): 278 -member(A,f17(power_set(B))) | member(A,B) | ilf_type(power_set(B),binary_relation_type). [resolve(214,c,119,a)]. given #142 (F,wt=5): 841 ilf_type(f5(A,B),binary_relation_type). [resolve(345,a,129,a)]. given #143 (F,wt=8): 347 ilf_type(f6(cross_product(A,B)),relation_type(A,B)). [resolve(245,a,236,a)]. given #144 (T,wt=8): 380 member(A,B) | -member(power_set(A),power_set(B)). [resolve(279,a,214,a)]. given #145 (T,wt=8): 428 -member(A,f24(power_set(B))) | member(A,B). [resolve(265,b,214,c),unit_del(a,213)]. given #146 (A,wt=14): 280 member(power_set(A),power_set(B)) | -member(C,f15(power_set(A),B)) | member(C,A). [resolve(216,b,214,c)]. given #147 (F,wt=8): 447 -member(A,f16(power_set(B))) | member(A,B). [resolve(272,b,214,c),unit_del(a,213)]. given #148 (F,wt=8): 493 ilf_type(c3,binary_relation_type) | member(f17(c3),range_of(c4)). [back_unit_del(388),unit_del(b,489)]. given #149 (T,wt=6): 884 ilf_type(c3,binary_relation_type) | -empty(range_of(c4)). [resolve(493,b,206,a)]. given #150 (T,wt=8): 565 ilf_type(domain_of(f5(A,B)),member_type(power_set(B))). [resolve(342,a,237,b)]. given #151 (A,wt=13): 281 member(A,power_set(B)) | member(f15(A,B),C) | -member(A,power_set(C)). [resolve(216,b,214,a)]. given #152 (F,wt=7): 889 member(domain_of(f5(A,B)),power_set(B)). [resolve(565,a,211,c),unit_del(a,213)]. given #153 (F,wt=8): 566 ilf_type(domain_of(f5(A,cross_product(B,C))),binary_relation_type). [resolve(342,a,129,a)]. given #154 (T,wt=8): 570 ilf_type(range_of(f5(A,B)),member_type(power_set(A))). [resolve(344,a,237,b)]. given #155 (T,wt=7): 911 member(range_of(f5(A,B)),power_set(A)). [resolve(570,a,211,c),unit_del(a,213)]. given #156 (A,wt=12): 282 member(A,power_set(B)) | empty(A) | ilf_type(f15(A,B),member_type(A)). [resolve(216,b,212,c)]. given #157 (F,wt=8): 571 ilf_type(range_of(f5(cross_product(A,B),C)),binary_relation_type). [resolve(344,a,129,a)]. given #158 (F,wt=8): 594 empty(c3) | member(f25(f23(c3)),domain_of(c4)). [resolve(269,b,252,b),unit_del(b,489)]. given #159 (T,wt=5): 991 empty(c3) | -empty(domain_of(c4)). [resolve(594,b,206,a)]. given #160 (T,wt=7): 977 empty(c3) | member(f25(f23(c3)),c2). [resolve(594,b,542,a)]. given #161 (A,wt=23): 283 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 #162 (F,wt=4): 1009 empty(c3) | -empty(c2). [resolve(977,b,206,a)]. given #163 (F,wt=6): 1010 empty(c3) | member(f24(c2),c2). [resolve(977,b,205,a)]. given #164 (T,wt=8): 631 member(f16(f6(A)),A) | empty(f6(A)). [resolve(465,a,272,b)]. given #165 (T,wt=5): 1065 empty(f6(A)) | -empty(A). [resolve(631,a,206,a)]. given #166 (A,wt=25): 286 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 #167 (F,wt=7): 1066 empty(f6(A)) | member(f24(A),A). [resolve(631,a,205,a)]. given #168 (F,wt=8): 632 member(f24(f6(A)),A) | empty(f6(A)). [resolve(465,a,265,b)]. given #169 (T,wt=8): 635 member(f23(f6(A)),A) | empty(f6(A)). [resolve(465,a,207,b)]. given #170 (T,wt=8): 680 -member(A,c4) | member(A,cross_product(c2,c3)). [resolve(663,a,214,c)]. given #171 (A,wt=23): 287 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 #172 (F,wt=8): 686 member(f16(range_of(c4)),c3) | empty(range_of(c4)). [resolve(525,a,272,b)]. given #173 (F,wt=5): 1201 empty(range_of(c4)) | -empty(c3). [resolve(686,a,206,a)]. given #174 (T,wt=7): 1202 empty(range_of(c4)) | member(f24(c3),c3). [resolve(686,a,205,a)]. given #175 (T,wt=8): 687 member(f24(range_of(c4)),c3) | empty(range_of(c4)). [resolve(525,a,265,b)]. given #176 (A,wt=22): 288 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 #177 (F,wt=8): 690 member(f23(range_of(c4)),c3) | empty(range_of(c4)). [resolve(525,a,207,b)]. given #178 (F,wt=8): 692 member(f16(domain_of(c4)),c2) | empty(domain_of(c4)). [resolve(542,a,272,b)]. given #179 (T,wt=5): 1271 empty(domain_of(c4)) | -empty(c2). [resolve(692,a,206,a)]. given #180 (T,wt=7): 1272 empty(domain_of(c4)) | member(f24(c2),c2). [resolve(692,a,205,a)]. given #181 (A,wt=14): 289 member(c3,power_set(A)) | member(ordered_pair(f25(f15(c3,A)),f15(c3,A)),c4). [resolve(216,b,116,a)]. given #182 (F,wt=6): 1308 member(c3,power_set(A)) | -empty(c4). [resolve(289,b,206,a)]. given #183 (F,wt=8): 693 member(f24(domain_of(c4)),c2) | empty(domain_of(c4)). [resolve(542,a,265,b)]. given #184 (T,wt=8): 696 member(f23(domain_of(c4)),c2) | empty(domain_of(c4)). [resolve(542,a,207,b)]. given #185 (T,wt=8): 717 ilf_type(domain_of(cross_product(A,B)),member_type(power_set(A))). [resolve(588,a,237,b)]. given #186 (A,wt=15): 290 member(power_set(power_set(A)),power_set(A)) | -member(power_set(power_set(A)),f15(power_set(power_set(A)),A)). [factor(280,a,c)]. given #187 (F,wt=7): 1345 member(domain_of(cross_product(A,B)),power_set(A)). [resolve(717,a,211,c),unit_del(a,213)]. given #188 (F,wt=8): 718 ilf_type(domain_of(cross_product(cross_product(A,B),C)),binary_relation_type). [resolve(588,a,129,a)]. given #189 (T,wt=8): 720 member(f23(c4),cross_product(c2,c3)) | empty(c4). [resolve(275,b,663,a)]. given #190 (T,wt=6): 1378 empty(c4) | -empty(cross_product(c2,c3)). [resolve(720,a,206,a)]. given #191 (A,wt=14): 291 member(f15(A,B),C) | -member(f14(A,C),C) | member(A,power_set(B)). [resolve(217,a,216,b)]. given #192 (F,wt=8): 727 ilf_type(range_of(cross_product(A,B)),member_type(power_set(B))). [resolve(590,a,237,b)]. given #193 (F,wt=7): 1385 member(range_of(cross_product(A,B)),power_set(B)). [resolve(727,a,211,c),unit_del(a,213)]. given #194 (T,wt=8): 728 ilf_type(range_of(cross_product(A,cross_product(B,C))),binary_relation_type). [resolve(590,a,129,a)]. given #195 (T,wt=8): 744 empty(c3) | member(f24(range_of(c4)),range_of(c4)). [resolve(592,b,205,a)]. given #196 (A,wt=11): 292 member(f23(A),B) | -member(f14(A,B),B) | empty(A). [resolve(217,a,207,b)]. given #197 (F,wt=7): 1405 empty(c3) | member(f24(range_of(c4)),c3). [resolve(744,b,525,a)]. given #198 (F,wt=8): 849 ilf_type(domain_of(f6(cross_product(A,B))),subset_type(A)). [resolve(347,a,203,a),rewrite(848(3))]. given #199 (T,wt=8): 851 ilf_type(range_of(f6(cross_product(A,B))),subset_type(B)). [resolve(347,a,201,a),rewrite(850(3))]. given #200 (T,wt=8): 992 empty(c3) | member(f24(domain_of(c4)),domain_of(c4)). [resolve(594,b,205,a)]. given #201 (A,wt=12): 293 member(f17(A),B) | -member(f14(A,B),B) | ilf_type(A,binary_relation_type). [resolve(217,a,119,a)]. given #202 (F,wt=7): 1451 empty(c3) | member(f24(domain_of(c4)),c2). [resolve(992,b,542,a)]. given #203 (F,wt=8): 1171 member(f24(c4),cross_product(c2,c3)) | empty(c3). [resolve(680,a,609,b)]. given #204 (T,wt=6): 1498 empty(c3) | -empty(cross_product(c2,c3)). [resolve(1171,a,206,a)]. given #205 (T,wt=8): 1174 member(f16(c4),cross_product(c2,c3)) | empty(c4). [resolve(680,a,272,b)]. given #206 (A,wt=14): 294 member(f15(A,B),C) | member(f14(A,C),A) | member(A,power_set(B)). [resolve(218,a,216,b)]. given #207 (F,wt=8): 1176 member(f24(c4),cross_product(c2,c3)) | empty(c4). [resolve(680,a,265,b)]. given #208 (F,wt=8): 1309 member(c3,power_set(A)) | member(f24(c4),c4). [resolve(289,b,205,a)]. given #209 (T,wt=8): 1435 empty(c3) | ilf_type(f24(range_of(c4)),member_type(c3)). [resolve(1405,b,212,c),merge(b)]. given #210 (T,wt=8): 1649 member(f24(c4),c4) | -member(f24(c4),c3). [factor(1626,a,c)]. given #211 (A,wt=11): 295 member(f23(A),B) | member(f14(A,B),A) | empty(A). [resolve(218,a,207,b)]. given #212 (F,wt=9): 379 member(A,B) | -member(f14(power_set(A),B),B). [resolve(279,a,217,a)]. given #213 (F,wt=9): 466 member(f6(A),B) | -member(power_set(A),power_set(B)). [resolve(454,a,214,a)]. given #214 (T,wt=9): 485 ilf_type(f16(power_set(cross_product(A,B))),relation_type(A,B)). [resolve(334,a,245,a)]. given #215 (T,wt=9): 491 ilf_type(c3,binary_relation_type) | member(f25(f17(c3)),domain_of(c4)). [back_unit_del(390),unit_del(b,489)]. given #216 (A,wt=12): 296 member(f17(A),B) | member(f14(A,B),A) | ilf_type(A,binary_relation_type). [resolve(218,a,119,a)]. given #217 (F,wt=6): 1737 ilf_type(c3,binary_relation_type) | -empty(domain_of(c4)). [resolve(491,b,206,a)]. given #218 (F,wt=8): 1723 ilf_type(c3,binary_relation_type) | member(f25(f17(c3)),c2). [resolve(491,b,542,a)]. given #219 (T,wt=5): 1817 ilf_type(c3,binary_relation_type) | -empty(c2). [resolve(1723,b,206,a)]. given #220 (T,wt=7): 1818 ilf_type(c3,binary_relation_type) | member(f24(c2),c2). [resolve(1723,b,205,a)]. given #221 (A,wt=11): 297 member(f13(A,B),A) | -member(C,A) | member(C,B). [resolve(221,a,219,c)]. given #222 (F,wt=9): 526 member(range_of(c4),A) | -member(power_set(c3),power_set(A)). [resolve(514,a,214,a)]. given #223 (F,wt=9): 543 member(domain_of(c4),A) | -member(power_set(c2),power_set(A)). [resolve(531,a,214,a)]. given #224 (T,wt=9): 560 ilf_type(f23(power_set(cross_product(A,B))),relation_type(A,B)). [resolve(558,a,245,a)]. given #225 (T,wt=9): 614 ilf_type(f24(power_set(cross_product(A,B))),relation_type(A,B)). [resolve(591,a,245,a)]. given #226 (A,wt=19): 298 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 #227 (F,wt=9): 633 member(f24(f6(A)),A) | ilf_type(f6(A),binary_relation_type). [resolve(465,a,264,a)]. given #228 (F,wt=6): 1941 ilf_type(f6(A),binary_relation_type) | -empty(A). [resolve(633,a,206,a)]. given #229 (T,wt=8): 1942 ilf_type(f6(A),binary_relation_type) | member(f24(A),A). [resolve(633,a,205,a)]. given #230 (T,wt=9): 636 member(f17(f6(A)),A) | ilf_type(f6(A),binary_relation_type). [resolve(465,a,119,a)]. given #231 (A,wt=16): 299 member(f23(A),B) | -member(f11(A,B),B) | member(f12(A,B),B) | empty(A). [resolve(222,b,207,b)]. given #232 (F,wt=9): 688 member(f24(range_of(c4)),c3) | ilf_type(range_of(c4),binary_relation_type). [resolve(525,a,264,a)]. given #233 (F,wt=6): 2021 ilf_type(range_of(c4),binary_relation_type) | -empty(c3). [resolve(688,a,206,a)]. given #234 (T,wt=8): 2022 ilf_type(range_of(c4),binary_relation_type) | member(f24(c3),c3). [resolve(688,a,205,a)]. given #235 (T,wt=9): 691 member(f17(range_of(c4)),c3) | ilf_type(range_of(c4),binary_relation_type). [resolve(525,a,119,a)]. given #236 (A,wt=17): 300 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 #237 (F,wt=9): 694 member(f24(domain_of(c4)),c2) | ilf_type(domain_of(c4),binary_relation_type). [resolve(542,a,264,a)]. given #238 (F,wt=6): 2078 ilf_type(domain_of(c4),binary_relation_type) | -empty(c2). [resolve(694,a,206,a)]. given #239 (T,wt=8): 2079 ilf_type(domain_of(c4),binary_relation_type) | member(f24(c2),c2). [resolve(694,a,205,a)]. given #240 (T,wt=9): 697 member(f17(domain_of(c4)),c2) | ilf_type(domain_of(c4),binary_relation_type). [resolve(542,a,119,a)]. given #241 (A,wt=19): 301 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 #242 (F,wt=9): 753 ilf_type(domain_of(c4),binary_relation_type) | member(f22(domain_of(c4)),c2). [resolve(669,a,542,a)]. given #243 (F,wt=9): 754 ilf_type(range_of(c4),binary_relation_type) | member(f22(range_of(c4)),c3). [resolve(669,a,525,a)]. given #244 (T,wt=9): 755 ilf_type(f6(A),binary_relation_type) | member(f22(f6(A)),A). [resolve(669,a,465,a)]. given #245 (T,wt=9): 807 member(f24(A),A) | ilf_type(A,member_type(power_set(B))). [resolve(285,a,212,c),unit_del(b,213)]. given #246 (A,wt=16): 302 member(f23(A),B) | -member(f11(A,B),B) | -member(f12(A,B),A) | empty(A). [resolve(223,b,207,b)]. given #247 (F,wt=7): 2208 ilf_type(A,member_type(power_set(B))) | -empty(A). [resolve(807,a,206,a)]. given #248 (F,wt=9): 840 ilf_type(f5(A,B),member_type(power_set(cross_product(B,A)))). [resolve(345,a,237,b)]. given #249 (T,wt=8): 2215 member(f5(A,B),power_set(cross_product(B,A))). [resolve(840,a,211,c),unit_del(a,213)]. given #250 (T,wt=9): 885 ilf_type(c3,binary_relation_type) | member(f24(range_of(c4)),range_of(c4)). [resolve(493,b,205,a)]. given #251 (A,wt=17): 303 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 #252 (F,wt=8): 2235 ilf_type(c3,binary_relation_type) | member(f24(range_of(c4)),c3). [resolve(885,b,525,a)]. given #253 (F,wt=9): 905 -member(A,domain_of(f5(B,C))) | member(A,C). [resolve(889,a,214,c)]. given #254 (T,wt=9): 925 -member(A,range_of(f5(B,C))) | member(A,B). [resolve(911,a,214,c)]. given #255 (T,wt=9): 1082 empty(f6(domain_of(c4))) | member(f24(domain_of(c4)),c2). [resolve(1066,b,542,a)]. given #256 (A,wt=19): 304 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 #257 (F,wt=6): 2322 empty(f6(domain_of(c4))) | -empty(c2). [resolve(1082,b,206,a)]. given #258 (F,wt=8): 2323 empty(f6(domain_of(c4))) | member(f24(c2),c2). [resolve(1082,b,205,a)]. given #259 (T,wt=9): 1083 empty(f6(range_of(c4))) | member(f24(range_of(c4)),c3). [resolve(1066,b,525,a)]. given #260 (T,wt=6): 2459 empty(f6(range_of(c4))) | -empty(c3). [resolve(1083,b,206,a)]. given #261 (A,wt=16): 305 member(f23(A),B) | member(f11(A,B),A) | member(f12(A,B),B) | empty(A). [resolve(224,b,207,b)]. given #262 (F,wt=8): 2460 empty(f6(range_of(c4))) | member(f24(c3),c3). [resolve(1083,b,205,a)]. given #263 (F,wt=9): 1084 empty(f6(f6(A))) | member(f24(f6(A)),A). [resolve(1066,b,465,a)]. given #264 (T,wt=6): 2586 empty(f6(f6(A))) | -empty(A). [resolve(1084,b,206,a)]. given #265 (T,wt=8): 2587 empty(f6(f6(A))) | member(f24(A),A). [resolve(1084,b,205,a)]. given #266 (A,wt=17): 306 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 #267 (F,wt=9): 1167 member(f24(c4),cross_product(c2,c3)) | empty(f6(c4)). [resolve(680,a,1066,b)]. given #268 (F,wt=7): 2711 empty(f6(c4)) | -empty(cross_product(c2,c3)). [resolve(1167,a,206,a)]. given #269 (T,wt=9): 1172 member(f24(c4),cross_product(c2,c3)) | ilf_type(c3,binary_relation_type). [resolve(680,a,405,b)]. given #270 (T,wt=7): 2730 ilf_type(c3,binary_relation_type) | -empty(cross_product(c2,c3)). [resolve(1172,a,206,a)]. given #271 (A,wt=19): 307 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 #272 (F,wt=9): 1359 -member(A,domain_of(cross_product(B,C))) | member(A,B). [resolve(1345,a,214,c)]. given #273 (F,wt=9): 1399 -member(A,range_of(cross_product(B,C))) | member(A,C). [resolve(1385,a,214,c)]. given #274 (T,wt=9): 1444 ilf_type(domain_of(f6(cross_product(A,B))),member_type(power_set(A))). [resolve(849,a,237,b)]. given #275 (T,wt=8): 2793 member(domain_of(f6(cross_product(A,B))),power_set(A)). [resolve(1444,a,211,c),unit_del(a,213)]. given #276 (A,wt=16): 308 member(f23(A),B) | member(f11(A,B),A) | -member(f12(A,B),A) | empty(A). [resolve(225,b,207,b)]. given #277 (F,wt=9): 1445 ilf_type(domain_of(f6(cross_product(cross_product(A,B),C))),binary_relation_type). [resolve(849,a,129,a)]. given #278 (F,wt=9): 1449 ilf_type(range_of(f6(cross_product(A,B))),member_type(power_set(B))). [resolve(851,a,237,b)]. given #279 (T,wt=8): 2816 member(range_of(f6(cross_product(A,B))),power_set(B)). [resolve(1449,a,211,c),unit_del(a,213)]. given #280 (T,wt=9): 1450 ilf_type(range_of(f6(cross_product(A,cross_product(B,C)))),binary_relation_type). [resolve(851,a,129,a)]. given #281 (A,wt=17): 309 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 #282 (F,wt=9): 1542 member(f14(A,B),A) | member(A,power_set(B)). [resolve(294,a,215,b),merge(c)]. given #283 (F,wt=9): 1628 member(f24(c4),c4) | ilf_type(c3,member_type(power_set(A))). [resolve(1309,a,212,c),unit_del(b,213)]. given #284 (T,wt=7): 2890 ilf_type(c3,member_type(power_set(A))) | -empty(c4). [resolve(1628,a,206,a)]. given #285 (T,wt=9): 1677 member(f14(A,B),A) | empty(A) | -empty(B). [resolve(295,a,206,a)]. given #286 (A,wt=19): 310 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 #287 (F,wt=9): 1720 ilf_type(domain_of(f16(power_set(cross_product(A,B)))),subset_type(A)). [resolve(485,a,203,a),rewrite(1719(4))]. given #288 (F,wt=9): 1722 ilf_type(range_of(f16(power_set(cross_product(A,B)))),subset_type(B)). [resolve(485,a,201,a),rewrite(1721(4))]. given #289 (T,wt=9): 1738 ilf_type(c3,binary_relation_type) | member(f24(domain_of(c4)),domain_of(c4)). [resolve(491,b,205,a)]. given #290 (T,wt=8): 2906 ilf_type(c3,binary_relation_type) | member(f24(domain_of(c4)),c2). [resolve(1738,b,542,a)]. given #291 (A,wt=16): 311 member(f23(A),B) | -member(f9(B,A),A) | member(f10(B,A),A) | empty(A). [resolve(227,b,207,b)]. given #292 (F,wt=9): 1904 ilf_type(domain_of(f23(power_set(cross_product(A,B)))),subset_type(A)). [resolve(560,a,203,a),rewrite(1903(4))]. given #293 (F,wt=9): 1906 ilf_type(range_of(f23(power_set(cross_product(A,B)))),subset_type(B)). [resolve(560,a,201,a),rewrite(1905(4))]. given #294 (T,wt=9): 1908 ilf_type(domain_of(f24(power_set(cross_product(A,B)))),subset_type(A)). [resolve(614,a,203,a),rewrite(1907(4))]. given #295 (T,wt=9): 1910 ilf_type(range_of(f24(power_set(cross_product(A,B)))),subset_type(B)). [resolve(614,a,201,a),rewrite(1909(4))]. given #296 (A,wt=17): 312 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 #297 (F,wt=10): 335 member(A,unordered_pair(B,C)) | -member(A,unordered_pair(C,B)). [resolve(239,a,231,c)]. given #298 (F,wt=10): 350 unordered_pair(unordered_pair(A,B),singleton(A)) = ordered_pair(A,B). [xx_res(246,b)]. given #299 (T,wt=10): 378 member(A,B) | member(f14(power_set(A),B),power_set(A)). [resolve(279,a,218,a)]. given #300 (T,wt=9): 3020 member(A,A) | -member(A,f14(power_set(A),A)). [factor(3013,a,c)]. given #301 (A,wt=19): 313 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 #302 (F,wt=10): 429 empty(A) | member(f24(A),B) | -member(A,power_set(B)). [resolve(265,b,214,a)]. given #303 (F,wt=10): 435 empty(c3) | member(ordered_pair(f25(f24(c3)),f24(c3)),c4). [resolve(265,b,116,a)]. given #304 (T,wt=7): 3057 empty(c3) | member(f24(c3),range_of(c4)). [resolve(435,b,255,c),unit_del(b,489)]. given #305 (T,wt=8): 3059 empty(c3) | member(f25(f24(c3)),domain_of(c4)). [resolve(435,b,252,b),unit_del(b,489)]. given #306 (A,wt=16): 314 member(f23(A),B) | -member(f9(B,A),A) | -member(f10(B,A),B) | empty(A). [resolve(228,b,207,b)]. given #307 (F,wt=7): 3094 empty(c3) | member(f25(f24(c3)),c2). [resolve(3059,b,542,a)]. given #308 (F,wt=10): 448 empty(A) | member(f16(A),B) | -member(A,power_set(B)). [resolve(272,b,214,a)]. given #309 (T,wt=10): 453 empty(c3) | member(ordered_pair(f25(f16(c3)),f16(c3)),c4). [resolve(272,b,116,a)]. given #310 (T,wt=7): 3159 empty(c3) | member(f16(c3),range_of(c4)). [resolve(453,b,255,c),unit_del(b,489)]. given #311 (A,wt=17): 315 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 #312 (F,wt=8): 3161 empty(c3) | member(f25(f16(c3)),domain_of(c4)). [resolve(453,b,252,b),unit_del(b,489)]. given #313 (F,wt=7): 3198 empty(c3) | member(f25(f16(c3)),c2). [resolve(3161,b,542,a)]. given #314 (T,wt=10): 464 member(f6(A),B) | -member(f14(power_set(A),B),B). [resolve(454,a,217,a)]. given #315 (T,wt=10): 504 member(f24(power_set(A)),B) | -member(power_set(A),power_set(B)). [resolve(383,a,214,a)]. given #316 (A,wt=19): 316 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 #317 (F,wt=10): 524 member(range_of(c4),A) | -member(f14(power_set(c3),A),A). [resolve(514,a,217,a)]. given #318 (F,wt=10): 541 member(domain_of(c4),A) | -member(f14(power_set(c2),A),A). [resolve(531,a,217,a)]. given #319 (T,wt=10): 564 ilf_type(domain_of(f5(A,cross_product(B,C))),relation_type(B,C)). [resolve(342,a,245,a)]. given #320 (T,wt=10): 569 ilf_type(range_of(f5(cross_product(A,B),C)),relation_type(A,B)). [resolve(344,a,245,a)]. given #321 (A,wt=16): 317 member(f23(A),B) | member(f9(B,A),B) | member(f10(B,A),A) | empty(A). [resolve(229,b,207,b)]. given #322 (F,wt=10): 626 empty(c3) | member(f24(c4),A) | -member(c4,power_set(A)). [resolve(609,b,214,a)]. given #323 (F,wt=10): 658 member(f16(power_set(A)),B) | -member(power_set(A),power_set(B)). [resolve(647,a,214,a)]. given #324 (T,wt=10): 681 member(c4,A) | -member(power_set(cross_product(c2,c3)),power_set(A)). [resolve(663,a,214,a)]. given #325 (T,wt=10): 698 ilf_type(power_set(A),binary_relation_type) | ilf_type(f17(power_set(A)),subset_type(A)). [resolve(274,b,238,b),unit_del(a,213)]. given #326 (A,wt=17): 318 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 #327 (F,wt=10): 710 member(f23(power_set(A)),B) | -member(power_set(A),power_set(B)). [resolve(699,a,214,a)]. given #328 (F,wt=10): 716 ilf_type(domain_of(cross_product(cross_product(A,B),C)),relation_type(A,B)). [resolve(588,a,245,a)]. given #329 (T,wt=10): 719 member(f23(f23(power_set(A))),A) | empty(f23(power_set(A))). [resolve(275,b,699,a)]. given #330 (T,wt=6): 3559 empty(f23(power_set(A))) | -empty(A). [resolve(719,a,206,a)]. given #331 (A,wt=19): 319 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 #332 (F,wt=8): 3560 empty(f23(power_set(A))) | member(f24(A),A). [resolve(719,a,205,a)]. given #333 (F,wt=10): 721 member(f23(f16(power_set(A))),A) | empty(f16(power_set(A))). [resolve(275,b,647,a)]. given #334 (T,wt=6): 3634 empty(f16(power_set(A))) | -empty(A). [resolve(721,a,206,a)]. given #335 (T,wt=8): 3635 empty(f16(power_set(A))) | member(f24(A),A). [resolve(721,a,205,a)]. given #336 (A,wt=16): 320 member(f23(A),B) | member(f9(B,A),B) | -member(f10(B,A),B) | empty(A). [resolve(230,b,207,b)]. given #337 (F,wt=10): 722 member(f23(f24(power_set(A))),A) | empty(f24(power_set(A))). [resolve(275,b,383,a)]. given #338 (F,wt=6): 3709 empty(f24(power_set(A))) | -empty(A). [resolve(722,a,206,a)]. given #339 (T,wt=8): 3710 empty(f24(power_set(A))) | member(f24(A),A). [resolve(722,a,205,a)]. given #340 (T,wt=10): 726 ilf_type(range_of(cross_product(A,cross_product(B,C))),relation_type(B,C)). [resolve(590,a,245,a)]. given #341 (A,wt=17): 321 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 #342 (F,wt=10): 771 ilf_type(A,binary_relation_type) | empty(A) | ilf_type(f22(A),member_type(A)). [resolve(669,a,212,c)]. given #343 (F,wt=10): 774 member(f16(f23(power_set(A))),A) | empty(f23(power_set(A))). [resolve(277,a,272,b)]. given #344 (T,wt=10): 775 member(f24(f23(power_set(A))),A) | empty(f23(power_set(A))). [resolve(277,a,265,b)]. given #345 (T,wt=10): 816 member(domain_of(c4),power_set(A)) | member(f24(domain_of(c4)),c2). [resolve(285,b,542,a)]. given #346 (A,wt=16): 322 member(f7(A,B),A) | member(f8(A,B),B) | member(C,A) | -member(C,B). [resolve(234,a,231,c)]. given #347 (F,wt=7): 3863 member(domain_of(c4),power_set(A)) | -empty(c2). [resolve(816,b,206,a)]. given #348 (F,wt=9): 3864 member(domain_of(c4),power_set(A)) | member(f24(c2),c2). [resolve(816,b,205,a)]. given #349 (T,wt=10): 817 member(range_of(c4),power_set(A)) | member(f24(range_of(c4)),c3). [resolve(285,b,525,a)]. given #350 (T,wt=7): 4070 member(range_of(c4),power_set(A)) | -empty(c3). [resolve(817,b,206,a)]. given #351 (A,wt=16): 323 member(f7(A,B),A) | member(f8(A,B),B) | member(C,B) | -member(C,A). [resolve(234,a,226,c)]. given #352 (F,wt=9): 4071 member(range_of(c4),power_set(A)) | member(f24(c3),c3). [resolve(817,b,205,a)]. given #353 (F,wt=10): 818 member(f6(A),power_set(B)) | member(f24(f6(A)),A). [resolve(285,b,465,a)]. given #354 (T,wt=7): 4309 member(f6(A),power_set(B)) | -empty(A). [resolve(818,b,206,a)]. given #355 (T,wt=9): 4310 member(f6(A),power_set(B)) | member(f24(A),A). [resolve(818,b,205,a)]. given #356 (A,wt=31): 324 member(f7(ordered_pair(A,B),f22(C)),ordered_pair(A,B)) | member(f8(ordered_pair(A,B),f22(C)),f22(C)) | -member(D,C) | ordered_pair(f20(C,D),f21(C,D)) = D. [resolve(234,a,208,c)]. given #357 (F,wt=10): 854 member(f16(f24(power_set(A))),A) | empty(f24(power_set(A))). [resolve(428,a,272,b)]. given #358 (F,wt=10): 855 member(f24(f24(power_set(A))),A) | empty(f24(power_set(A))). [resolve(428,a,265,b)]. given #359 (T,wt=10): 866 member(f16(f16(power_set(A))),A) | empty(f16(power_set(A))). [resolve(447,a,272,b)]. given #360 (T,wt=10): 867 member(f24(f16(power_set(A))),A) | empty(f16(power_set(A))). [resolve(447,a,265,b)]. given #361 (A,wt=31): 325 member(f7(ordered_pair(A,B),f17(C)),ordered_pair(A,B)) | member(f8(ordered_pair(A,B),f17(C)),f17(C)) | -member(D,C) | ordered_pair(f18(C,D),f19(C,D)) = D. [resolve(234,a,127,c)]. given #362 (F,wt=10): 1007 empty(c3) | empty(c2) | ilf_type(f25(f23(c3)),member_type(c2)). [resolve(977,b,212,c)]. given #363 (F,wt=10): 1034 empty(c3) | member(f24(c2),A) | -member(c2,power_set(A)). [resolve(1010,b,214,a)]. given #364 (T,wt=10): 1039 empty(f6(domain_of(c4))) | member(f16(f6(domain_of(c4))),c2). [resolve(631,a,542,a)]. given #365 (T,wt=10): 1040 empty(f6(range_of(c4))) | member(f16(f6(range_of(c4))),c3). [resolve(631,a,525,a)]. given #366 (A,wt=22): 326 member(f7(ordered_pair(A,B),f17(C)),ordered_pair(A,B)) | member(f8(ordered_pair(A,B),f17(C)),f17(C)) | ilf_type(C,binary_relation_type). [resolve(234,a,121,a)]. given #367 (F,wt=10): 1041 empty(f6(f6(A))) | member(f16(f6(f6(A))),A). [resolve(631,a,465,a)]. given #368 (F,wt=10): 1107 empty(f6(domain_of(c4))) | member(f24(f6(domain_of(c4))),c2). [resolve(632,a,542,a)]. given #369 (T,wt=10): 1108 empty(f6(range_of(c4))) | member(f24(f6(range_of(c4))),c3). [resolve(632,a,525,a)]. given #370 (T,wt=10): 1109 empty(f6(f6(A))) | member(f24(f6(f6(A))),A). [resolve(632,a,465,a)]. given #371 (A,wt=31): 327 member(f7(f22(A),ordered_pair(B,C)),f22(A)) | member(f8(f22(A),ordered_pair(B,C)),ordered_pair(B,C)) | -member(D,A) | ordered_pair(f20(A,D),f21(A,D)) = D. [resolve(234,a,208,c(flip))]. given #372 (F,wt=10): 1137 empty(f6(domain_of(c4))) | member(f23(f6(domain_of(c4))),c2). [resolve(635,a,542,a)]. given #373 (F,wt=10): 1138 empty(f6(range_of(c4))) | member(f23(f6(range_of(c4))),c3). [resolve(635,a,525,a)]. given #374 (T,wt=10): 1139 empty(f6(f6(A))) | member(f23(f6(f6(A))),A). [resolve(635,a,465,a)]. given #375 (T,wt=10): 1168 member(f23(f6(c4)),cross_product(c2,c3)) | empty(f6(c4)). [resolve(680,a,635,a)]. given #376 (A,wt=31): 328 member(f7(f17(A),ordered_pair(B,C)),f17(A)) | member(f8(f17(A),ordered_pair(B,C)),ordered_pair(B,C)) | -member(D,A) | ordered_pair(f18(A,D),f19(A,D)) = D. [resolve(234,a,127,c(flip))]. given #377 (F,wt=10): 1169 member(f24(f6(c4)),cross_product(c2,c3)) | empty(f6(c4)). [resolve(680,a,632,a)]. given #378 (F,wt=10): 1170 member(f16(f6(c4)),cross_product(c2,c3)) | empty(f6(c4)). [resolve(680,a,631,a)]. given #379 (T,wt=10): 1173 member(f24(c4),cross_product(c2,c3)) | member(c4,power_set(A)). [resolve(680,a,285,b)]. given #380 (T,wt=8): 5438 member(c4,power_set(A)) | -empty(cross_product(c2,c3)). [resolve(1173,a,206,a)]. given #381 (A,wt=22): 329 member(f7(f17(A),ordered_pair(B,C)),f17(A)) | member(f8(f17(A),ordered_pair(B,C)),ordered_pair(B,C)) | ilf_type(A,binary_relation_type). [resolve(234,a,121,a(flip))]. given #382 (F,wt=10): 1292 member(c3,power_set(A)) | member(f15(c3,A),range_of(c4)). [resolve(289,b,255,c),unit_del(b,489)]. given #383 (F,wt=5): 5517 member(c3,power_set(range_of(c4))). [resolve(1292,b,215,b),merge(b)]. given #384 (T,wt=6): 5545 ilf_type(c3,member_type(power_set(range_of(c4)))). [resolve(5517,a,212,c),unit_del(a,213)]. given #385 (T,wt=5): 5550 ilf_type(c3,subset_type(range_of(c4))). [resolve(5545,a,238,b)]. given #386 (A,wt=15): 330 member(f7(A,B),A) | member(f8(A,B),B) | -member(f7(A,B),B). [factor(322,a,c)]. given #387 (F,wt=7): 5521 member(c3,power_set(A)) | -empty(range_of(c4)). [resolve(1292,b,206,a)]. given #388 (F,wt=7): 5543 -member(A,c3) | member(A,range_of(c4)). [resolve(5517,a,214,c)]. given #389 (T,wt=8): 5561 member(f24(c3),range_of(c4)) | empty(range_of(c4)). [resolve(5543,a,1202,b)]. given #390 (T,wt=8): 5565 member(f24(c3),range_of(c4)) | empty(f6(c3)). [resolve(5543,a,1066,b)]. given #391 (A,wt=15): 331 member(f7(A,B),A) | member(f8(A,B),B) | -member(f8(A,B),A). [factor(323,b,c)]. given #392 (F,wt=6): 5649 empty(f6(c3)) | -empty(range_of(c4)). [resolve(5565,a,206,a)]. given #393 (F,wt=8): 5579 member(f22(c3),range_of(c4)) | ilf_type(c3,binary_relation_type). [resolve(5543,a,669,a)]. given #394 (T,wt=8): 5604 member(f24(c3),range_of(c4)) | ilf_type(c3,binary_relation_type). [resolve(5543,a,264,a)]. given #395 (T,wt=9): 5544 member(c3,A) | -member(power_set(range_of(c4)),power_set(A)). [resolve(5517,a,214,a)]. given #396 (A,wt=13): 337 subset(A,B) | member(f7(B,A),B) | member(f8(B,A),A). [resolve(240,b,234,a)]. given #397 (F,wt=9): 5553 member(f24(c3),range_of(c4)) | empty(f24(power_set(c3))). [resolve(5543,a,3710,b)]. given #398 (F,wt=7): 5723 empty(f24(power_set(c3))) | -empty(range_of(c4)). [resolve(5553,a,206,a)]. given #399 (T,wt=9): 5554 member(f24(c3),range_of(c4)) | empty(f16(power_set(c3))). [resolve(5543,a,3635,b)]. given #400 (T,wt=7): 5748 empty(f16(power_set(c3))) | -empty(range_of(c4)). [resolve(5554,a,206,a)]. given #401 (A,wt=13): 338 subset(A,B) | member(f7(A,B),A) | member(f8(A,B),B). [resolve(240,b,234,a(flip))]. given #402 (F,wt=9): 5555 member(f24(c3),range_of(c4)) | empty(f23(power_set(c3))). [resolve(5543,a,3560,b)]. given #403 (F,wt=7): 5774 empty(f23(power_set(c3))) | -empty(range_of(c4)). [resolve(5555,a,206,a)]. given #404 (T,wt=9): 5556 member(f24(c3),range_of(c4)) | empty(f6(f6(c3))). [resolve(5543,a,2587,b)]. given #405 (T,wt=7): 5799 empty(f6(f6(c3))) | -empty(range_of(c4)). [resolve(5556,a,206,a)]. given #406 (A,wt=11): 339 A = B | -subset(A,B) | member(f13(B,A),B). [resolve(242,b,221,a)]. given #407 (F,wt=9): 5557 member(f24(c3),range_of(c4)) | empty(f6(range_of(c4))). [resolve(5543,a,2460,b)]. given #408 (F,wt=9): 5558 member(f24(c3),range_of(c4)) | ilf_type(range_of(c4),binary_relation_type). [resolve(5543,a,2022,b)]. given #409 (T,wt=9): 5559 member(f24(c3),range_of(c4)) | ilf_type(f6(c3),binary_relation_type). [resolve(5543,a,1942,b)]. given #410 (T,wt=7): 5866 ilf_type(f6(c3),binary_relation_type) | -empty(range_of(c4)). [resolve(5559,a,206,a)]. given #411 (A,wt=11): 340 A = B | -subset(B,A) | member(f13(A,B),A). [resolve(242,c,221,a)]. given #412 (F,wt=9): 5581 member(f23(f6(c3)),range_of(c4)) | empty(f6(c3)). [resolve(5543,a,635,a)]. given #413 (F,wt=9): 5583 member(f24(f6(c3)),range_of(c4)) | empty(f6(c3)). [resolve(5543,a,632,a)]. given #414 (T,wt=9): 5584 member(f16(f6(c3)),range_of(c4)) | empty(f6(c3)). [resolve(5543,a,631,a)]. given #415 (T,wt=9): 5603 member(f24(c3),range_of(c4)) | member(c3,power_set(A)). [resolve(5543,a,285,b)]. given #416 (A,wt=11): 341 domain(A,B,f5(B,A)) = domain_of(f5(B,A)). [resolve(243,a,204,a)]. given #417 (F,wt=9): 5624 empty(range_of(c4)) | ilf_type(f24(c3),member_type(range_of(c4))). [resolve(5561,a,212,c),merge(b)]. given #418 (F,wt=9): 5650 empty(f6(c3)) | member(f24(range_of(c4)),range_of(c4)). [resolve(5565,a,205,a)]. given #419 (T,wt=8): 5990 empty(f6(c3)) | member(f24(range_of(c4)),c3). [resolve(5650,b,525,a)]. given #420 (T,wt=10): 1379 empty(c4) | member(f24(cross_product(c2,c3)),cross_product(c2,c3)). [resolve(720,a,205,a)]. given #421 (A,wt=11): 343 range(A,B,f5(B,A)) = range_of(f5(B,A)). [resolve(243,a,202,a)]. given #422 (F,wt=10): 1480 empty(c3) | empty(c2) | ilf_type(f24(domain_of(c4)),member_type(c2)). [resolve(1451,b,212,c)]. given #423 (F,wt=10): 1499 empty(c3) | member(f24(cross_product(c2,c3)),cross_product(c2,c3)). [resolve(1171,a,205,a)]. given #424 (T,wt=10): 1626 member(f24(c4),c4) | -member(A,c3) | member(A,B). [resolve(1309,a,214,c)]. given #425 (T,wt=10): 1633 member(c3,power_set(A)) | member(f24(c4),cross_product(c2,c3)). [resolve(1309,b,680,a)]. given #426 (A,wt=21): 351 ordered_pair(A,B) = C | member(f7(ordered_pair(A,B),C),ordered_pair(A,B)) | member(f8(ordered_pair(A,B),C),C). [back_rewrite(349),rewrite(350(3))]. given #427 (F,wt=8): 6179 member(c3,power_set(A)) | -empty(cross_product(c2,c3)). [resolve(1633,b,206,a)]. given #428 (F,wt=10): 1769 member(f14(A,B),A) | ilf_type(A,binary_relation_type) | -empty(B). [resolve(296,a,206,a)]. given #429 (T,wt=10): 1891 member(f13(power_set(A),B),power_set(A)) | member(A,B). [resolve(297,b,279,a)]. given #430 (T,wt=9): 6232 member(A,A) | -member(A,f13(power_set(A),A)). [factor(6225,a,c)]. given #431 (A,wt=13): 352 member(f3(A,B),A) | member(f4(A,B),B) | subset(A,B). [resolve(250,c,241,b)]. given #432 (F,wt=10): 1947 ilf_type(f6(c4),binary_relation_type) | member(f24(c4),cross_product(c2,c3)). [resolve(1942,b,680,a)]. given #433 (F,wt=8): 6264 ilf_type(f6(c4),binary_relation_type) | -empty(cross_product(c2,c3)). [resolve(1947,b,206,a)]. given #434 (T,wt=10): 1948 ilf_type(f6(domain_of(c4)),binary_relation_type) | member(f24(domain_of(c4)),c2). [resolve(1942,b,542,a)]. given #435 (T,wt=7): 6289 ilf_type(f6(domain_of(c4)),binary_relation_type) | -empty(c2). [resolve(1948,b,206,a)]. given #436 (A,wt=13): 353 member(f3(A,B),A) | member(f4(A,B),B) | subset(B,A). [resolve(250,c,240,b)]. given #437 (F,wt=9): 6290 ilf_type(f6(domain_of(c4)),binary_relation_type) | member(f24(c2),c2). [resolve(1948,b,205,a)]. given #438 (F,wt=10): 1949 ilf_type(f6(range_of(c4)),binary_relation_type) | member(f24(range_of(c4)),c3). [resolve(1942,b,525,a)]. given #439 (T,wt=7): 6338 ilf_type(f6(range_of(c4)),binary_relation_type) | -empty(c3). [resolve(1949,b,206,a)]. given #440 (T,wt=9): 6339 ilf_type(f6(range_of(c4)),binary_relation_type) | member(f24(c3),c3). [resolve(1949,b,205,a)]. given #441 (A,wt=16): 354 member(f3(A,B),A) | member(f4(A,B),B) | member(C,A) | -member(C,B). [resolve(250,c,231,c)]. given #442 (F,wt=10): 1950 ilf_type(f6(f6(A)),binary_relation_type) | member(f24(f6(A)),A). [resolve(1942,b,465,a)]. given #443 (F,wt=7): 6607 ilf_type(f6(f6(A)),binary_relation_type) | -empty(A). [resolve(1950,b,206,a)]. given #444 (T,wt=9): 6608 ilf_type(f6(f6(A)),binary_relation_type) | member(f24(A),A). [resolve(1950,b,205,a)]. given #445 (T,wt=10): 2229 -member(A,f5(B,C)) | member(A,cross_product(C,B)). [resolve(2215,a,214,c)]. given #446 (A,wt=16): 355 member(f3(A,B),A) | member(f4(A,B),B) | member(C,B) | -member(C,A). [resolve(250,c,226,c)]. given #447 (F,wt=10): 2594 empty(f6(f6(c4))) | member(f24(c4),cross_product(c2,c3)). [resolve(2587,b,680,a)]. given #448 (F,wt=8): 6920 empty(f6(f6(c4))) | -empty(cross_product(c2,c3)). [resolve(2594,b,206,a)]. given #449 (T,wt=10): 2595 empty(f6(f6(domain_of(c4)))) | member(f24(domain_of(c4)),c2). [resolve(2587,b,542,a)]. given #450 (T,wt=7): 6947 empty(f6(f6(domain_of(c4)))) | -empty(c2). [resolve(2595,b,206,a)]. given #451 (A,wt=31): 356 member(f3(ordered_pair(A,B),f22(C)),ordered_pair(A,B)) | member(f4(ordered_pair(A,B),f22(C)),f22(C)) | -member(D,C) | ordered_pair(f20(C,D),f21(C,D)) = D. [resolve(250,c,208,c)]. given #452 (F,wt=9): 6948 empty(f6(f6(domain_of(c4)))) | member(f24(c2),c2). [resolve(2595,b,205,a)]. given #453 (F,wt=10): 2596 empty(f6(f6(range_of(c4)))) | member(f24(range_of(c4)),c3). [resolve(2587,b,525,a)]. given #454 (T,wt=7): 7188 empty(f6(f6(range_of(c4)))) | -empty(c3). [resolve(2596,b,206,a)]. given #455 (T,wt=9): 7189 empty(f6(f6(range_of(c4)))) | member(f24(c3),c3). [resolve(2596,b,205,a)]. given #456 (A,wt=31): 357 member(f3(ordered_pair(A,B),f17(C)),ordered_pair(A,B)) | member(f4(ordered_pair(A,B),f17(C)),f17(C)) | -member(D,C) | ordered_pair(f18(C,D),f19(C,D)) = D. [resolve(250,c,127,c)]. given #457 (F,wt=10): 2597 empty(f6(f6(f6(A)))) | member(f24(f6(A)),A). [resolve(2587,b,465,a)]. given #458 (F,wt=7): 7430 empty(f6(f6(f6(A)))) | -empty(A). [resolve(2597,b,206,a)]. given #459 (T,wt=9): 7431 empty(f6(f6(f6(A)))) | member(f24(A),A). [resolve(2597,b,205,a)]. given #460 (T,wt=10): 2808 -member(A,domain_of(f6(cross_product(B,C)))) | member(A,B). [resolve(2793,a,214,c)]. given #461 (A,wt=22): 358 member(f3(ordered_pair(A,B),f17(C)),ordered_pair(A,B)) | member(f4(ordered_pair(A,B),f17(C)),f17(C)) | ilf_type(C,binary_relation_type). [resolve(250,c,121,a)]. given #462 (F,wt=10): 2831 -member(A,range_of(f6(cross_product(B,C)))) | member(A,C). [resolve(2816,a,214,c)]. given #463 (F,wt=10): 2899 ilf_type(domain_of(f16(power_set(cross_product(A,B)))),member_type(power_set(A))). [resolve(1720,a,237,b)]. given #464 (T,wt=9): 7624 member(domain_of(f16(power_set(cross_product(A,B)))),power_set(A)). [resolve(2899,a,211,c),unit_del(a,213)]. given #465 (T,wt=10): 2900 ilf_type(domain_of(f16(power_set(cross_product(cross_product(A,B),C)))),binary_relation_type). [resolve(1720,a,129,a)]. given #466 (A,wt=31): 359 member(f3(f22(A),ordered_pair(B,C)),f22(A)) | member(f4(f22(A),ordered_pair(B,C)),ordered_pair(B,C)) | -member(D,A) | ordered_pair(f20(A,D),f21(A,D)) = D. [resolve(250,c,208,c(flip))]. given #467 (F,wt=10): 2904 ilf_type(range_of(f16(power_set(cross_product(A,B)))),member_type(power_set(B))). [resolve(1722,a,237,b)]. given #468 (F,wt=9): 7852 member(range_of(f16(power_set(cross_product(A,B)))),power_set(B)). [resolve(2904,a,211,c),unit_del(a,213)]. given #469 (T,wt=10): 2905 ilf_type(range_of(f16(power_set(cross_product(A,cross_product(B,C))))),binary_relation_type). [resolve(1722,a,129,a)]. given #470 (T,wt=10): 2945 ilf_type(domain_of(f23(power_set(cross_product(A,B)))),member_type(power_set(A))). [resolve(1904,a,237,b)]. given #471 (A,wt=31): 360 member(f3(f17(A),ordered_pair(B,C)),f17(A)) | member(f4(f17(A),ordered_pair(B,C)),ordered_pair(B,C)) | -member(D,A) | ordered_pair(f18(A,D),f19(A,D)) = D. [resolve(250,c,127,c(flip))]. given #472 (F,wt=9): 7886 member(domain_of(f23(power_set(cross_product(A,B)))),power_set(A)). [resolve(2945,a,211,c),unit_del(a,213)]. given #473 (F,wt=10): 2946 ilf_type(domain_of(f23(power_set(cross_product(cross_product(A,B),C)))),binary_relation_type). [resolve(1904,a,129,a)]. given #474 (T,wt=10): 2950 ilf_type(range_of(f23(power_set(cross_product(A,B)))),member_type(power_set(B))). [resolve(1906,a,237,b)]. given #475 (T,wt=9): 8086 member(range_of(f23(power_set(cross_product(A,B)))),power_set(B)). [resolve(2950,a,211,c),unit_del(a,213)]. given #476 (A,wt=22): 361 member(f3(f17(A),ordered_pair(B,C)),f17(A)) | member(f4(f17(A),ordered_pair(B,C)),ordered_pair(B,C)) | ilf_type(A,binary_relation_type). [resolve(250,c,121,a(flip))]. given #477 (F,wt=10): 2951 ilf_type(range_of(f23(power_set(cross_product(A,cross_product(B,C))))),binary_relation_type). [resolve(1906,a,129,a)]. given #478 (F,wt=10): 2955 ilf_type(domain_of(f24(power_set(cross_product(A,B)))),member_type(power_set(A))). [resolve(1908,a,237,b)]. given #479 (T,wt=9): 8161 member(domain_of(f24(power_set(cross_product(A,B)))),power_set(A)). [resolve(2955,a,211,c),unit_del(a,213)]. given #480 (T,wt=10): 2956 ilf_type(domain_of(f24(power_set(cross_product(cross_product(A,B),C)))),binary_relation_type). [resolve(1908,a,129,a)]. given #481 (A,wt=15): 362 member(f3(A,B),A) | member(f4(A,B),B) | -member(f3(A,B),B). [factor(354,a,c)]. given #482 (F,wt=10): 2960 ilf_type(range_of(f24(power_set(cross_product(A,B)))),member_type(power_set(B))). [resolve(1910,a,237,b)]. given #483 (F,wt=9): 8196 member(range_of(f24(power_set(cross_product(A,B)))),power_set(B)). [resolve(2960,a,211,c),unit_del(a,213)]. given #484 (T,wt=10): 2961 ilf_type(range_of(f24(power_set(cross_product(A,cross_product(B,C))))),binary_relation_type). [resolve(1910,a,129,a)]. given #485 (T,wt=10): 2996 unordered_pair(singleton(A),unordered_pair(A,B)) = ordered_pair(A,B). [para(350(a,1),239(a,1)),flip(a)]. given #486 (A,wt=15): 363 member(f3(A,B),A) | member(f4(A,B),B) | -member(f4(A,B),A). [factor(355,b,c)]. given #487 (F,wt=10): 2997 unordered_pair(unordered_pair(A,B),singleton(B)) = ordered_pair(B,A). [para(239(a,1),350(a,1,1))]. given #488 (F,wt=10): 3126 empty(c3) | empty(c2) | ilf_type(f25(f24(c3)),member_type(c2)). [resolve(3094,b,212,c)]. given #489 (T,wt=10): 3228 empty(c3) | empty(c2) | ilf_type(f25(f16(c3)),member_type(c2)). [resolve(3198,b,212,c)]. given #490 (T,wt=10): 3341 ilf_type(domain_of(domain_of(f5(A,cross_product(B,C)))),subset_type(B)). [resolve(564,a,203,a),rewrite(3340(4))]. given #491 (A,wt=21): 364 -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 #492 (F,wt=10): 3343 ilf_type(range_of(domain_of(f5(A,cross_product(B,C)))),subset_type(C)). [resolve(564,a,201,a),rewrite(3342(4))]. given #493 (F,wt=10): 3345 ilf_type(domain_of(range_of(f5(cross_product(A,B),C))),subset_type(A)). [resolve(569,a,203,a),rewrite(3344(4))]. given #494 (T,wt=10): 3347 ilf_type(range_of(range_of(f5(cross_product(A,B),C))),subset_type(B)). [resolve(569,a,201,a),rewrite(3346(4))]. given #495 (T,wt=10): 3521 ilf_type(domain_of(domain_of(cross_product(cross_product(A,B),C))),subset_type(A)). [resolve(716,a,203,a),rewrite(3520(4))]. given #496 (A,wt=17): 365 -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 #497 (F,wt=10): 3523 ilf_type(range_of(domain_of(cross_product(cross_product(A,B),C))),subset_type(B)). [resolve(716,a,201,a),rewrite(3522(4))]. given #498 (F,wt=10): 3571 empty(f23(power_set(c4))) | member(f24(c4),cross_product(c2,c3)). [resolve(3560,b,680,a)]. given #499 (T,wt=8): 8331 empty(f23(power_set(c4))) | -empty(cross_product(c2,c3)). [resolve(3571,b,206,a)]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 45 (0.00 of 1.04 sec). given #500 (T,wt=10): 3572 empty(f23(power_set(domain_of(c4)))) | member(f24(domain_of(c4)),c2). [resolve(3560,b,542,a)]. given #501 (A,wt=18): 366 -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 #502 (F,wt=7): 8362 empty(f23(power_set(domain_of(c4)))) | -empty(c2). [resolve(3572,b,206,a)]. given #503 (F,wt=9): 8363 empty(f23(power_set(domain_of(c4)))) | member(f24(c2),c2). [resolve(3572,b,205,a)]. given #504 (T,wt=10): 3573 empty(f23(power_set(range_of(c4)))) | member(f24(range_of(c4)),c3). [resolve(3560,b,525,a)]. given #505 (T,wt=7): 8441 empty(f23(power_set(range_of(c4)))) | -empty(c3). [resolve(3573,b,206,a)]. given #506 (A,wt=13): 367 -ilf_type(power_set(ordered_pair(A,B)),binary_relation_type) | member(B,range_of(power_set(ordered_pair(A,B)))). [resolve(279,a,255,c)]. given #507 (F,wt=9): 8442 empty(f23(power_set(range_of(c4)))) | member(f24(c3),c3). [resolve(3573,b,205,a)]. given #508 (F,wt=10): 3574 empty(f23(power_set(f6(A)))) | member(f24(f6(A)),A). [resolve(3560,b,465,a)]. given #509 (T,wt=7): 8535 empty(f23(power_set(f6(A)))) | -empty(A). [resolve(3574,b,206,a)]. given #510 (T,wt=9): 8536 empty(f23(power_set(f6(A)))) | member(f24(A),A). [resolve(3574,b,205,a)]. given #511 (A,wt=19): 368 -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(279,a,253,c)]. given #512 (F,wt=10): 3644 empty(f16(power_set(c4))) | member(f24(c4),cross_product(c2,c3)). [resolve(3635,b,680,a)]. given #513 (F,wt=8): 8621 empty(f16(power_set(c4))) | -empty(cross_product(c2,c3)). [resolve(3644,b,206,a)]. given #514 (T,wt=10): 3645 empty(f16(power_set(domain_of(c4)))) | member(f24(domain_of(c4)),c2). [resolve(3635,b,542,a)]. given #515 (T,wt=7): 8652 empty(f16(power_set(domain_of(c4)))) | -empty(c2). [resolve(3645,b,206,a)]. given #516 (A,wt=13): 369 -ilf_type(power_set(ordered_pair(A,B)),binary_relation_type) | member(A,domain_of(power_set(ordered_pair(A,B)))). [resolve(279,a,252,b)]. given #517 (F,wt=9): 8653 empty(f16(power_set(domain_of(c4)))) | member(f24(c2),c2). [resolve(3645,b,205,a)]. given #518 (F,wt=10): 3646 empty(f16(power_set(range_of(c4)))) | member(f24(range_of(c4)),c3). [resolve(3635,b,525,a)]. given #519 (T,wt=7): 8716 empty(f16(power_set(range_of(c4)))) | -empty(c3). [resolve(3646,b,206,a)]. given #520 (T,wt=9): 8717 empty(f16(power_set(range_of(c4)))) | member(f24(c3),c3). [resolve(3646,b,205,a)]. given #521 (A,wt=15): 370 member(A,B) | member(f9(B,power_set(A)),B) | -member(f10(B,power_set(A)),B). [resolve(279,a,230,b)]. given #522 (F,wt=10): 3647 empty(f16(power_set(f6(A)))) | member(f24(f6(A)),A). [resolve(3635,b,465,a)]. given #523 (F,wt=7): 8807 empty(f16(power_set(f6(A)))) | -empty(A). [resolve(3647,b,206,a)]. given #524 (T,wt=9): 8808 empty(f16(power_set(f6(A)))) | member(f24(A),A). [resolve(3647,b,205,a)]. given #525 (T,wt=10): 3719 empty(f24(power_set(c4))) | member(f24(c4),cross_product(c2,c3)). [resolve(3710,b,680,a)]. given #526 (A,wt=16): 371 member(A,B) | member(f9(B,power_set(A)),B) | member(f10(B,power_set(A)),power_set(A)). [resolve(279,a,229,b)]. given #527 (F,wt=8): 8888 empty(f24(power_set(c4))) | -empty(cross_product(c2,c3)). [resolve(3719,b,206,a)]. given #528 (F,wt=10): 3720 empty(f24(power_set(domain_of(c4)))) | member(f24(domain_of(c4)),c2). [resolve(3710,b,542,a)]. given #529 (T,wt=7): 8956 empty(f24(power_set(domain_of(c4)))) | -empty(c2). [resolve(3720,b,206,a)]. given #530 (T,wt=9): 8957 empty(f24(power_set(domain_of(c4)))) | member(f24(c2),c2). [resolve(3720,b,205,a)]. given #531 (A,wt=16): 372 member(A,B) | -member(f9(B,power_set(A)),power_set(A)) | -member(f10(B,power_set(A)),B). [resolve(279,a,228,b)]. given #532 (F,wt=10): 3721 empty(f24(power_set(range_of(c4)))) | member(f24(range_of(c4)),c3). [resolve(3710,b,525,a)]. given #533 (F,wt=7): 9017 empty(f24(power_set(range_of(c4)))) | -empty(c3). [resolve(3721,b,206,a)]. given #534 (T,wt=9): 9018 empty(f24(power_set(range_of(c4)))) | member(f24(c3),c3). [resolve(3721,b,205,a)]. given #535 (T,wt=10): 3722 empty(f24(power_set(f6(A)))) | member(f24(f6(A)),A). [resolve(3710,b,465,a)]. given #536 (A,wt=17): 373 member(A,B) | -member(f9(B,power_set(A)),power_set(A)) | member(f10(B,power_set(A)),power_set(A)). [resolve(279,a,227,b)]. given #537 (F,wt=7): 9106 empty(f24(power_set(f6(A)))) | -empty(A). [resolve(3722,b,206,a)]. given #538 (F,wt=9): 9107 empty(f24(power_set(f6(A)))) | member(f24(A),A). [resolve(3722,b,205,a)]. given #539 (T,wt=10): 3748 ilf_type(domain_of(range_of(cross_product(A,cross_product(B,C)))),subset_type(B)). [resolve(726,a,203,a),rewrite(3747(4))]. given #540 (T,wt=10): 3750 ilf_type(range_of(range_of(cross_product(A,cross_product(B,C)))),subset_type(C)). [resolve(726,a,201,a),rewrite(3749(4))]. given #541 (A,wt=17): 374 member(A,B) | member(f11(power_set(A),B),power_set(A)) | -member(f12(power_set(A),B),power_set(A)). [resolve(279,a,225,b)]. given #542 (F,wt=10): 3753 ilf_type(power_set(A),binary_relation_type) | ilf_type(f22(power_set(A)),subset_type(A)). [resolve(771,c,238,b),unit_del(b,213)]. given #543 (F,wt=10): 4016 member(f24(c2),c2) | ilf_type(domain_of(c4),member_type(power_set(A))). [resolve(3864,a,212,c),unit_del(b,213)]. given #544 (T,wt=8): 9205 ilf_type(domain_of(c4),member_type(power_set(A))) | -empty(c2). [resolve(4016,a,206,a)]. given #545 (T,wt=10): 4229 member(f24(c3),c3) | ilf_type(range_of(c4),member_type(power_set(A))). [resolve(4071,a,212,c),unit_del(b,213)]. given #546 (A,wt=16): 375 member(A,B) | member(f11(power_set(A),B),power_set(A)) | member(f12(power_set(A),B),B). [resolve(279,a,224,b)]. given #547 (F,wt=8): 9236 ilf_type(range_of(c4),member_type(power_set(A))) | -empty(c3). [resolve(4229,a,206,a)]. given #548 (F,wt=10): 4331 member(f24(A),A) | ilf_type(f6(A),member_type(power_set(B))). [resolve(4310,a,212,c),unit_del(b,213)]. given #549 (T,wt=8): 9366 ilf_type(f6(A),member_type(power_set(B))) | -empty(A). [resolve(4331,a,206,a)]. given #550 (T,wt=10): 5522 member(c3,power_set(A)) | member(f24(range_of(c4)),range_of(c4)). [resolve(1292,b,205,a)]. given #551 (A,wt=16): 376 member(A,B) | -member(f11(power_set(A),B),B) | -member(f12(power_set(A),B),power_set(A)). [resolve(279,a,223,b)]. given #552 (F,wt=9): 9401 member(c3,power_set(A)) | member(f24(range_of(c4)),c3). [resolve(5522,b,525,a)]. given #553 (F,wt=10): 5542 member(c3,A) | -member(f14(power_set(range_of(c4)),A),A). [resolve(5517,a,217,a)]. given #554 (T,wt=10): 5551 member(f24(c3),range_of(c4)) | member(f6(c3),power_set(A)). [resolve(5543,a,4310,b)]. given #555 (T,wt=8): 9520 member(f6(c3),power_set(A)) | -empty(range_of(c4)). [resolve(5551,a,206,a)]. given #556 (A,wt=15): 377 member(A,B) | -member(f11(power_set(A),B),B) | member(f12(power_set(A),B),B). [resolve(279,a,222,b)]. given #557 (F,wt=10): 5552 member(f24(c3),range_of(c4)) | member(range_of(c4),power_set(A)). [resolve(5543,a,4071,b)]. given #558 (F,wt=10): 5560 member(f14(c3,A),range_of(c4)) | member(c3,power_set(A)). [resolve(5543,a,1542,a)]. given #559 (T,wt=10): 5564 member(f24(f6(c3)),range_of(c4)) | empty(f6(f6(c3))). [resolve(5543,a,1084,b)]. given #560 (T,wt=10): 5572 member(f24(c3),range_of(c4)) | ilf_type(c3,member_type(power_set(A))). [resolve(5543,a,807,a)]. given #561 (A,wt=17): 382 ordered_pair(f20(power_set(A),A),f21(power_set(A),A)) = A | member(f22(power_set(A)),power_set(A)). [resolve(279,a,209,a)]. given #562 (F,wt=8): 9701 ilf_type(c3,member_type(power_set(A))) | -empty(range_of(c4)). [resolve(5572,a,206,a)]. given #563 (F,wt=10): 5575 member(f22(f6(c3)),range_of(c4)) | ilf_type(f6(c3),binary_relation_type). [resolve(5543,a,755,b)]. given #564 (T,wt=10): 5580 member(f17(f6(c3)),range_of(c4)) | ilf_type(f6(c3),binary_relation_type). [resolve(5543,a,636,a)]. given #565 (T,wt=10): 5582 member(f24(f6(c3)),range_of(c4)) | ilf_type(f6(c3),binary_relation_type). [resolve(5543,a,633,a)]. given #566 (A,wt=18): 384 -ilf_type(power_set(A),subset_type(cross_product(B,C))) | ordered_pair(f18(power_set(A),A),f19(power_set(A),A)) = A. [resolve(279,a,131,b)]. given #567 (F,wt=10): 5724 empty(f24(power_set(c3))) | member(f24(range_of(c4)),range_of(c4)). [resolve(5553,a,205,a)]. given #568 (F,wt=9): 9819 empty(f24(power_set(c3))) | member(f24(range_of(c4)),c3). [resolve(5724,b,525,a)]. given #569 (T,wt=10): 5749 empty(f16(power_set(c3))) | member(f24(range_of(c4)),range_of(c4)). [resolve(5554,a,205,a)]. given #570 (T,wt=9): 9879 empty(f16(power_set(c3))) | member(f24(range_of(c4)),c3). [resolve(5749,b,525,a)]. given #571 (A,wt=17): 385 ordered_pair(f18(power_set(A),A),f19(power_set(A),A)) = A | member(f17(power_set(A)),power_set(A)). [resolve(279,a,125,a)]. given #572 (F,wt=10): 5775 empty(f23(power_set(c3))) | member(f24(range_of(c4)),range_of(c4)). [resolve(5555,a,205,a)]. given #573 (F,wt=9): 9963 empty(f23(power_set(c3))) | member(f24(range_of(c4)),c3). [resolve(5775,b,525,a)]. given #574 (T,wt=10): 5800 empty(f6(f6(c3))) | member(f24(range_of(c4)),range_of(c4)). [resolve(5556,a,205,a)]. given #575 (T,wt=9): 10023 empty(f6(f6(c3))) | member(f24(range_of(c4)),c3). [resolve(5800,b,525,a)]. given #576 (A,wt=15): 386 ordered_pair(f18(power_set(A),A),f19(power_set(A),A)) = A | -ilf_type(power_set(A),binary_relation_type). [resolve(279,a,123,a)]. given #577 (F,wt=10): 5867 ilf_type(f6(c3),binary_relation_type) | member(f24(range_of(c4)),range_of(c4)). [resolve(5559,a,205,a)]. given #578 (F,wt=9): 10083 ilf_type(f6(c3),binary_relation_type) | member(f24(range_of(c4)),c3). [resolve(5867,b,525,a)]. given #579 (T,wt=10): 6184 member(f24(c4),cross_product(c2,c3)) | -member(f24(c4),c3). [factor(6153,a,c)]. given #580 (T,wt=10): 6344 ilf_type(f6(range_of(c4)),binary_relation_type) | member(f24(c3),range_of(c4)). [resolve(6339,b,5543,a)]. given #581 (A,wt=21): 391 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 #582 (F,wt=10): 6613 ilf_type(f6(f6(c3)),binary_relation_type) | member(f24(c3),range_of(c4)). [resolve(6608,b,5543,a)]. given #583 (F,wt=8): 10200 ilf_type(f6(f6(c3)),binary_relation_type) | -empty(range_of(c4)). [resolve(6613,b,206,a)]. given #584 (T,wt=10): 7194 empty(f6(f6(range_of(c4)))) | member(f24(c3),range_of(c4)). [resolve(7189,b,5543,a)]. given #585 (T,wt=10): 7436 empty(f6(f6(f6(c3)))) | member(f24(c3),range_of(c4)). [resolve(7431,b,5543,a)]. given #586 (A,wt=21): 392 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 #587 (F,wt=8): 10260 empty(f6(f6(f6(c3)))) | -empty(range_of(c4)). [resolve(7436,b,206,a)]. given #588 (F,wt=10): 8231 unordered_pair(singleton(A),unordered_pair(B,A)) = ordered_pair(A,B). [para(239(a,1),2996(a,1,2))]. given #589 (T,wt=10): 8452 empty(f23(power_set(range_of(c4)))) | member(f24(c3),range_of(c4)). [resolve(8442,b,5543,a)]. given #590 (T,wt=10): 8541 empty(f23(power_set(f6(c3)))) | member(f24(c3),range_of(c4)). [resolve(8536,b,5543,a)]. given #591 (A,wt=21): 393 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 #592 (F,wt=8): 10414 empty(f23(power_set(f6(c3)))) | -empty(range_of(c4)). [resolve(8541,b,206,a)]. given #593 (F,wt=10): 8722 empty(f16(power_set(range_of(c4)))) | member(f24(c3),range_of(c4)). [resolve(8717,b,5543,a)]. given #594 (T,wt=10): 8813 empty(f16(power_set(f6(c3)))) | member(f24(c3),range_of(c4)). [resolve(8808,b,5543,a)]. given #595 (T,wt=8): 10476 empty(f16(power_set(f6(c3)))) | -empty(range_of(c4)). [resolve(8813,b,206,a)]. given #596 (A,wt=21): 394 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 #597 (F,wt=10): 9023 empty(f24(power_set(range_of(c4)))) | member(f24(c3),range_of(c4)). [resolve(9018,b,5543,a)]. given #598 (F,wt=10): 9114 empty(f24(power_set(f6(c3)))) | member(f24(c3),range_of(c4)). [resolve(9107,b,5543,a)]. given #599 (T,wt=8): 10536 empty(f24(power_set(f6(c3)))) | -empty(range_of(c4)). [resolve(9114,b,206,a)]. given #600 (T,wt=10): 9458 member(f24(range_of(c4)),c3) | ilf_type(c3,member_type(power_set(A))). [resolve(9401,a,212,c),unit_del(b,213)]. given #601 (A,wt=21): 395 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 #602 (F,wt=10): 9554 member(f24(c3),range_of(c4)) | -member(f24(c3),f6(c3)). [factor(9548,a,c)]. given #603 (F,wt=11): 426 empty(A) | member(f24(A),B) | member(f14(A,B),A). [resolve(265,b,218,a)]. given #604 (T,wt=11): 427 empty(A) | member(f24(A),B) | -member(f14(A,B),B). [resolve(265,b,217,a)]. given #605 (T,wt=11): 445 empty(A) | member(f16(A),B) | member(f14(A,B),A). [resolve(272,b,218,a)]. given #606 (A,wt=21): 396 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)]. given #607 (F,wt=11): 446 empty(A) | member(f16(A),B) | -member(f14(A,B),B). [resolve(272,b,217,a)]. given #608 (F,wt=11): 463 member(f6(A),B) | member(f14(power_set(A),B),power_set(A)). [resolve(454,a,218,a)]. given #609 (T,wt=9): 10979 member(f14(power_set(A),B),power_set(A)) | -empty(B). [resolve(463,a,206,a)]. given #610 (T,wt=11): 482 ilf_type(A,binary_relation_type) | member(f24(A),B) | -member(A,power_set(B)). [resolve(264,a,214,a)]. given #611 (A,wt=21): 397 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 #612 (F,wt=11): 484 ilf_type(c3,binary_relation_type) | member(ordered_pair(f25(f24(c3)),f24(c3)),c4). [resolve(264,a,116,a)]. given #613 (F,wt=9): 11101 ilf_type(c3,binary_relation_type) | member(f25(f24(c3)),domain_of(c4)). [resolve(484,b,252,b),unit_del(b,489)]. given #614 (T,wt=8): 11119 ilf_type(c3,binary_relation_type) | member(f25(f24(c3)),c2). [resolve(11101,b,542,a)]. given #615 (T,wt=11): 503 member(f24(power_set(A)),B) | -member(f14(power_set(A),B),B). [resolve(383,a,217,a)]. given #616 (A,wt=21): 398 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)]. given #617 (F,wt=11): 523 member(range_of(c4),A) | member(f14(power_set(c3),A),power_set(c3)). [resolve(514,a,218,a)]. given #618 (F,wt=11): 540 member(domain_of(c4),A) | member(f14(power_set(c2),A),power_set(c2)). [resolve(531,a,218,a)]. given #619 (T,wt=11): 582 ilf_type(c3,binary_relation_type) | member(f24(c4),A) | -member(c4,power_set(A)). [resolve(405,b,214,a)]. given #620 (T,wt=11): 587 domain(A,B,cross_product(A,B)) = domain_of(cross_product(A,B)). [resolve(415,a,204,a)]. given #621 (A,wt=16): 399 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)]. Low Water (keep): wt=51, part=0.98, limit=48 given #622 (F,wt=10): 11424 ilf_type(c3,binary_relation_type) | member(f14(c4,A),c4) | -empty(A). [resolve(399,b,206,a)]. given #623 (F,wt=11): 589 range(A,B,cross_product(A,B)) = range_of(cross_product(A,B)). [resolve(415,a,202,a)]. given #624 (T,wt=11): 593 empty(c3) | member(ordered_pair(f2(c4,f23(c3)),f23(c3)),c4). [resolve(269,b,253,c),unit_del(b,489)]. Low Water (keep): wt=48, part=0.97, limit=46 given #625 (T,wt=9): 11468 empty(c3) | member(f2(c4,f23(c3)),domain_of(c4)). [resolve(593,b,252,b),unit_del(b,489)]. given #626 (A,wt=16): 400 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)]. given #627 (F,wt=8): 11486 empty(c3) | member(f2(c4,f23(c3)),c2). [resolve(11468,b,542,a)]. given #628 (F,wt=11): 624 empty(c3) | member(f24(c4),A) | member(f14(c4,A),c4). [resolve(609,b,218,a)]. given #629 (T,wt=9): 11600 empty(c3) | member(f14(c4,A),c4) | -empty(A). [resolve(624,b,206,a)]. given #630 (T,wt=11): 625 empty(c3) | member(f24(c4),A) | -member(f14(c4,A),A). [resolve(609,b,217,a)]. given #631 (A,wt=15): 401 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 #632 (F,wt=11): 634 member(f15(f6(A),B),A) | member(f6(A),power_set(B)). [resolve(465,a,216,b)]. given #633 (F,wt=11): 657 member(f16(power_set(A)),B) | -member(f14(power_set(A),B),B). [resolve(647,a,217,a)]. given #634 (T,wt=11): 679 member(c4,A) | -member(f14(power_set(cross_product(c2,c3)),A),A). [resolve(663,a,217,a)]. given #635 (T,wt=11): 689 member(f15(range_of(c4),A),c3) | member(range_of(c4),power_set(A)). [resolve(525,a,216,b)]. given #636 (A,wt=14): 402 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 #637 (F,wt=11): 695 member(f15(domain_of(c4),A),c2) | member(domain_of(c4),power_set(A)). [resolve(542,a,216,b)]. given #638 (F,wt=11): 709 member(f23(power_set(A)),B) | -member(f14(power_set(A),B),B). [resolve(699,a,217,a)]. given #639 (T,wt=11): 729 empty(c3) | member(ordered_pair(f1(c4,f23(c3)),f23(c3)),c4). [resolve(592,b,254,c),unit_del(b,489)]. given #640 (T,wt=9): 11771 empty(c3) | member(f1(c4,f23(c3)),domain_of(c4)). [resolve(729,b,252,b),unit_del(b,489)]. Low Water (keep): wt=44, part=0.96, limit=44 given #641 (A,wt=31): 403 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)]. given #642 (F,wt=8): 11789 empty(c3) | member(f1(c4,f23(c3)),c2). [resolve(11771,b,542,a)]. given #643 (F,wt=11): 740 empty(c3) | member(f23(c3),A) | -member(range_of(c4),power_set(A)). [resolve(592,b,214,a)]. given #644 (T,wt=11): 741 empty(c3) | empty(range_of(c4)) | ilf_type(f23(c3),member_type(range_of(c4))). [resolve(592,b,212,c)]. given #645 (T,wt=11): 748 member(f17(f23(power_set(A))),A) | ilf_type(f23(power_set(A)),binary_relation_type). [resolve(276,b,699,a)]. given #646 (A,wt=13): 409 member(f3(c3,range_of(c4)),c3) | member(f4(c3,range_of(c4)),range_of(c4)). [resolve(260,a,250,c)]. given #647 (F,wt=7): 11902 ilf_type(f23(power_set(A)),binary_relation_type) | -empty(A). [resolve(748,a,206,a)]. given #648 (F,wt=9): 11903 ilf_type(f23(power_set(A)),binary_relation_type) | member(f24(A),A). [resolve(748,a,205,a)]. given #649 (T,wt=9): 11928 member(f3(c3,range_of(c4)),c3) | -empty(range_of(c4)). [resolve(409,b,206,a)]. given #650 (T,wt=10): 11933 ilf_type(f23(power_set(c3)),binary_relation_type) | member(f24(c3),range_of(c4)). [resolve(11903,b,5543,a)]. given #651 (A,wt=13): 410 member(f7(c3,range_of(c4)),c3) | member(f8(c3,range_of(c4)),range_of(c4)). [resolve(260,a,234,a)]. given #652 (F,wt=8): 12008 ilf_type(f23(power_set(c3)),binary_relation_type) | -empty(range_of(c4)). [resolve(11933,b,206,a)]. given #653 (F,wt=9): 12033 member(f7(c3,range_of(c4)),c3) | -empty(range_of(c4)). [resolve(410,b,206,a)]. given #654 (T,wt=11): 749 member(f17(f16(power_set(A))),A) | ilf_type(f16(power_set(A)),binary_relation_type). [resolve(276,b,647,a)]. given #655 (T,wt=7): 12091 ilf_type(f16(power_set(A)),binary_relation_type) | -empty(A). [resolve(749,a,206,a)]. given #656 (A,wt=13): 411 member(f3(range_of(c4),c3),range_of(c4)) | member(f4(range_of(c4),c3),c3). [resolve(260,a,250,c(flip))]. given #657 (F,wt=9): 12092 ilf_type(f16(power_set(A)),binary_relation_type) | member(f24(A),A). [resolve(749,a,205,a)]. given #658 (F,wt=9): 12117 member(f3(range_of(c4),c3),range_of(c4)) | -empty(c3). [resolve(411,b,206,a)]. given #659 (T,wt=10): 12123 ilf_type(f16(power_set(c3)),binary_relation_type) | member(f24(c3),range_of(c4)). [resolve(12092,b,5543,a)]. given #660 (T,wt=8): 12198 ilf_type(f16(power_set(c3)),binary_relation_type) | -empty(range_of(c4)). [resolve(12123,b,206,a)]. given #661 (A,wt=13): 412 member(f7(range_of(c4),c3),range_of(c4)) | member(f8(range_of(c4),c3),c3). [resolve(260,a,234,a(flip))]. given #662 (F,wt=9): 12223 member(f7(range_of(c4),c3),range_of(c4)) | -empty(c3). [resolve(412,b,206,a)]. given #663 (F,wt=11): 750 member(f17(f24(power_set(A))),A) | ilf_type(f24(power_set(A)),binary_relation_type). [resolve(276,b,383,a)]. Low Water (keep): wt=42, part=0.94, limit=42 given #664 (T,wt=7): 12274 ilf_type(f24(power_set(A)),binary_relation_type) | -empty(A). [resolve(750,a,206,a)]. given #665 (T,wt=9): 12275 ilf_type(f24(power_set(A)),binary_relation_type) | member(f24(A),A). [resolve(750,a,205,a)]. given #666 (A,wt=17): 417 empty(range_of(A)) | -ilf_type(A,binary_relation_type) | member(ordered_pair(f1(A,f24(range_of(A))),f24(range_of(A))),A). [resolve(265,b,254,c)]. given #667 (F,wt=10): 12280 ilf_type(f24(power_set(c3)),binary_relation_type) | member(f24(c3),range_of(c4)). [resolve(12275,b,5543,a)]. given #668 (F,wt=8): 12367 ilf_type(f24(power_set(c3)),binary_relation_type) | -empty(range_of(c4)). [resolve(12280,b,206,a)]. given #669 (T,wt=11): 770 ilf_type(A,binary_relation_type) | member(f22(A),B) | -member(A,power_set(B)). [resolve(669,a,214,a)]. given #670 (T,wt=11): 772 ilf_type(c3,binary_relation_type) | member(ordered_pair(f25(f22(c3)),f22(c3)),c4). [resolve(669,a,116,a)]. given #671 (A,wt=16): 418 empty(A) | member(f24(A),B) | member(f9(B,A),B) | -member(f10(B,A),B). [resolve(265,b,230,b)]. given #672 (F,wt=9): 12454 ilf_type(c3,binary_relation_type) | member(f25(f22(c3)),domain_of(c4)). [resolve(772,b,252,b),unit_del(b,489)]. given #673 (F,wt=8): 12474 ilf_type(c3,binary_relation_type) | member(f25(f22(c3)),c2). [resolve(12454,b,542,a)]. given #674 (T,wt=11): 773 member(f22(f23(power_set(A))),A) | ilf_type(f23(power_set(A)),binary_relation_type). [resolve(277,a,669,a)]. given #675 (T,wt=11): 776 member(f24(f23(power_set(A))),A) | ilf_type(f23(power_set(A)),binary_relation_type). [resolve(277,a,264,a)]. given #676 (A,wt=16): 419 empty(A) | member(f24(A),B) | member(f9(B,A),B) | member(f10(B,A),A). [resolve(265,b,229,b)]. given #677 (F,wt=11): 852 member(f22(f24(power_set(A))),A) | ilf_type(f24(power_set(A)),binary_relation_type). [resolve(428,a,669,a)]. given #678 (F,wt=11): 856 member(f24(f24(power_set(A))),A) | ilf_type(f24(power_set(A)),binary_relation_type). [resolve(428,a,264,a)]. given #679 (T,wt=11): 864 member(f22(f16(power_set(A))),A) | ilf_type(f16(power_set(A)),binary_relation_type). [resolve(447,a,669,a)]. given #680 (T,wt=11): 868 member(f24(f16(power_set(A))),A) | ilf_type(f16(power_set(A)),binary_relation_type). [resolve(447,a,264,a)]. given #681 (A,wt=16): 420 empty(A) | member(f24(A),B) | -member(f9(B,A),A) | -member(f10(B,A),B). [resolve(265,b,228,b)]. given #682 (F,wt=11): 891 member(c4,power_set(A)) | member(f15(c4,A),cross_product(c2,c3)). [resolve(281,c,663,a)]. given #683 (F,wt=11): 906 member(domain_of(f5(A,B)),C) | -member(power_set(B),power_set(C)). [resolve(889,a,214,a)]. given #684 (T,wt=11): 926 member(range_of(f5(A,B)),C) | -member(power_set(A),power_set(C)). [resolve(911,a,214,a)]. given #685 (T,wt=11): 931 ilf_type(f15(power_set(A),B),member_type(power_set(A))) | member(A,B). [resolve(282,a,380,b),unit_del(a,213)]. given #686 (A,wt=16): 421 empty(A) | member(f24(A),B) | -member(f9(B,A),A) | member(f10(B,A),A). [resolve(265,b,227,b)]. given #687 (F,wt=10): 13100 ilf_type(f15(power_set(A),B),member_type(power_set(A))) | -empty(B). [resolve(931,b,206,a)]. given #688 (F,wt=11): 1006 empty(c3) | member(f25(f23(c3)),A) | -member(c2,power_set(A)). [resolve(977,b,214,a)]. given #689 (T,wt=11): 1032 empty(c3) | member(f24(c2),A) | member(f14(c2,A),c2). [resolve(1010,b,218,a)]. Low Water (keep): wt=40, part=0.89, limit=40 given #690 (T,wt=9): 13172 empty(c3) | member(f14(c2,A),c2) | -empty(A). [resolve(1032,b,206,a)]. given #691 (A,wt=16): 422 empty(A) | member(f24(A),B) | member(f11(A,B),A) | -member(f12(A,B),A). [resolve(265,b,225,b)]. given #692 (F,wt=11): 1033 empty(c3) | member(f24(c2),A) | -member(f14(c2,A),A). [resolve(1010,b,217,a)]. given #693 (F,wt=11): 1063 empty(f6(A)) | empty(A) | ilf_type(f16(f6(A)),member_type(A)). [resolve(631,a,212,c)]. given #694 (T,wt=11): 1085 empty(f6(f16(power_set(A)))) | member(f24(f16(power_set(A))),A). [resolve(1066,b,447,a)]. given #695 (T,wt=7): 13253 empty(f6(f16(power_set(A)))) | -empty(A). [resolve(1085,b,206,a)]. given #696 (A,wt=16): 423 empty(A) | member(f24(A),B) | member(f11(A,B),A) | member(f12(A,B),B). [resolve(265,b,224,b)]. given #697 (F,wt=9): 13254 empty(f6(f16(power_set(A)))) | member(f24(A),A). [resolve(1085,b,205,a)]. given #698 (F,wt=10): 13365 empty(f6(f16(power_set(c3)))) | member(f24(c3),range_of(c4)). [resolve(13254,b,5543,a)]. given #699 (T,wt=8): 13432 empty(f6(f16(power_set(c3)))) | -empty(range_of(c4)). [resolve(13365,b,206,a)]. given #700 (T,wt=11): 1086 empty(f6(f24(power_set(A)))) | member(f24(f24(power_set(A))),A). [resolve(1066,b,428,a)]. given #701 (A,wt=16): 424 empty(A) | member(f24(A),B) | -member(f11(A,B),B) | -member(f12(A,B),A). [resolve(265,b,223,b)]. given #702 (F,wt=7): 13483 empty(f6(f24(power_set(A)))) | -empty(A). [resolve(1086,b,206,a)]. given #703 (F,wt=9): 13484 empty(f6(f24(power_set(A)))) | member(f24(A),A). [resolve(1086,b,205,a)]. given #704 (T,wt=10): 13492 empty(f6(f24(power_set(c3)))) | member(f24(c3),range_of(c4)). [resolve(13484,b,5543,a)]. given #705 (T,wt=8): 13559 empty(f6(f24(power_set(c3)))) | -empty(range_of(c4)). [resolve(13492,b,206,a)]. given #706 (A,wt=16): 425 empty(A) | member(f24(A),B) | -member(f11(A,B),B) | member(f12(A,B),B). [resolve(265,b,222,b)]. given #707 (F,wt=11): 1089 empty(f6(f23(power_set(A)))) | member(f24(f23(power_set(A))),A). [resolve(1066,b,277,a)]. given #708 (F,wt=7): 13613 empty(f6(f23(power_set(A)))) | -empty(A). [resolve(1089,b,206,a)]. given #709 (T,wt=9): 13614 empty(f6(f23(power_set(A)))) | member(f24(A),A). [resolve(1089,b,205,a)]. given #710 (T,wt=10): 13619 empty(f6(f23(power_set(c3)))) | member(f24(c3),range_of(c4)). [resolve(13614,b,5543,a)]. given #711 (A,wt=18): 431 empty(A) | ordered_pair(f20(A,f24(A)),f21(A,f24(A))) = f24(A) | member(f22(A),A). [resolve(265,b,209,a)]. Low Water (keep): wt=39, part=0.86, limit=38 given #712 (F,wt=8): 13686 empty(f6(f23(power_set(c3)))) | -empty(range_of(c4)). [resolve(13619,b,206,a)]. given #713 (F,wt=11): 1101 empty(f6(A)) | member(f24(A),B) | -member(A,power_set(B)). [resolve(1066,b,214,a)]. given #714 (T,wt=11): 1106 empty(f6(c3)) | member(ordered_pair(f25(f24(c3)),f24(c3)),c4). [resolve(1066,b,116,a)]. given #715 (T,wt=5): 13814 empty(f6(c3)) | -empty(c4). [resolve(1106,b,206,a)]. given #716 (A,wt=20): 432 empty(A) | -ilf_type(A,subset_type(cross_product(B,C))) | ordered_pair(f18(A,f24(A)),f19(A,f24(A))) = f24(A). [resolve(265,b,131,b)]. Low Water (keep): wt=38, part=0.86, limit=38 given #717 (F,wt=7): 13815 empty(f6(c3)) | member(f24(c4),c4). [resolve(1106,b,205,a)]. given #718 (F,wt=9): 13800 empty(f6(c3)) | member(f25(f24(c3)),domain_of(c4)). [resolve(1106,b,252,b),unit_del(b,489)]. given #719 (T,wt=6): 13872 empty(f6(c3)) | -empty(domain_of(c4)). [resolve(13800,b,206,a)]. given #720 (T,wt=8): 13853 empty(f6(c3)) | member(f25(f24(c3)),c2). [resolve(13800,b,542,a)]. given #721 (A,wt=18): 433 empty(A) | ordered_pair(f18(A,f24(A)),f19(A,f24(A))) = f24(A) | member(f17(A),A). [resolve(265,b,125,a)]. given #722 (F,wt=5): 13903 empty(f6(c3)) | -empty(c2). [resolve(13853,b,206,a)]. given #723 (F,wt=7): 13904 empty(f6(c3)) | member(f24(c2),c2). [resolve(13853,b,205,a)]. given #724 (T,wt=9): 13824 empty(f6(c3)) | member(f24(c4),cross_product(c2,c3)). [resolve(13815,b,680,a)]. given #725 (T,wt=7): 13966 empty(f6(c3)) | -empty(cross_product(c2,c3)). [resolve(13824,b,206,a)]. given #726 (A,wt=17): 434 empty(A) | ordered_pair(f18(A,f24(A)),f19(A,f24(A))) = f24(A) | -ilf_type(A,binary_relation_type). [resolve(265,b,123,a)]. given #727 (F,wt=9): 13873 empty(f6(c3)) | member(f24(domain_of(c4)),domain_of(c4)). [resolve(13800,b,205,a)]. given #728 (F,wt=8): 13972 empty(f6(c3)) | member(f24(domain_of(c4)),c2). [resolve(13873,b,542,a)]. Low Water (keep): wt=37, part=0.85, limit=37 given #729 (T,wt=11): 1131 empty(f6(A)) | empty(A) | ilf_type(f24(f6(A)),member_type(A)). [resolve(632,a,212,c)]. given #730 (T,wt=11): 1161 empty(f6(A)) | empty(A) | ilf_type(f23(f6(A)),member_type(A)). [resolve(635,a,212,c)]. given #731 (A,wt=17): 436 empty(range_of(A)) | -ilf_type(A,binary_relation_type) | member(ordered_pair(f1(A,f16(range_of(A))),f16(range_of(A))),A). [resolve(272,b,254,c)]. given #732 (F,wt=11): 1199 empty(range_of(c4)) | empty(c3) | ilf_type(f16(range_of(c4)),member_type(c3)). [resolve(686,a,212,c)]. given #733 (F,wt=11): 1217 empty(range_of(c4)) | member(f24(c3),A) | -member(c3,power_set(A)). [resolve(1202,b,214,a)]. given #734 (T,wt=11): 1222 empty(range_of(c4)) | member(ordered_pair(f25(f24(c3)),f24(c3)),c4). [resolve(1202,b,116,a)]. given #735 (T,wt=5): 14047 empty(range_of(c4)) | -empty(c4). [resolve(1222,b,206,a)]. given #736 (A,wt=16): 437 empty(A) | member(f16(A),B) | member(f9(B,A),B) | -member(f10(B,A),B). [resolve(272,b,230,b)]. given #737 (F,wt=7): 14048 empty(range_of(c4)) | member(f24(c4),c4). [resolve(1222,b,205,a)]. given #738 (F,wt=9): 14033 empty(range_of(c4)) | member(f25(f24(c3)),domain_of(c4)). [resolve(1222,b,252,b),unit_del(b,489)]. given #739 (T,wt=6): 14104 empty(range_of(c4)) | -empty(domain_of(c4)). [resolve(14033,b,206,a)]. given #740 (T,wt=8): 14085 empty(range_of(c4)) | member(f25(f24(c3)),c2). [resolve(14033,b,542,a)]. given #741 (A,wt=16): 438 empty(A) | mem