============================== FOF-Prover9 =========================== FOF-Prover9 (32) version November-2006, November 2006. Process 3794 was started by mccune on cleo.thornwood, Wed Nov 22 11:23:45 2006 The command was "/home/mccune/bin/fof-prover9 -f SET668+3.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file SET668+3.in set(prolog_style_variables). formulas(assumptions). (all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> (subset(B,C) & subset(C,B) -> 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,relation_type(B,C)) -> (subset(identity_relation_of(D),E) -> subset(D,domain(B,C,E)) & subset(D,range(B,C,E))))))))))). (all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> (all D (ilf_type(D,set_type) -> (member(ordered_pair(C,D),identity_relation_of(B)) <-> member(C,B) & C = D))))))). (all B (ilf_type(B,set_type) -> ilf_type(identity_relation_of(B),binary_relation_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) -> (subset(B,C) <-> (all D (ilf_type(D,set_type) -> (member(D,B) -> member(D,C))))))))). (all B (ilf_type(B,binary_relation_type) -> (all C (ilf_type(C,binary_relation_type) -> (subset(B,C) <-> (all D (ilf_type(D,set_type) -> (all E (ilf_type(E,set_type) -> (member(ordered_pair(D,E),B) -> member(ordered_pair(D,E),C))))))))))). (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) -> (all C (ilf_type(C,set_type) -> ilf_type(cross_product(B,C),set_type))))). (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) -> ilf_type(ordered_pair(B,C),set_type))))). (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) -> subset(B,B))). (all B (ilf_type(B,binary_relation_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(C,B)) -> (subset(identity_relation_of(C),D) -> C = domain(C,B,D) & subset(C,range(C,B,D))))))))). end_of_list. ============================== end of input ========================== % clear(auto_denials), because it is incompatiable with FOF reduction. Attempting problem reduction; original problem has = <482,104>. Problem reduction (0.00 sec) gives 2 independent subproblems: ( <641,82> <641,82> ). Max nnf_size of subproblems is 641; max cnf_max is 82. ============================== FOF REDUCTION MULTISEARCH ============= Subproblem 1 of 2 (negated): ((all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | - subset(B,C) | - subset(C,B) | =(C,B))))) & (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,relation_type(B,C)) | - subset(identity_relation_of(D),E) | subset(D,domain(B,C,E)))))))))) & (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,relation_type(B,C)) | - subset(identity_relation_of(D),E) | subset(D,range(B,C,E)))))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | - member(C,B) | (all D (- ilf_type(D,set_type) | member(ordered_pair(C,D),identity_relation_of(B)) | - =(D,C))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | member(C,B) | (all D (- ilf_type(D,set_type) | - member(ordered_pair(C,D),identity_relation_of(B)))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,set_type) | =(D,C) | - member(ordered_pair(C,D),identity_relation_of(B)))))))) & (all B (- ilf_type(B,set_type) | ilf_type(identity_relation_of(B),binary_relation_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) | 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,binary_relation_type) | (all C (- ilf_type(C,binary_relation_type) | subset(B,C) | (exists D (ilf_type(D,set_type) & (exists E (ilf_type(E,set_type) & member(ordered_pair(D,E),B) & - member(ordered_pair(D,E),C))))))))) & (all B (- ilf_type(B,binary_relation_type) | (all C (- ilf_type(C,binary_relation_type) | (all D (- ilf_type(D,set_type) | (all E (- ilf_type(E,set_type) | - member(ordered_pair(D,E),B) | member(ordered_pair(D,E),C))))) | - subset(B,C))))) & (all B (- ilf_type(B,binary_relation_type) | (all C (- ilf_type(C,binary_relation_type) | (all D (- ilf_type(D,set_type) | (all E (- ilf_type(E,set_type) | - member(ordered_pair(D,E),B) | member(ordered_pair(D,E),C))))) | (exists D (ilf_type(D,set_type) & (exists E (ilf_type(E,set_type) & member(ordered_pair(D,E),B) & - member(ordered_pair(D,E),C))))))))) & (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) | (all C (- ilf_type(C,set_type) | ilf_type(cross_product(B,C),set_type))))) & (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) | ilf_type(ordered_pair(B,C),set_type))))) & (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) | subset(B,B))) & (all B (- ilf_type(B,binary_relation_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_of(D),domain(B,C,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_of(D),range(B,C,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(C,B)) & subset(identity_relation_of(C),D) & - =(domain(C,B,D),C)))))))). Child search process 3795 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). -ilf_type(A,set_type) | -ilf_type(B,set_type) | -subset(A,B) | -subset(B,A) | B = A. [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | -ilf_type(D,relation_type(A,B)) | -subset(identity_relation_of(C),D) | subset(C,domain(A,B,D)). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | -ilf_type(D,relation_type(A,B)) | -subset(identity_relation_of(C),D) | subset(C,range(A,B,D)). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | -ilf_type(C,set_type) | member(ordered_pair(B,C),identity_relation_of(A)) | C != B. [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | member(B,A) | -ilf_type(C,set_type) | -member(ordered_pair(B,C),identity_relation_of(A)). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | C = B | -member(ordered_pair(B,C),identity_relation_of(A)). [assumption]. -ilf_type(A,set_type) | ilf_type(identity_relation_of(A),binary_relation_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(f1(A,B),relation_type(B,A)). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | subset(A,B) | ilf_type(f2(A,B),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | subset(A,B) | member(f2(A,B),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | subset(A,B) | -member(f2(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(f3(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(f3(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(f3(A,B),B). [assumption]. -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | subset(A,B) | ilf_type(f4(A,B),set_type). [assumption]. -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | subset(A,B) | ilf_type(f5(A,B),set_type). [assumption]. -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | subset(A,B) | member(ordered_pair(f4(A,B),f5(A,B)),A). [assumption]. -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | subset(A,B) | -member(ordered_pair(f4(A,B),f5(A,B)),B). [assumption]. -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | -ilf_type(C,set_type) | -ilf_type(D,set_type) | -member(ordered_pair(C,D),A) | member(ordered_pair(C,D),B) | -subset(A,B). [assumption]. -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | -ilf_type(C,set_type) | -ilf_type(D,set_type) | -member(ordered_pair(C,D),A) | member(ordered_pair(C,D),B) | ilf_type(f6(A,B),set_type). [assumption]. -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | -ilf_type(C,set_type) | -ilf_type(D,set_type) | -member(ordered_pair(C,D),A) | member(ordered_pair(C,D),B) | ilf_type(f7(A,B),set_type). [assumption]. -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | -ilf_type(C,set_type) | -ilf_type(D,set_type) | -member(ordered_pair(C,D),A) | member(ordered_pair(C,D),B) | member(ordered_pair(f6(A,B),f7(A,B)),A). [assumption]. -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | -ilf_type(C,set_type) | -ilf_type(D,set_type) | -member(ordered_pair(C,D),A) | member(ordered_pair(C,D),B) | -member(ordered_pair(f6(A,B),f7(A,B)),B). [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(B,set_type) | ilf_type(cross_product(A,B),set_type). [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(ordered_pair(A,B),set_type). [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(f8(A),subset_type(A)). [assumption]. -ilf_type(A,set_type) | subset(A,A). [assumption]. -ilf_type(A,binary_relation_type) | subset(A,A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | member(A,power_set(B)) | ilf_type(f9(A,B),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | member(A,power_set(B)) | member(f9(A,B),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | member(A,power_set(B)) | -member(f9(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(f10(A),member_type(A)). [assumption]. -ilf_type(A,set_type) | relation_like(A) | ilf_type(f11(A),set_type). [assumption]. -ilf_type(A,set_type) | relation_like(A) | member(f11(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) != f11(A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f12(A,B),set_type) | -relation_like(A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f13(A,B),set_type) | -relation_like(A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ordered_pair(f12(A,B),f13(A,B)) = B | -relation_like(A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f14(A,B),set_type) | ilf_type(f16(A),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f14(A,B),set_type) | member(f16(A),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f14(A,B),set_type) | -ilf_type(C,set_type) | -ilf_type(D,set_type) | ordered_pair(C,D) != f16(A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f15(A,B),set_type) | ilf_type(f16(A),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f15(A,B),set_type) | member(f16(A),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f15(A,B),set_type) | -ilf_type(C,set_type) | -ilf_type(D,set_type) | ordered_pair(C,D) != f16(A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ordered_pair(f14(A,B),f15(A,B)) = B | ilf_type(f16(A),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ordered_pair(f14(A,B),f15(A,B)) = B | member(f16(A),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ordered_pair(f14(A,B),f15(A,B)) = B | -ilf_type(C,set_type) | -ilf_type(D,set_type) | ordered_pair(C,D) != f16(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(f17(A),set_type). [assumption]. -ilf_type(A,set_type) | empty(A) | member(f17(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(f18(A),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | member(f18(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_of(C) = domain(A,B,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_of(C) = range(A,B,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(c3,c2)). [assumption]. subset(identity_relation_of(c3),c4). [assumption]. domain(c3,c2,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(f11(A),set_type). [assumption]. 4 -ilf_type(A,set_type) | relation_like(A) | member(f11(A),A). [assumption]. Derived: -ilf_type(A,set_type) | member(f11(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) != f11(A). [assumption]. Derived: -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | ordered_pair(B,C) != f11(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(f12(A,B),set_type) | -relation_like(A). [assumption]. 7 -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f13(A,B),set_type) | -relation_like(A). [assumption]. 8 -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ordered_pair(f12(A,B),f13(A,B)) = B | -relation_like(A). [assumption]. Derived: -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ordered_pair(f12(A,B),f13(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(f12(A,B),f13(A,B)) = B | -ilf_type(A,set_type) | member(f11(A),A). [resolve(8,e,4,b)]. Derived: -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ordered_pair(f12(A,B),f13(A,B)) = B | -ilf_type(A,set_type) | -ilf_type(C,set_type) | -ilf_type(D,set_type) | ordered_pair(C,D) != f11(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(f12(C,D),f13(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(f12(A,B),f13(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, cross_product, f1, f2, f3, f4, f5, f6, f7, f9, f12, f13, f14, f15, subset_type, identity_relation_of, power_set, member_type, domain_of, range_of, f8, f10, f11, f16, f17, f18, 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) % set(neg_ur_resolution). % (non-Horn, less than 100 clauses) Auto_process settings: % set(factor). % (non-Horn) % set(back_unit_deletion). % (non-Horn) % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 30 -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | subset(A,B) | member(ordered_pair(f4(A,B),f5(A,B)),A). [assumption]. 31 -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | subset(A,B) | -member(ordered_pair(f4(A,B),f5(A,B)),B). [assumption]. 43 ilf_type(c1,binary_relation_type). [assumption]. 81 ilf_type(A,set_type). [assumption]. 82 ilf_type(c4,relation_type(c3,c2)). [assumption]. 83 subset(identity_relation_of(c3),c4). [assumption]. 84 domain(c3,c2,c4) != c3. [assumption]. 86 member(f11(A),A) | ilf_type(A,binary_relation_type). [copy(85),merge(c),unit_del(a,81)]. 88 f11(A) != ordered_pair(B,C) | ilf_type(A,binary_relation_type). [copy(87),flip(d),merge(e),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. 90 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | -ilf_type(B,binary_relation_type). [copy(89),merge(e),unit_del(a,81),unit_del(b,81)]. 92 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | member(f11(B),B). [copy(91),merge(e),unit_del(a,81),unit_del(b,81)]. 94 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | f11(B) != ordered_pair(C,D). [copy(93),flip(h),merge(e),unit_del(a,81),unit_del(b,81),unit_del(e,81),unit_del(f,81)]. 96 -ilf_type(A,subset_type(cross_product(B,C))) | ilf_type(A,binary_relation_type). [copy(95),unit_del(a,81),unit_del(b,81),unit_del(d,81)]. 98 -ilf_type(A,subset_type(cross_product(B,C))) | -member(D,A) | ordered_pair(f12(A,D),f13(A,D)) = D. [copy(97),unit_del(a,81),unit_del(b,81),unit_del(d,81),unit_del(e,81)]. 100 -empty(A) | ilf_type(A,binary_relation_type). [copy(99),merge(c),unit_del(b,81)]. 111 -member(A,B) | member(ordered_pair(A,A),identity_relation_of(B)). [factor(14,b,d),xx(e),unit_del(a,81),unit_del(b,81)]. 131 subset(A,A). [factor(37,a,b),xx(c),unit_del(a,81)]. 138 -member(power_set(A),power_set(A)) | member(power_set(A),A). [factor(52,d,f),merge(c),unit_del(a,81),unit_del(b,81)]. 154 -ilf_type(A,relation_type(B,C)) | ilf_type(range(B,C,A),subset_type(C)). [back_unit_del(80),unit_del(a,81),unit_del(b,81)]. 155 -ilf_type(A,relation_type(B,C)) | range(B,C,A) = range_of(A). [back_unit_del(79),unit_del(a,81),unit_del(b,81)]. 156 -ilf_type(A,relation_type(B,C)) | ilf_type(domain(B,C,A),subset_type(B)). [back_unit_del(77),unit_del(a,81),unit_del(b,81)]. 157 -ilf_type(A,relation_type(B,C)) | domain(B,C,A) = domain_of(A). [back_unit_del(76),unit_del(a,81),unit_del(b,81)]. 158 -member(A,B) | member(f18(B),B). [back_unit_del(74),unit_del(a,81),unit_del(b,81)]. 159 -member(A,B) | -empty(B). [back_unit_del(72),unit_del(a,81),unit_del(b,81)]. 160 empty(A) | member(f17(A),A). [back_unit_del(71),unit_del(a,81)]. 161 -member(A,B) | ordered_pair(f14(B,A),f15(B,A)) = A | f16(B) != ordered_pair(C,D). [back_unit_del(69),unit_del(a,81),unit_del(b,81),unit_del(e,81),unit_del(f,81)]. 162 -member(A,B) | ordered_pair(f14(B,A),f15(B,A)) = A | member(f16(B),B). [back_unit_del(67),unit_del(a,81),unit_del(b,81)]. 163 empty(A) | ilf_type(f10(A),member_type(A)). [back_unit_del(57),unit_del(b,81)]. 164 empty(A) | member(B,A) | -ilf_type(B,member_type(A)). [back_unit_del(56),unit_del(a,81),unit_del(c,81)]. 165 empty(A) | ilf_type(B,member_type(A)) | -member(B,A). [back_unit_del(55),unit_del(a,81),unit_del(c,81)]. 166 -empty(power_set(A)). [back_unit_del(53),unit_del(a,81)]. 167 -member(A,B) | member(A,C) | -member(B,power_set(C)). [back_unit_del(52),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. 168 member(A,power_set(B)) | -member(f9(A,B),B). [back_unit_del(51),unit_del(a,81),unit_del(b,81)]. 169 member(A,power_set(B)) | member(f9(A,B),A). [back_unit_del(50),unit_del(a,81),unit_del(b,81)]. 170 ilf_type(f8(A),subset_type(A)). [back_unit_del(46),unit_del(a,81)]. 171 ilf_type(A,member_type(power_set(B))) | -ilf_type(A,subset_type(B)). [back_unit_del(45),unit_del(a,81),unit_del(b,81)]. 172 ilf_type(A,subset_type(B)) | -ilf_type(A,member_type(power_set(B))). [back_unit_del(44),unit_del(a,81),unit_del(b,81)]. 173 subset(A,B) | A != B. [back_unit_del(38),unit_del(a,81),unit_del(b,81)]. 174 subset(A,B) | B != A. [back_unit_del(37),unit_del(a,81),unit_del(b,81)]. 175 -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | -member(ordered_pair(C,D),A) | member(ordered_pair(C,D),B) | -member(ordered_pair(f6(A,B),f7(A,B)),B). [back_unit_del(36),unit_del(c,81),unit_del(d,81)]. 176 -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | -member(ordered_pair(C,D),A) | member(ordered_pair(C,D),B) | member(ordered_pair(f6(A,B),f7(A,B)),A). [back_unit_del(35),unit_del(c,81),unit_del(d,81)]. 178 -member(A,B) | member(A,C) | -member(f3(B,C),C). [back_unit_del(27),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. 179 -member(A,B) | member(A,C) | member(f3(B,C),B). [back_unit_del(26),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. 180 -member(A,B) | member(A,C) | -subset(B,C). [back_unit_del(24),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. 181 subset(A,B) | -member(f2(A,B),B). [back_unit_del(23),unit_del(a,81),unit_del(b,81)]. 182 subset(A,B) | member(f2(A,B),A). [back_unit_del(22),unit_del(a,81),unit_del(b,81)]. 183 ilf_type(f1(A,B),relation_type(B,A)). [back_unit_del(20),unit_del(a,81),unit_del(b,81)]. 184 -ilf_type(A,relation_type(B,C)) | ilf_type(A,subset_type(cross_product(B,C))). [back_unit_del(19),unit_del(a,81),unit_del(b,81)]. 185 -ilf_type(A,subset_type(cross_product(B,C))) | ilf_type(A,relation_type(B,C)). [back_unit_del(18),unit_del(a,81),unit_del(b,81)]. 186 ilf_type(identity_relation_of(A),binary_relation_type). [back_unit_del(17),unit_del(a,81)]. 187 A = B | -member(ordered_pair(B,A),identity_relation_of(C)). [back_unit_del(16),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. 188 member(A,B) | -member(ordered_pair(A,C),identity_relation_of(B)). [back_unit_del(15),unit_del(a,81),unit_del(b,81),unit_del(d,81)]. 189 -member(A,B) | member(ordered_pair(A,C),identity_relation_of(B)) | C != A. [back_unit_del(14),unit_del(a,81),unit_del(b,81),unit_del(d,81)]. 190 -ilf_type(A,relation_type(B,C)) | -subset(identity_relation_of(D),A) | subset(D,range(B,C,A)). [back_unit_del(13),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. 191 -ilf_type(A,relation_type(B,C)) | -subset(identity_relation_of(D),A) | subset(D,domain(B,C,A)). [back_unit_del(12),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. 192 -subset(A,B) | -subset(B,A) | B = A. [back_unit_del(11),unit_del(a,81),unit_del(b,81)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=18): 30 -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | subset(A,B) | member(ordered_pair(f4(A,B),f5(A,B)),A). [assumption]. given #2 (I,wt=18): 31 -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | subset(A,B) | -member(ordered_pair(f4(A,B),f5(A,B)),B). [assumption]. given #3 (I,wt=3): 43 ilf_type(c1,binary_relation_type). [assumption]. given #4 (I,wt=3): 81 ilf_type(A,set_type). [assumption]. given #5 (I,wt=5): 82 ilf_type(c4,relation_type(c3,c2)). [assumption]. given #6 (I,wt=4): 83 subset(identity_relation_of(c3),c4). [assumption]. given #7 (I,wt=6): 84 domain(c3,c2,c4) != c3. [assumption]. given #8 (I,wt=7): 86 member(f11(A),A) | ilf_type(A,binary_relation_type). [copy(85),merge(c),unit_del(a,81)]. given #9 (I,wt=9): 88 f11(A) != ordered_pair(B,C) | ilf_type(A,binary_relation_type). [copy(87),flip(d),merge(e),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. given #10 (I,wt=15): 90 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | -ilf_type(B,binary_relation_type). [copy(89),merge(e),unit_del(a,81),unit_del(b,81)]. given #11 (I,wt=16): 92 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | member(f11(B),B). [copy(91),merge(e),unit_del(a,81),unit_del(b,81)]. given #12 (I,wt=18): 94 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | f11(B) != ordered_pair(C,D). [copy(93),flip(h),merge(e),unit_del(a,81),unit_del(b,81),unit_del(e,81),unit_del(f,81)]. given #13 (I,wt=9): 96 -ilf_type(A,subset_type(cross_product(B,C))) | ilf_type(A,binary_relation_type). [copy(95),unit_del(a,81),unit_del(b,81),unit_del(d,81)]. given #14 (I,wt=18): 98 -ilf_type(A,subset_type(cross_product(B,C))) | -member(D,A) | ordered_pair(f12(A,D),f13(A,D)) = D. [copy(97),unit_del(a,81),unit_del(b,81),unit_del(d,81),unit_del(e,81)]. given #15 (I,wt=5): 100 -empty(A) | ilf_type(A,binary_relation_type). [copy(99),merge(c),unit_del(b,81)]. given #16 (I,wt=9): 111 -member(A,B) | member(ordered_pair(A,A),identity_relation_of(B)). [factor(14,b,d),xx(e),unit_del(a,81),unit_del(b,81)]. given #17 (I,wt=3): 131 subset(A,A). [factor(37,a,b),xx(c),unit_del(a,81)]. given #18 (I,wt=9): 138 -member(power_set(A),power_set(A)) | member(power_set(A),A). [factor(52,d,f),merge(c),unit_del(a,81),unit_del(b,81)]. given #19 (I,wt=12): 154 -ilf_type(A,relation_type(B,C)) | ilf_type(range(B,C,A),subset_type(C)). [back_unit_del(80),unit_del(a,81),unit_del(b,81)]. given #20 (I,wt=12): 155 -ilf_type(A,relation_type(B,C)) | range(B,C,A) = range_of(A). [back_unit_del(79),unit_del(a,81),unit_del(b,81)]. given #21 (I,wt=12): 156 -ilf_type(A,relation_type(B,C)) | ilf_type(domain(B,C,A),subset_type(B)). [back_unit_del(77),unit_del(a,81),unit_del(b,81)]. given #22 (I,wt=12): 157 -ilf_type(A,relation_type(B,C)) | domain(B,C,A) = domain_of(A). [back_unit_del(76),unit_del(a,81),unit_del(b,81)]. given #23 (I,wt=7): 158 -member(A,B) | member(f18(B),B). [back_unit_del(74),unit_del(a,81),unit_del(b,81)]. given #24 (I,wt=5): 159 -member(A,B) | -empty(B). [back_unit_del(72),unit_del(a,81),unit_del(b,81)]. given #25 (I,wt=6): 160 empty(A) | member(f17(A),A). [back_unit_del(71),unit_del(a,81)]. given #26 (I,wt=18): 161 -member(A,B) | ordered_pair(f14(B,A),f15(B,A)) = A | f16(B) != ordered_pair(C,D). [back_unit_del(69),unit_del(a,81),unit_del(b,81),unit_del(e,81),unit_del(f,81)]. given #27 (I,wt=16): 162 -member(A,B) | ordered_pair(f14(B,A),f15(B,A)) = A | member(f16(B),B). [back_unit_del(67),unit_del(a,81),unit_del(b,81)]. given #28 (I,wt=7): 163 empty(A) | ilf_type(f10(A),member_type(A)). [back_unit_del(57),unit_del(b,81)]. given #29 (I,wt=9): 164 empty(A) | member(B,A) | -ilf_type(B,member_type(A)). [back_unit_del(56),unit_del(a,81),unit_del(c,81)]. given #30 (I,wt=9): 165 empty(A) | ilf_type(B,member_type(A)) | -member(B,A). [back_unit_del(55),unit_del(a,81),unit_del(c,81)]. given #31 (I,wt=3): 166 -empty(power_set(A)). [back_unit_del(53),unit_del(a,81)]. given #32 (I,wt=10): 167 -member(A,B) | member(A,C) | -member(B,power_set(C)). [back_unit_del(52),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. given #33 (I,wt=9): 168 member(A,power_set(B)) | -member(f9(A,B),B). [back_unit_del(51),unit_del(a,81),unit_del(b,81)]. given #34 (I,wt=9): 169 member(A,power_set(B)) | member(f9(A,B),A). [back_unit_del(50),unit_del(a,81),unit_del(b,81)]. given #35 (I,wt=5): 170 ilf_type(f8(A),subset_type(A)). [back_unit_del(46),unit_del(a,81)]. given #36 (I,wt=9): 171 ilf_type(A,member_type(power_set(B))) | -ilf_type(A,subset_type(B)). [back_unit_del(45),unit_del(a,81),unit_del(b,81)]. given #37 (I,wt=9): 172 ilf_type(A,subset_type(B)) | -ilf_type(A,member_type(power_set(B))). [back_unit_del(44),unit_del(a,81),unit_del(b,81)]. given #38 (I,wt=6): 173 subset(A,B) | A != B. [back_unit_del(38),unit_del(a,81),unit_del(b,81)]. given #39 (I,wt=6): 174 subset(A,B) | B != A. [back_unit_del(37),unit_del(a,81),unit_del(b,81)]. given #40 (I,wt=25): 175 -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | -member(ordered_pair(C,D),A) | member(ordered_pair(C,D),B) | -member(ordered_pair(f6(A,B),f7(A,B)),B). [back_unit_del(36),unit_del(c,81),unit_del(d,81)]. given #41 (I,wt=25): 176 -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | -member(ordered_pair(C,D),A) | member(ordered_pair(C,D),B) | member(ordered_pair(f6(A,B),f7(A,B)),A). [back_unit_del(35),unit_del(c,81),unit_del(d,81)]. given #42 (I,wt=11): 178 -member(A,B) | member(A,C) | -member(f3(B,C),C). [back_unit_del(27),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. given #43 (I,wt=11): 179 -member(A,B) | member(A,C) | member(f3(B,C),B). [back_unit_del(26),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. given #44 (I,wt=9): 180 -member(A,B) | member(A,C) | -subset(B,C). [back_unit_del(24),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. given #45 (I,wt=8): 181 subset(A,B) | -member(f2(A,B),B). [back_unit_del(23),unit_del(a,81),unit_del(b,81)]. given #46 (I,wt=8): 182 subset(A,B) | member(f2(A,B),A). [back_unit_del(22),unit_del(a,81),unit_del(b,81)]. given #47 (I,wt=7): 183 ilf_type(f1(A,B),relation_type(B,A)). [back_unit_del(20),unit_del(a,81),unit_del(b,81)]. given #48 (I,wt=11): 184 -ilf_type(A,relation_type(B,C)) | ilf_type(A,subset_type(cross_product(B,C))). [back_unit_del(19),unit_del(a,81),unit_del(b,81)]. given #49 (I,wt=11): 185 -ilf_type(A,subset_type(cross_product(B,C))) | ilf_type(A,relation_type(B,C)). [back_unit_del(18),unit_del(a,81),unit_del(b,81)]. given #50 (I,wt=4): 186 ilf_type(identity_relation_of(A),binary_relation_type). [back_unit_del(17),unit_del(a,81)]. given #51 (I,wt=9): 187 A = B | -member(ordered_pair(B,A),identity_relation_of(C)). [back_unit_del(16),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. given #52 (I,wt=9): 188 member(A,B) | -member(ordered_pair(A,C),identity_relation_of(B)). [back_unit_del(15),unit_del(a,81),unit_del(b,81),unit_del(d,81)]. given #53 (I,wt=12): 189 -member(A,B) | member(ordered_pair(A,C),identity_relation_of(B)) | C != A. [back_unit_del(14),unit_del(a,81),unit_del(b,81),unit_del(d,81)]. given #54 (I,wt=15): 190 -ilf_type(A,relation_type(B,C)) | -subset(identity_relation_of(D),A) | subset(D,range(B,C,A)). [back_unit_del(13),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. given #55 (I,wt=15): 191 -ilf_type(A,relation_type(B,C)) | -subset(identity_relation_of(D),A) | subset(D,domain(B,C,A)). [back_unit_del(12),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. given #56 (I,wt=9): 192 -subset(A,B) | -subset(B,A) | B = A. [back_unit_del(11),unit_del(a,81),unit_del(b,81)]. given #57 (F,wt=4): 202 domain_of(c4) != c3. [back_rewrite(84),rewrite(200(4))]. given #58 (F,wt=7): 259 -member(ordered_pair(c3,domain_of(c4)),identity_relation_of(A)). [ur(187,a,202,a)]. given #59 (T,wt=4): 218 member(A,power_set(A)). [resolve(169,b,168,b),merge(b)]. given #60 (T,wt=5): 198 ilf_type(range_of(c4),subset_type(c2)). [back_rewrite(196),rewrite(197(4))]. given #61 (A,wt=15): 193 -ilf_type(A,binary_relation_type) | subset(A,c1) | member(ordered_pair(f4(A,c1),f5(A,c1)),A). [resolve(43,a,30,b)]. given #62 (F,wt=7): 260 -member(ordered_pair(domain_of(c4),c3),identity_relation_of(A)). [ur(187,a,202,a(flip))]. given #63 (F,wt=8): 274 -subset(power_set(ordered_pair(c3,domain_of(c4))),identity_relation_of(A)). [ur(180,a,218,a,b,259,a)]. given #64 (T,wt=5): 201 ilf_type(domain_of(c4),subset_type(c3)). [back_rewrite(199),rewrite(200(4))]. given #65 (T,wt=5): 267 ilf_type(A,member_type(power_set(A))). [resolve(218,a,165,c),unit_del(a,166)]. given #66 (A,wt=15): 194 -ilf_type(A,binary_relation_type) | subset(c1,A) | member(ordered_pair(f4(c1,A),f5(c1,A)),c1). [resolve(43,a,30,a)]. given #67 (F,wt=8): 280 -subset(power_set(ordered_pair(domain_of(c4),c3)),identity_relation_of(A)). [ur(180,a,218,a,b,260,a)]. given #68 (F,wt=8): 285 power_set(ordered_pair(c3,domain_of(c4))) != identity_relation_of(A). [ur(174,a,274,a),flip(a)]. given #69 (T,wt=4): 287 ilf_type(A,subset_type(A)). [resolve(267,a,172,b)]. given #70 (T,wt=5): 295 ilf_type(cross_product(A,B),binary_relation_type). [resolve(287,a,96,a)]. given #71 (A,wt=11): 195 member(ordered_pair(f11(A),f11(A)),identity_relation_of(A)) | ilf_type(A,binary_relation_type). [resolve(111,a,86,a)]. given #72 (F,wt=8): 291 power_set(ordered_pair(domain_of(c4),c3)) != identity_relation_of(A). [ur(174,a,280,a),flip(a)]. given #73 (F,wt=9): 276 -member(power_set(ordered_pair(c3,domain_of(c4))),power_set(identity_relation_of(A))). [ur(167,a,218,a,b,259,a)]. given #74 (T,wt=6): 204 empty(A) | member(f18(A),A). [resolve(160,b,158,a)]. given #75 (T,wt=6): 211 empty(A) | member(f10(A),A). [resolve(164,c,163,b),merge(c)]. given #76 (A,wt=7): 197 range(c3,c2,c4) = range_of(c4). [resolve(155,a,82,a)]. given #77 (F,wt=9): 282 -member(power_set(ordered_pair(domain_of(c4),c3)),power_set(identity_relation_of(A))). [ur(167,a,218,a,b,260,a)]. given #78 (F,wt=10): 261 -member(ordered_pair(ordered_pair(c3,domain_of(c4)),A),identity_relation_of(identity_relation_of(B))). [ur(188,a,259,a)]. given #79 (T,wt=6): 223 member(A,power_set(B)) | -empty(A). [resolve(169,b,159,a)]. given #80 (T,wt=6): 230 ilf_type(f8(cross_product(A,B)),binary_relation_type). [resolve(170,a,96,a)]. given #81 (A,wt=7): 200 domain(c3,c2,c4) = domain_of(c4). [resolve(157,a,82,a)]. given #82 (F,wt=10): 279 -member(ordered_pair(ordered_pair(domain_of(c4),c3),A),identity_relation_of(identity_relation_of(B))). [ur(188,a,260,a)]. given #83 (F,wt=10): 316 -subset(power_set(power_set(ordered_pair(c3,domain_of(c4)))),power_set(identity_relation_of(A))). [ur(180,a,218,a,b,276,a)]. given #84 (T,wt=6): 231 ilf_type(f8(A),member_type(power_set(A))). [resolve(171,b,170,a)]. given #85 (T,wt=5): 361 member(f8(A),power_set(A)). [resolve(231,a,164,c),unit_del(a,166)]. given #86 (A,wt=7): 203 member(f18(A),A) | ilf_type(A,binary_relation_type). [resolve(158,a,86,a)]. given #87 (F,wt=8): 375 -member(ordered_pair(domain_of(c4),c3),f8(identity_relation_of(A))). [ur(167,b,260,a,c,361,a)]. given #88 (F,wt=8): 376 -member(ordered_pair(c3,domain_of(c4)),f8(identity_relation_of(A))). [ur(167,b,259,a,c,361,a)]. given #89 (T,wt=6): 232 ilf_type(f10(power_set(A)),subset_type(A)). [resolve(172,b,163,b),unit_del(b,166)]. given #90 (T,wt=6): 246 ilf_type(c4,subset_type(cross_product(c3,c2))). [resolve(184,a,82,a)]. given #91 (A,wt=10): 205 empty(A) | member(ordered_pair(f17(A),f17(A)),identity_relation_of(A)). [resolve(160,b,111,a)]. given #92 (F,wt=9): 383 -subset(power_set(ordered_pair(domain_of(c4),c3)),f8(identity_relation_of(A))). [ur(180,a,218,a,b,375,a)]. given #93 (F,wt=9): 385 -member(ordered_pair(domain_of(c4),c3),f8(f8(identity_relation_of(A)))). [ur(167,b,375,a,c,361,a)]. given #94 (T,wt=3): 396 ilf_type(c4,binary_relation_type). [resolve(246,a,96,a)]. given #95 (T,wt=5): 404 empty(A) | -empty(identity_relation_of(A)). [resolve(205,b,159,a)]. given #96 (A,wt=20): 206 empty(A) | -ilf_type(A,subset_type(cross_product(B,C))) | ordered_pair(f12(A,f17(A)),f13(A,f17(A))) = f17(A). [resolve(160,b,98,b)]. given #97 (F,wt=4): 422 -empty(identity_relation_of(power_set(A))). [ur(404,a,166,a)]. given #98 (F,wt=5): 427 -empty(identity_relation_of(identity_relation_of(power_set(A)))). [ur(404,a,422,a)]. given #99 (T,wt=6): 269 member(f18(power_set(A)),power_set(A)). [resolve(218,a,158,a)]. given #100 (T,wt=6): 277 ilf_type(range_of(c4),member_type(power_set(c2))). [resolve(198,a,171,b)]. given #101 (A,wt=18): 207 empty(A) | ordered_pair(f12(A,f17(A)),f13(A,f17(A))) = f17(A) | member(f11(A),A). [resolve(160,b,92,a)]. given #102 (F,wt=6): 430 -empty(identity_relation_of(identity_relation_of(identity_relation_of(power_set(A))))). [ur(404,a,427,a)]. given #103 (F,wt=7): 467 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(power_set(A)))))). [ur(404,a,430,a)]. given #104 (T,wt=5): 453 member(range_of(c4),power_set(c2)). [resolve(277,a,164,c),unit_del(a,166)]. given #105 (T,wt=6): 286 ilf_type(domain_of(c4),member_type(power_set(c3))). [resolve(201,a,171,b)]. given #106 (A,wt=17): 208 empty(A) | ordered_pair(f12(A,f17(A)),f13(A,f17(A))) = f17(A) | -ilf_type(A,binary_relation_type). [resolve(160,b,90,a)]. given #107 (F,wt=8): 472 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(power_set(A))))))). [ur(404,a,467,a)]. given #108 (F,wt=9): 388 -subset(power_set(ordered_pair(c3,domain_of(c4))),f8(identity_relation_of(A))). [ur(180,a,218,a,b,376,a)]. given #109 (T,wt=5): 486 member(domain_of(c4),power_set(c3)). [resolve(286,a,164,c),unit_del(a,166)]. given #110 (T,wt=6): 307 ilf_type(A,binary_relation_type) | -empty(identity_relation_of(A)). [resolve(195,a,159,a)]. given #111 (A,wt=18): 209 ordered_pair(f14(A,f17(A)),f15(A,f17(A))) = f17(A) | member(f16(A),A) | empty(A). [resolve(162,a,160,b)]. given #112 (F,wt=9): 390 -member(ordered_pair(c3,domain_of(c4)),f8(f8(identity_relation_of(A)))). [ur(167,b,376,a,c,361,a)]. given #113 (F,wt=9): 412 f8(identity_relation_of(A)) != power_set(ordered_pair(domain_of(c4),c3)). [ur(174,a,383,a)]. given #114 (T,wt=7): 212 empty(A) | ilf_type(f17(A),member_type(A)). [resolve(165,c,160,b),merge(c)]. given #115 (T,wt=6): 527 ilf_type(f17(power_set(A)),subset_type(A)). [resolve(212,b,172,b),unit_del(a,166)]. given #116 (A,wt=19): 210 ordered_pair(f14(A,f11(A)),f15(A,f11(A))) = f11(A) | member(f16(A),A) | ilf_type(A,binary_relation_type). [resolve(162,a,86,a)]. given #117 (F,wt=9): 428 -ilf_type(ordered_pair(domain_of(c4),c3),member_type(identity_relation_of(power_set(A)))). [ur(164,a,422,a,b,260,a)]. given #118 (F,wt=9): 429 -ilf_type(ordered_pair(c3,domain_of(c4)),member_type(identity_relation_of(power_set(A)))). [ur(164,a,422,a,b,259,a)]. given #119 (T,wt=7): 239 -member(A,identity_relation_of(c3)) | member(A,c4). [resolve(180,c,83,a)]. given #120 (T,wt=7): 242 ilf_type(domain_of(f1(A,B)),subset_type(B)). [resolve(183,a,156,a),rewrite(241(2))]. given #121 (A,wt=10): 213 empty(A) | ilf_type(f11(A),member_type(A)) | ilf_type(A,binary_relation_type). [resolve(165,c,86,a)]. given #122 (F,wt=9): 451 -member(ordered_pair(domain_of(c4),c3),f18(power_set(identity_relation_of(A)))). [ur(167,b,260,a,c,269,a)]. given #123 (F,wt=9): 452 -member(ordered_pair(c3,domain_of(c4)),f18(power_set(identity_relation_of(A)))). [ur(167,b,259,a,c,269,a)]. given #124 (T,wt=7): 244 ilf_type(range_of(f1(A,B)),subset_type(A)). [resolve(183,a,154,a),rewrite(243(2))]. given #125 (T,wt=7): 270 member(ordered_pair(A,A),identity_relation_of(power_set(A))). [resolve(218,a,111,a)]. given #126 (A,wt=10): 214 member(f17(A),B) | -member(A,power_set(B)) | empty(A). [resolve(167,a,160,b)]. given #127 (F,wt=9): 489 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(power_set(A)))))))). [ur(404,a,472,a)]. given #128 (F,wt=9): 496 f8(identity_relation_of(A)) != power_set(ordered_pair(c3,domain_of(c4))). [ur(174,a,388,a)]. given #129 (T,wt=7): 294 ilf_type(cross_product(A,B),relation_type(A,B)). [resolve(287,a,185,a)]. given #130 (T,wt=7): 325 empty(A) | ilf_type(f18(A),member_type(A)). [resolve(204,b,165,c),merge(b)]. given #131 (A,wt=11): 215 member(f11(A),B) | -member(A,power_set(B)) | ilf_type(A,binary_relation_type). [resolve(167,a,86,a)]. given #132 (F,wt=10): 320 -ilf_type(power_set(ordered_pair(c3,domain_of(c4))),member_type(power_set(identity_relation_of(A)))). [ur(164,a,166,a,b,276,a)]. given #133 (F,wt=9): 613 -ilf_type(power_set(ordered_pair(c3,domain_of(c4))),subset_type(identity_relation_of(A))). [ur(171,a,320,a)]. given #134 (T,wt=6): 604 ilf_type(f18(power_set(A)),subset_type(A)). [resolve(325,b,172,b),unit_del(a,166)]. given #135 (T,wt=7): 364 -member(A,f8(B)) | member(A,B). [resolve(361,a,167,c)]. given #136 (A,wt=8): 216 -member(A,f17(power_set(B))) | member(A,B). [resolve(167,c,160,b),unit_del(c,166)]. given #137 (F,wt=9): 635 -member(ordered_pair(domain_of(c4),c3),f17(power_set(identity_relation_of(A)))). [ur(216,b,260,a)]. given #138 (F,wt=9): 636 -member(ordered_pair(c3,domain_of(c4)),f17(power_set(identity_relation_of(A)))). [ur(216,b,259,a)]. given #139 (T,wt=7): 393 ilf_type(f10(power_set(A)),member_type(power_set(A))). [resolve(232,a,171,b)]. given #140 (T,wt=6): 651 member(f10(power_set(A)),power_set(A)). [resolve(393,a,164,c),unit_del(a,166)]. given #141 (A,wt=12): 217 -member(A,f11(power_set(B))) | member(A,B) | ilf_type(power_set(B),binary_relation_type). [resolve(167,c,86,a)]. given #142 (F,wt=9): 672 -member(ordered_pair(domain_of(c4),c3),f10(power_set(identity_relation_of(A)))). [ur(167,b,260,a,c,651,a)]. given #143 (F,wt=9): 673 -member(ordered_pair(c3,domain_of(c4)),f10(power_set(identity_relation_of(A)))). [ur(167,b,259,a,c,651,a)]. given #144 (T,wt=7): 394 ilf_type(f10(power_set(cross_product(A,B))),binary_relation_type). [resolve(232,a,96,a)]. given #145 (T,wt=7): 395 ilf_type(c4,member_type(power_set(cross_product(c3,c2)))). [resolve(246,a,171,b)]. given #146 (A,wt=14): 219 member(power_set(A),power_set(B)) | -member(C,f9(power_set(A),B)) | member(C,A). [resolve(169,b,167,c)]. given #147 (F,wt=10): 341 -subset(power_set(power_set(ordered_pair(domain_of(c4),c3))),power_set(identity_relation_of(A))). [ur(180,a,218,a,b,282,a)]. given #148 (F,wt=10): 345 -ilf_type(power_set(ordered_pair(domain_of(c4),c3)),member_type(power_set(identity_relation_of(A)))). [ur(164,a,166,a,b,282,a)]. given #149 (T,wt=6): 698 member(c4,power_set(cross_product(c3,c2))). [resolve(395,a,164,c),unit_del(a,166)]. given #150 (T,wt=7): 438 ilf_type(f18(power_set(A)),member_type(power_set(A))). [resolve(269,a,165,c),unit_del(a,166)]. given #151 (A,wt=13): 220 member(A,power_set(B)) | member(f9(A,B),C) | -member(A,power_set(C)). [resolve(169,b,167,a)]. given #152 (F,wt=9): 706 -ilf_type(power_set(ordered_pair(domain_of(c4),c3)),subset_type(identity_relation_of(A))). [ur(171,a,345,a)]. given #153 (F,wt=10): 360 power_set(power_set(ordered_pair(c3,domain_of(c4)))) != power_set(identity_relation_of(A)). [ur(174,a,316,a),flip(a)]. given #154 (T,wt=7): 479 -member(A,range_of(c4)) | member(A,c2). [resolve(453,a,167,c)]. given #155 (T,wt=7): 499 -member(A,domain_of(c4)) | member(A,c3). [resolve(486,a,167,c)]. given #156 (A,wt=12): 221 member(A,power_set(B)) | empty(A) | ilf_type(f9(A,B),member_type(A)). [resolve(169,b,165,c)]. given #157 (F,wt=10): 371 -member(power_set(ordered_pair(domain_of(c4),c3)),f8(power_set(identity_relation_of(A)))). [ur(167,b,282,a,c,361,a)]. given #158 (F,wt=10): 373 -member(power_set(ordered_pair(c3,domain_of(c4))),f8(power_set(identity_relation_of(A)))). [ur(167,b,276,a,c,361,a)]. given #159 (T,wt=7): 530 ilf_type(f17(power_set(A)),member_type(power_set(A))). [resolve(527,a,171,b)]. given #160 (T,wt=6): 769 member(f17(power_set(A)),power_set(A)). [resolve(530,a,164,c),unit_del(a,166)]. given #161 (A,wt=23): 222 member(A,power_set(B)) | ordered_pair(f14(A,f9(A,B)),f15(A,f9(A,B))) = f9(A,B) | member(f16(A),A). [resolve(169,b,162,a)]. given #162 (F,wt=10): 386 -member(power_set(ordered_pair(domain_of(c4),c3)),power_set(f8(identity_relation_of(A)))). [ur(167,a,218,a,b,375,a)]. given #163 (F,wt=10): 391 -member(power_set(ordered_pair(c3,domain_of(c4))),power_set(f8(identity_relation_of(A)))). [ur(167,a,218,a,b,376,a)]. given #164 (T,wt=7): 531 ilf_type(f17(power_set(cross_product(A,B))),binary_relation_type). [resolve(527,a,96,a)]. given #165 (T,wt=7): 537 member(f16(A),A) | ilf_type(A,binary_relation_type). [resolve(210,a,88,a(flip)),merge(c)]. given #166 (A,wt=8): 224 member(A,power_set(B)) | member(f18(A),A). [resolve(169,b,158,a)]. given #167 (F,wt=10): 414 -subset(power_set(ordered_pair(domain_of(c4),c3)),f8(f8(identity_relation_of(A)))). [ur(180,a,218,a,b,385,a)]. given #168 (F,wt=10): 416 -member(ordered_pair(domain_of(c4),c3),f8(f8(f8(identity_relation_of(A))))). [ur(167,b,385,a,c,361,a)]. given #169 (T,wt=7): 601 ilf_type(domain_of(cross_product(A,B)),subset_type(A)). [resolve(294,a,156,a),rewrite(600(2))]. given #170 (T,wt=7): 603 ilf_type(range_of(cross_product(A,B)),subset_type(B)). [resolve(294,a,154,a),rewrite(602(2))]. given #171 (A,wt=14): 225 member(A,power_set(B)) | member(ordered_pair(f9(A,B),f9(A,B)),identity_relation_of(A)). [resolve(169,b,111,a)]. given #172 (F,wt=10): 433 -ilf_type(ordered_pair(domain_of(c4),c3),member_type(identity_relation_of(identity_relation_of(power_set(A))))). [ur(164,a,427,a,b,260,a)]. given #173 (F,wt=10): 434 -ilf_type(ordered_pair(c3,domain_of(c4)),member_type(identity_relation_of(identity_relation_of(power_set(A))))). [ur(164,a,427,a,b,259,a)]. given #174 (T,wt=7): 616 ilf_type(f18(power_set(cross_product(A,B))),binary_relation_type). [resolve(604,a,96,a)]. given #175 (T,wt=7): 891 member(A,power_set(B)) | -empty(identity_relation_of(A)). [resolve(225,b,159,a)]. given #176 (A,wt=25): 226 member(A,power_set(B)) | -ilf_type(A,subset_type(cross_product(C,D))) | ordered_pair(f12(A,f9(A,B)),f13(A,f9(A,B))) = f9(A,B). [resolve(169,b,98,b)]. given #177 (F,wt=10): 445 -member(ordered_pair(c3,domain_of(c4)),f18(power_set(f8(identity_relation_of(A))))). [ur(167,b,376,a,c,269,a)]. given #178 (F,wt=10): 446 -member(ordered_pair(domain_of(c4),c3),f18(power_set(f8(identity_relation_of(A))))). [ur(167,b,375,a,c,269,a)]. given #179 (T,wt=8): 245 ilf_type(f1(A,B),subset_type(cross_product(B,A))). [resolve(184,a,183,a)]. given #180 (T,wt=5): 930 ilf_type(f1(A,B),binary_relation_type). [resolve(245,a,96,a)]. given #181 (A,wt=23): 227 member(A,power_set(B)) | ordered_pair(f12(A,f9(A,B)),f13(A,f9(A,B))) = f9(A,B) | member(f11(A),A). [resolve(169,b,92,a)]. given #182 (F,wt=10): 520 -subset(power_set(ordered_pair(c3,domain_of(c4))),f8(f8(identity_relation_of(A)))). [ur(180,a,218,a,b,390,a)]. given #183 (F,wt=10): 522 -member(ordered_pair(c3,domain_of(c4)),f8(f8(f8(identity_relation_of(A))))). [ur(167,b,390,a,c,361,a)]. given #184 (T,wt=8): 247 ilf_type(f8(cross_product(A,B)),relation_type(A,B)). [resolve(185,a,170,a)]. given #185 (T,wt=8): 257 -subset(c4,identity_relation_of(c3)) | identity_relation_of(c3) = c4. [resolve(192,a,83,a),flip(b)]. given #186 (A,wt=22): 228 member(A,power_set(B)) | ordered_pair(f12(A,f9(A,B)),f13(A,f9(A,B))) = f9(A,B) | -ilf_type(A,binary_relation_type). [resolve(169,b,90,a)]. given #187 (F,wt=10): 550 -subset(power_set(ordered_pair(domain_of(c4),c3)),f18(power_set(identity_relation_of(A)))). [ur(180,a,218,a,b,451,a)]. given #188 (F,wt=10): 552 -member(ordered_pair(domain_of(c4),c3),f8(f18(power_set(identity_relation_of(A))))). [ur(167,b,451,a,c,361,a)]. given #189 (T,wt=8): 266 member(A,B) | -member(power_set(A),power_set(B)). [resolve(218,a,167,a)]. given #190 (T,wt=8): 323 -member(A,f18(power_set(B))) | member(A,B). [resolve(204,b,167,c),unit_del(a,166)]. given #191 (A,wt=15): 229 member(power_set(power_set(A)),power_set(A)) | -member(power_set(power_set(A)),f9(power_set(power_set(A)),A)). [factor(219,a,c)]. given #192 (F,wt=10): 556 -subset(power_set(ordered_pair(c3,domain_of(c4))),f18(power_set(identity_relation_of(A)))). [ur(180,a,218,a,b,452,a)]. given #193 (F,wt=10): 558 -member(ordered_pair(c3,domain_of(c4)),f8(f18(power_set(identity_relation_of(A))))). [ur(167,b,452,a,c,361,a)]. given #194 (T,wt=8): 333 -member(A,f10(power_set(B))) | member(A,B). [resolve(211,b,167,c),unit_del(a,166)]. given #195 (T,wt=8): 405 empty(A) | member(f18(identity_relation_of(A)),identity_relation_of(A)). [resolve(205,b,158,a)]. given #196 (A,wt=14): 233 member(f9(A,B),C) | -member(f3(A,C),C) | member(A,power_set(B)). [resolve(178,a,169,b)]. given #197 (F,wt=10): 577 -subset(identity_relation_of(power_set(ordered_pair(domain_of(c4),c3))),identity_relation_of(identity_relation_of(A))). [ur(180,a,270,a,b,279,a)]. given #198 (F,wt=10): 578 -subset(identity_relation_of(power_set(ordered_pair(c3,domain_of(c4)))),identity_relation_of(identity_relation_of(A))). [ur(180,a,270,a,b,261,a)]. given #199 (T,wt=7): 1000 empty(c3) | member(f18(identity_relation_of(c3)),c4). [resolve(405,b,239,a)]. given #200 (T,wt=4): 1024 empty(c3) | -empty(c4). [resolve(1000,b,159,a)]. given #201 (A,wt=11): 234 member(f17(A),B) | -member(f3(A,B),B) | empty(A). [resolve(178,a,160,b)]. given #202 (F,wt=10): 593 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(power_set(A))))))))). [ur(404,a,489,a)]. given #203 (F,wt=10): 629 -member(ordered_pair(c3,domain_of(c4)),f17(power_set(f8(identity_relation_of(A))))). [ur(216,b,376,a)]. given #204 (T,wt=6): 1025 empty(c3) | member(f18(c4),c4). [resolve(1000,b,158,a)]. given #205 (T,wt=8): 538 member(f10(identity_relation_of(c3)),c4) | empty(identity_relation_of(c3)). [resolve(239,a,211,b)]. given #206 (A,wt=12): 235 member(f11(A),B) | -member(f3(A,B),B) | ilf_type(A,binary_relation_type). [resolve(178,a,86,a)]. given #207 (F,wt=10): 630 -member(ordered_pair(domain_of(c4),c3),f17(power_set(f8(identity_relation_of(A))))). [ur(216,b,375,a)]. given #208 (F,wt=10): 637 -member(ordered_pair(domain_of(c4),c3),f8(f17(power_set(identity_relation_of(A))))). [ur(364,b,635,a)]. given #209 (T,wt=5): 1058 empty(identity_relation_of(c3)) | -empty(c4). [resolve(538,a,159,a)]. given #210 (T,wt=7): 1059 empty(identity_relation_of(c3)) | member(f18(c4),c4). [resolve(538,a,158,a)]. given #211 (A,wt=14): 236 member(f9(A,B),C) | member(f3(A,C),A) | member(A,power_set(B)). [resolve(179,a,169,b)]. given #212 (F,wt=10): 640 -subset(power_set(ordered_pair(domain_of(c4),c3)),f17(power_set(identity_relation_of(A)))). [ur(180,a,218,a,b,635,a)]. given #213 (F,wt=10): 644 -member(ordered_pair(c3,domain_of(c4)),f8(f17(power_set(identity_relation_of(A))))). [ur(364,b,636,a)]. given #214 (T,wt=8): 540 member(f18(identity_relation_of(c3)),c4) | empty(identity_relation_of(c3)). [resolve(239,a,204,b)]. given #215 (T,wt=8): 543 member(f17(identity_relation_of(c3)),c4) | empty(identity_relation_of(c3)). [resolve(239,a,160,b)]. given #216 (A,wt=11): 237 member(f17(A),B) | member(f3(A,B),A) | empty(A). [resolve(179,a,160,b)]. given #217 (F,wt=10): 647 -subset(power_set(ordered_pair(c3,domain_of(c4))),f17(power_set(identity_relation_of(A)))). [ur(180,a,218,a,b,636,a)]. given #218 (F,wt=10): 666 -member(ordered_pair(c3,domain_of(c4)),f10(power_set(f8(identity_relation_of(A))))). [ur(167,b,376,a,c,651,a)]. given #219 (T,wt=8): 546 ilf_type(domain_of(f1(A,B)),member_type(power_set(B))). [resolve(242,a,171,b)]. given #220 (T,wt=7): 1233 member(domain_of(f1(A,B)),power_set(B)). [resolve(546,a,164,c),unit_del(a,166)]. given #221 (A,wt=12): 238 member(f11(A),B) | member(f3(A,B),A) | ilf_type(A,binary_relation_type). [resolve(179,a,86,a)]. given #222 (F,wt=10): 667 -member(ordered_pair(domain_of(c4),c3),f10(power_set(f8(identity_relation_of(A))))). [ur(167,b,375,a,c,651,a)]. given #223 (F,wt=10): 678 -member(ordered_pair(domain_of(c4),c3),f8(f10(power_set(identity_relation_of(A))))). [ur(364,b,672,a)]. given #224 (T,wt=8): 547 ilf_type(domain_of(f1(A,cross_product(B,C))),binary_relation_type). [resolve(242,a,96,a)]. given #225 (T,wt=8): 563 ilf_type(range_of(f1(A,B)),member_type(power_set(A))). [resolve(244,a,171,b)]. given #226 (A,wt=11): 240 member(f2(A,B),A) | -member(C,A) | member(C,B). [resolve(182,a,180,c)]. given #227 (F,wt=10): 681 -subset(power_set(ordered_pair(domain_of(c4),c3)),f10(power_set(identity_relation_of(A)))). [ur(180,a,218,a,b,672,a)]. given #228 (F,wt=10): 686 -member(ordered_pair(c3,domain_of(c4)),f8(f10(power_set(identity_relation_of(A))))). [ur(364,b,673,a)]. given #229 (T,wt=7): 1343 member(range_of(f1(A,B)),power_set(A)). [resolve(563,a,164,c),unit_del(a,166)]. given #230 (T,wt=8): 564 ilf_type(range_of(f1(cross_product(A,B),C)),binary_relation_type). [resolve(244,a,96,a)]. given #231 (A,wt=11): 241 domain(A,B,f1(B,A)) = domain_of(f1(B,A)). [resolve(183,a,157,a)]. given #232 (F,wt=10): 689 -subset(power_set(ordered_pair(c3,domain_of(c4))),f10(power_set(identity_relation_of(A)))). [ur(180,a,218,a,b,673,a)]. given #233 (F,wt=10): 705 power_set(power_set(ordered_pair(domain_of(c4),c3))) != power_set(identity_relation_of(A)). [ur(174,a,341,a),flip(a)]. given #234 (T,wt=8): 570 ilf_type(ordered_pair(A,A),member_type(identity_relation_of(power_set(A)))). [resolve(270,a,165,c),unit_del(a,422)]. given #235 (T,wt=8): 572 member(f18(identity_relation_of(power_set(A))),identity_relation_of(power_set(A))). [resolve(270,a,158,a)]. given #236 (A,wt=11): 243 range(A,B,f1(B,A)) = range_of(f1(B,A)). [resolve(183,a,155,a)]. given #237 (F,wt=10): 866 f8(f8(identity_relation_of(A))) != power_set(ordered_pair(domain_of(c4),c3)). [ur(174,a,414,a)]. given #238 (F,wt=10): 951 f8(f8(identity_relation_of(A))) != power_set(ordered_pair(c3,domain_of(c4))). [ur(174,a,520,a)]. given #239 (T,wt=8): 585 member(f17(domain_of(c4)),c3) | empty(domain_of(c4)). [resolve(214,b,486,a)]. given #240 (T,wt=5): 1469 empty(domain_of(c4)) | -empty(c3). [resolve(585,a,159,a)]. given #241 (A,wt=18): 248 -ilf_type(A,binary_relation_type) | subset(A,identity_relation_of(B)) | member(ordered_pair(f4(A,identity_relation_of(B)),f5(A,identity_relation_of(B))),A). [resolve(186,a,30,b)]. given #242 (F,wt=10): 969 f18(power_set(identity_relation_of(A))) != power_set(ordered_pair(domain_of(c4),c3)). [ur(174,a,550,a)]. given #243 (F,wt=10): 986 f18(power_set(identity_relation_of(A))) != power_set(ordered_pair(c3,domain_of(c4))). [ur(174,a,556,a)]. given #244 (T,wt=7): 1470 empty(domain_of(c4)) | member(f18(c3),c3). [resolve(585,a,158,a)]. given #245 (T,wt=8): 586 member(f17(range_of(c4)),c2) | empty(range_of(c4)). [resolve(214,b,453,a)]. given #246 (A,wt=19): 249 -ilf_type(A,binary_relation_type) | subset(identity_relation_of(B),A) | member(ordered_pair(f4(identity_relation_of(B),A),f5(identity_relation_of(B),A)),identity_relation_of(B)). [resolve(186,a,30,a)]. given #247 (F,wt=10): 1013 identity_relation_of(power_set(ordered_pair(domain_of(c4),c3))) != identity_relation_of(identity_relation_of(A)). [ur(174,a,577,a),flip(a)]. given #248 (F,wt=10): 1017 identity_relation_of(power_set(ordered_pair(c3,domain_of(c4)))) != identity_relation_of(identity_relation_of(A)). [ur(174,a,578,a),flip(a)]. given #249 (T,wt=5): 1504 empty(range_of(c4)) | -empty(c2). [resolve(586,a,159,a)]. given #250 (T,wt=7): 1505 empty(range_of(c4)) | member(f18(c2),c2). [resolve(586,a,158,a)]. given #251 (A,wt=18): 250 -ilf_type(A,relation_type(B,C)) | subset(D,range(B,C,A)) | member(f2(identity_relation_of(D),A),identity_relation_of(D)). [resolve(190,b,182,a)]. given #252 (F,wt=10): 1147 f17(power_set(identity_relation_of(A))) != power_set(ordered_pair(domain_of(c4),c3)). [ur(174,a,640,a)]. given #253 (F,wt=10): 1224 f17(power_set(identity_relation_of(A))) != power_set(ordered_pair(c3,domain_of(c4))). [ur(174,a,647,a)]. given #254 (T,wt=8): 587 member(f17(f8(A)),A) | empty(f8(A)). [resolve(214,b,361,a)]. given #255 (T,wt=5): 1559 empty(f8(A)) | -empty(A). [resolve(587,a,159,a)]. given #256 (A,wt=13): 251 -ilf_type(identity_relation_of(A),relation_type(B,C)) | subset(A,range(B,C,identity_relation_of(A))). [resolve(190,b,131,a)]. given #257 (F,wt=10): 1275 -member(ordered_pair(domain_of(c4),c3),domain_of(f1(A,identity_relation_of(B)))). [ur(167,b,260,a,c,1233,a)]. given #258 (F,wt=10): 1276 -member(ordered_pair(c3,domain_of(c4)),domain_of(f1(A,identity_relation_of(B)))). [ur(167,b,259,a,c,1233,a)]. given #259 (T,wt=7): 1560 empty(f8(A)) | member(f18(A),A). [resolve(587,a,158,a)]. given #260 (T,wt=8): 617 member(f10(f8(A)),A) | empty(f8(A)). [resolve(364,a,211,b)]. given #261 (A,wt=11): 252 -ilf_type(c4,relation_type(A,B)) | subset(c3,range(A,B,c4)). [resolve(190,b,83,a)]. given #262 (F,wt=10): 1383 f10(power_set(identity_relation_of(A))) != power_set(ordered_pair(domain_of(c4),c3)). [ur(174,a,681,a)]. given #263 (F,wt=10): 1438 -member(ordered_pair(domain_of(c4),c3),range_of(f1(identity_relation_of(A),B))). [ur(167,b,260,a,c,1343,a)]. given #264 (T,wt=4): 1626 subset(c3,range_of(c4)). [resolve(252,a,82,a),rewrite(197(5))]. given #265 (T,wt=7): 1640 -member(A,c3) | member(A,range_of(c4)). [resolve(1626,a,180,c)]. given #266 (A,wt=18): 253 -ilf_type(A,relation_type(B,C)) | subset(D,domain(B,C,A)) | member(f2(identity_relation_of(D),A),identity_relation_of(D)). [resolve(191,b,182,a)]. given #267 (F,wt=10): 1439 -member(ordered_pair(c3,domain_of(c4)),range_of(f1(identity_relation_of(A),B))). [ur(167,b,259,a,c,1343,a)]. given #268 (F,wt=10): 1446 f10(power_set(identity_relation_of(A))) != power_set(ordered_pair(c3,domain_of(c4))). [ur(174,a,689,a)]. given #269 (T,wt=7): 1654 member(f10(c3),range_of(c4)) | empty(c3). [resolve(1640,a,211,b)]. given #270 (T,wt=5): 1683 empty(c3) | -empty(range_of(c4)). [resolve(1654,a,159,a)]. given #271 (A,wt=13): 254 -ilf_type(identity_relation_of(A),relation_type(B,C)) | subset(A,domain(B,C,identity_relation_of(A))). [resolve(191,b,131,a)]. given #272 (F,wt=11): 275 -member(f3(power_set(ordered_pair(c3,domain_of(c4))),identity_relation_of(A)),identity_relation_of(A)). [ur(178,a,218,a,b,259,a)]. given #273 (F,wt=11): 281 -member(f3(power_set(ordered_pair(domain_of(c4),c3)),identity_relation_of(A)),identity_relation_of(A)). [ur(178,a,218,a,b,260,a)]. given #274 (T,wt=6): 1676 empty(c3) | member(f10(c3),c2). [resolve(1654,a,479,a)]. given #275 (T,wt=4): 1729 empty(c3) | -empty(c2). [resolve(1676,b,159,a)]. given #276 (A,wt=11): 255 -ilf_type(c4,relation_type(A,B)) | subset(c3,domain(A,B,c4)). [resolve(191,b,83,a)]. given #277 (F,wt=11): 284 -member(f2(power_set(ordered_pair(c3,domain_of(c4))),identity_relation_of(A)),identity_relation_of(A)). [ur(181,a,274,a)]. given #278 (F,wt=11): 290 -member(f2(power_set(ordered_pair(domain_of(c4),c3)),identity_relation_of(A)),identity_relation_of(A)). [ur(181,a,280,a)]. given #279 (T,wt=4): 1735 subset(c3,domain_of(c4)). [resolve(255,a,82,a),rewrite(200(5))]. given #280 (T,wt=6): 1730 empty(c3) | member(f18(c2),c2). [resolve(1676,b,158,a)]. given #281 (A,wt=11): 256 -subset(A,B) | A = B | member(f2(B,A),B). [resolve(192,a,182,a)]. given #282 (F,wt=4): 1770 -subset(domain_of(c4),c3). [resolve(1735,a,192,b),flip(b),unit_del(b,202)]. given #283 (F,wt=6): 1784 -member(f2(domain_of(c4),c3),c3). [ur(181,a,1770,a)]. ============================== PROOF ================================= % Proof 1 at 0.16 (+ 0.00) seconds. % Length of proof is 39. % Level of proof is 8. % Maximum clause weight is 24. % Given clauses 283. 11 -ilf_type(A,set_type) | -ilf_type(B,set_type) | -subset(A,B) | -subset(B,A) | B = A. [assumption]. 12 -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | -ilf_type(D,relation_type(A,B)) | -subset(identity_relation_of(C),D) | subset(C,domain(A,B,D)). [assumption]. 22 -ilf_type(A,set_type) | -ilf_type(B,set_type) | subset(A,B) | member(f2(A,B),A). [assumption]. 23 -ilf_type(A,set_type) | -ilf_type(B,set_type) | subset(A,B) | -member(f2(A,B),B). [assumption]. 45 -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]. 52 -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]. 53 -ilf_type(A,set_type) | -empty(power_set(A)). [assumption]. 56 -ilf_type(A,set_type) | empty(B) | -ilf_type(B,set_type) | member(A,B) | -ilf_type(A,member_type(B)). [assumption]. 75 -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,relation_type(A,B)) | domain_of(C) = domain(A,B,C). [assumption]. 76 -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,relation_type(A,B)) | domain(A,B,C) = domain_of(C). [copy(75),flip(d)]. 77 -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]. 81 ilf_type(A,set_type). [assumption]. 82 ilf_type(c4,relation_type(c3,c2)). [assumption]. 83 subset(identity_relation_of(c3),c4). [assumption]. 84 domain(c3,c2,c4) != c3. [assumption]. 156 -ilf_type(A,relation_type(B,C)) | ilf_type(domain(B,C,A),subset_type(B)). [back_unit_del(77),unit_del(a,81),unit_del(b,81)]. 157 -ilf_type(A,relation_type(B,C)) | domain(B,C,A) = domain_of(A). [back_unit_del(76),unit_del(a,81),unit_del(b,81)]. 164 empty(A) | member(B,A) | -ilf_type(B,member_type(A)). [back_unit_del(56),unit_del(a,81),unit_del(c,81)]. 166 -empty(power_set(A)). [back_unit_del(53),unit_del(a,81)]. 167 -member(A,B) | member(A,C) | -member(B,power_set(C)). [back_unit_del(52),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. 171 ilf_type(A,member_type(power_set(B))) | -ilf_type(A,subset_type(B)). [back_unit_del(45),unit_del(a,81),unit_del(b,81)]. 181 subset(A,B) | -member(f2(A,B),B). [back_unit_del(23),unit_del(a,81),unit_del(b,81)]. 182 subset(A,B) | member(f2(A,B),A). [back_unit_del(22),unit_del(a,81),unit_del(b,81)]. 191 -ilf_type(A,relation_type(B,C)) | -subset(identity_relation_of(D),A) | subset(D,domain(B,C,A)). [back_unit_del(12),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. 192 -subset(A,B) | -subset(B,A) | B = A. [back_unit_del(11),unit_del(a,81),unit_del(b,81)]. 199 ilf_type(domain(c3,c2,c4),subset_type(c3)). [resolve(156,a,82,a)]. 200 domain(c3,c2,c4) = domain_of(c4). [resolve(157,a,82,a)]. 201 ilf_type(domain_of(c4),subset_type(c3)). [back_rewrite(199),rewrite(200(4))]. 202 domain_of(c4) != c3. [back_rewrite(84),rewrite(200(4))]. 255 -ilf_type(c4,relation_type(A,B)) | subset(c3,domain(A,B,c4)). [resolve(191,b,83,a)]. 256 -subset(A,B) | A = B | member(f2(B,A),B). [resolve(192,a,182,a)]. 286 ilf_type(domain_of(c4),member_type(power_set(c3))). [resolve(201,a,171,b)]. 486 member(domain_of(c4),power_set(c3)). [resolve(286,a,164,c),unit_del(a,166)]. 499 -member(A,domain_of(c4)) | member(A,c3). [resolve(486,a,167,c)]. 1735 subset(c3,domain_of(c4)). [resolve(255,a,82,a),rewrite(200(5))]. 1770 -subset(domain_of(c4),c3). [resolve(1735,a,192,b),flip(b),unit_del(b,202)]. 1781 member(f2(domain_of(c4),c3),domain_of(c4)). [resolve(256,a,1735,a),flip(a),unit_del(a,202)]. 1784 -member(f2(domain_of(c4),c3),c3). [ur(181,a,1770,a)]. 1785 $F. [ur(499,b,1784,a),unit_del(a,1781)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=283. Generated=2495. Kept=1760. proofs=1. Usable=281. Sos=1333. Demods=10. Limbo=0, Disabled=237. Hints=0. Weight_deleted=4. Literals_deleted=0. Forward_subsumed=730. Back_subsumed=103. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=10 (0 lex), Back_demodulated=3. Back_unit_deleted=40. Demod_attempts=23804. Demod_rewrites=47. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=2381. Nonunit_bsub_feature_tests=1707. Megabytes=2.56. User_CPU=0.16, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 3795 exit (max_proofs) Wed Nov 22 11:23:45 2006 ============================== continuing FOF reduction multisearch == Subproblem 2 of 2 (negated): ((all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | - subset(B,C) | - subset(C,B) | =(C,B))))) & (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,relation_type(B,C)) | - subset(identity_relation_of(D),E) | subset(D,domain(B,C,E)))))))))) & (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,relation_type(B,C)) | - subset(identity_relation_of(D),E) | subset(D,range(B,C,E)))))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | - member(C,B) | (all D (- ilf_type(D,set_type) | member(ordered_pair(C,D),identity_relation_of(B)) | - =(D,C))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | member(C,B) | (all D (- ilf_type(D,set_type) | - member(ordered_pair(C,D),identity_relation_of(B)))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,set_type) | =(D,C) | - member(ordered_pair(C,D),identity_relation_of(B)))))))) & (all B (- ilf_type(B,set_type) | ilf_type(identity_relation_of(B),binary_relation_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) | 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,binary_relation_type) | (all C (- ilf_type(C,binary_relation_type) | subset(B,C) | (exists D (ilf_type(D,set_type) & (exists E (ilf_type(E,set_type) & member(ordered_pair(D,E),B) & - member(ordered_pair(D,E),C))))))))) & (all B (- ilf_type(B,binary_relation_type) | (all C (- ilf_type(C,binary_relation_type) | (all D (- ilf_type(D,set_type) | (all E (- ilf_type(E,set_type) | - member(ordered_pair(D,E),B) | member(ordered_pair(D,E),C))))) | - subset(B,C))))) & (all B (- ilf_type(B,binary_relation_type) | (all C (- ilf_type(C,binary_relation_type) | (all D (- ilf_type(D,set_type) | (all E (- ilf_type(E,set_type) | - member(ordered_pair(D,E),B) | member(ordered_pair(D,E),C))))) | (exists D (ilf_type(D,set_type) & (exists E (ilf_type(E,set_type) & member(ordered_pair(D,E),B) & - member(ordered_pair(D,E),C))))))))) & (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) | (all C (- ilf_type(C,set_type) | ilf_type(cross_product(B,C),set_type))))) & (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) | ilf_type(ordered_pair(B,C),set_type))))) & (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) | subset(B,B))) & (all B (- ilf_type(B,binary_relation_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_of(D),domain(B,C,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_of(D),range(B,C,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(C,B)) & subset(identity_relation_of(C),D) & - subset(C,range(C,B,D))))))))). Child search process 3796 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). -ilf_type(A,set_type) | -ilf_type(B,set_type) | -subset(A,B) | -subset(B,A) | B = A. [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | -ilf_type(D,relation_type(A,B)) | -subset(identity_relation_of(C),D) | subset(C,domain(A,B,D)). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | -ilf_type(D,relation_type(A,B)) | -subset(identity_relation_of(C),D) | subset(C,range(A,B,D)). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | -ilf_type(C,set_type) | member(ordered_pair(B,C),identity_relation_of(A)) | C != B. [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | member(B,A) | -ilf_type(C,set_type) | -member(ordered_pair(B,C),identity_relation_of(A)). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | C = B | -member(ordered_pair(B,C),identity_relation_of(A)). [assumption]. -ilf_type(A,set_type) | ilf_type(identity_relation_of(A),binary_relation_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(f1(A,B),relation_type(B,A)). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | subset(A,B) | ilf_type(f2(A,B),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | subset(A,B) | member(f2(A,B),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | subset(A,B) | -member(f2(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(f3(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(f3(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(f3(A,B),B). [assumption]. -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | subset(A,B) | ilf_type(f4(A,B),set_type). [assumption]. -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | subset(A,B) | ilf_type(f5(A,B),set_type). [assumption]. -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | subset(A,B) | member(ordered_pair(f4(A,B),f5(A,B)),A). [assumption]. -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | subset(A,B) | -member(ordered_pair(f4(A,B),f5(A,B)),B). [assumption]. -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | -ilf_type(C,set_type) | -ilf_type(D,set_type) | -member(ordered_pair(C,D),A) | member(ordered_pair(C,D),B) | -subset(A,B). [assumption]. -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | -ilf_type(C,set_type) | -ilf_type(D,set_type) | -member(ordered_pair(C,D),A) | member(ordered_pair(C,D),B) | ilf_type(f6(A,B),set_type). [assumption]. -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | -ilf_type(C,set_type) | -ilf_type(D,set_type) | -member(ordered_pair(C,D),A) | member(ordered_pair(C,D),B) | ilf_type(f7(A,B),set_type). [assumption]. -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | -ilf_type(C,set_type) | -ilf_type(D,set_type) | -member(ordered_pair(C,D),A) | member(ordered_pair(C,D),B) | member(ordered_pair(f6(A,B),f7(A,B)),A). [assumption]. -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | -ilf_type(C,set_type) | -ilf_type(D,set_type) | -member(ordered_pair(C,D),A) | member(ordered_pair(C,D),B) | -member(ordered_pair(f6(A,B),f7(A,B)),B). [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(B,set_type) | ilf_type(cross_product(A,B),set_type). [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(ordered_pair(A,B),set_type). [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(f8(A),subset_type(A)). [assumption]. -ilf_type(A,set_type) | subset(A,A). [assumption]. -ilf_type(A,binary_relation_type) | subset(A,A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | member(A,power_set(B)) | ilf_type(f9(A,B),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | member(A,power_set(B)) | member(f9(A,B),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | member(A,power_set(B)) | -member(f9(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(f10(A),member_type(A)). [assumption]. -ilf_type(A,set_type) | relation_like(A) | ilf_type(f11(A),set_type). [assumption]. -ilf_type(A,set_type) | relation_like(A) | member(f11(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) != f11(A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f12(A,B),set_type) | -relation_like(A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f13(A,B),set_type) | -relation_like(A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ordered_pair(f12(A,B),f13(A,B)) = B | -relation_like(A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f14(A,B),set_type) | ilf_type(f16(A),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f14(A,B),set_type) | member(f16(A),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f14(A,B),set_type) | -ilf_type(C,set_type) | -ilf_type(D,set_type) | ordered_pair(C,D) != f16(A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f15(A,B),set_type) | ilf_type(f16(A),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f15(A,B),set_type) | member(f16(A),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f15(A,B),set_type) | -ilf_type(C,set_type) | -ilf_type(D,set_type) | ordered_pair(C,D) != f16(A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ordered_pair(f14(A,B),f15(A,B)) = B | ilf_type(f16(A),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ordered_pair(f14(A,B),f15(A,B)) = B | member(f16(A),A). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ordered_pair(f14(A,B),f15(A,B)) = B | -ilf_type(C,set_type) | -ilf_type(D,set_type) | ordered_pair(C,D) != f16(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(f17(A),set_type). [assumption]. -ilf_type(A,set_type) | empty(A) | member(f17(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(f18(A),set_type). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | member(f18(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_of(C) = domain(A,B,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_of(C) = range(A,B,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(c3,c2)). [assumption]. subset(identity_relation_of(c3),c4). [assumption]. -subset(c3,range(c3,c2,c4)). [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(f11(A),set_type). [assumption]. 4 -ilf_type(A,set_type) | relation_like(A) | member(f11(A),A). [assumption]. Derived: -ilf_type(A,set_type) | member(f11(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) != f11(A). [assumption]. Derived: -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,set_type) | ordered_pair(B,C) != f11(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(f12(A,B),set_type) | -relation_like(A). [assumption]. 7 -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ilf_type(f13(A,B),set_type) | -relation_like(A). [assumption]. 8 -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ordered_pair(f12(A,B),f13(A,B)) = B | -relation_like(A). [assumption]. Derived: -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ordered_pair(f12(A,B),f13(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(f12(A,B),f13(A,B)) = B | -ilf_type(A,set_type) | member(f11(A),A). [resolve(8,e,4,b)]. Derived: -ilf_type(A,set_type) | -ilf_type(B,set_type) | -member(B,A) | ordered_pair(f12(A,B),f13(A,B)) = B | -ilf_type(A,set_type) | -ilf_type(C,set_type) | -ilf_type(D,set_type) | ordered_pair(C,D) != f11(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(f12(C,D),f13(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(f12(A,B),f13(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, cross_product, f1, f2, f3, f4, f5, f6, f7, f9, f12, f13, f14, f15, subset_type, identity_relation_of, power_set, member_type, domain_of, range_of, f8, f10, f11, f16, f17, f18, 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) % set(neg_ur_resolution). % (non-Horn, less than 100 clauses) Auto_process settings: % set(factor). % (non-Horn) % set(back_unit_deletion). % (non-Horn) % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 30 -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | subset(A,B) | member(ordered_pair(f4(A,B),f5(A,B)),A). [assumption]. 31 -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | subset(A,B) | -member(ordered_pair(f4(A,B),f5(A,B)),B). [assumption]. 43 ilf_type(c1,binary_relation_type). [assumption]. 81 ilf_type(A,set_type). [assumption]. 82 ilf_type(c4,relation_type(c3,c2)). [assumption]. 83 subset(identity_relation_of(c3),c4). [assumption]. 84 -subset(c3,range(c3,c2,c4)). [assumption]. 86 member(f11(A),A) | ilf_type(A,binary_relation_type). [copy(85),merge(c),unit_del(a,81)]. 88 f11(A) != ordered_pair(B,C) | ilf_type(A,binary_relation_type). [copy(87),flip(d),merge(e),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. 90 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | -ilf_type(B,binary_relation_type). [copy(89),merge(e),unit_del(a,81),unit_del(b,81)]. 92 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | member(f11(B),B). [copy(91),merge(e),unit_del(a,81),unit_del(b,81)]. 94 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | f11(B) != ordered_pair(C,D). [copy(93),flip(h),merge(e),unit_del(a,81),unit_del(b,81),unit_del(e,81),unit_del(f,81)]. 96 -ilf_type(A,subset_type(cross_product(B,C))) | ilf_type(A,binary_relation_type). [copy(95),unit_del(a,81),unit_del(b,81),unit_del(d,81)]. 98 -ilf_type(A,subset_type(cross_product(B,C))) | -member(D,A) | ordered_pair(f12(A,D),f13(A,D)) = D. [copy(97),unit_del(a,81),unit_del(b,81),unit_del(d,81),unit_del(e,81)]. 100 -empty(A) | ilf_type(A,binary_relation_type). [copy(99),merge(c),unit_del(b,81)]. 111 -member(A,B) | member(ordered_pair(A,A),identity_relation_of(B)). [factor(14,b,d),xx(e),unit_del(a,81),unit_del(b,81)]. 131 subset(A,A). [factor(37,a,b),xx(c),unit_del(a,81)]. 138 -member(power_set(A),power_set(A)) | member(power_set(A),A). [factor(52,d,f),merge(c),unit_del(a,81),unit_del(b,81)]. 154 -ilf_type(A,relation_type(B,C)) | ilf_type(range(B,C,A),subset_type(C)). [back_unit_del(80),unit_del(a,81),unit_del(b,81)]. 155 -ilf_type(A,relation_type(B,C)) | range(B,C,A) = range_of(A). [back_unit_del(79),unit_del(a,81),unit_del(b,81)]. 156 -ilf_type(A,relation_type(B,C)) | ilf_type(domain(B,C,A),subset_type(B)). [back_unit_del(77),unit_del(a,81),unit_del(b,81)]. 157 -ilf_type(A,relation_type(B,C)) | domain(B,C,A) = domain_of(A). [back_unit_del(76),unit_del(a,81),unit_del(b,81)]. 158 -member(A,B) | member(f18(B),B). [back_unit_del(74),unit_del(a,81),unit_del(b,81)]. 159 -member(A,B) | -empty(B). [back_unit_del(72),unit_del(a,81),unit_del(b,81)]. 160 empty(A) | member(f17(A),A). [back_unit_del(71),unit_del(a,81)]. 161 -member(A,B) | ordered_pair(f14(B,A),f15(B,A)) = A | f16(B) != ordered_pair(C,D). [back_unit_del(69),unit_del(a,81),unit_del(b,81),unit_del(e,81),unit_del(f,81)]. 162 -member(A,B) | ordered_pair(f14(B,A),f15(B,A)) = A | member(f16(B),B). [back_unit_del(67),unit_del(a,81),unit_del(b,81)]. 163 empty(A) | ilf_type(f10(A),member_type(A)). [back_unit_del(57),unit_del(b,81)]. 164 empty(A) | member(B,A) | -ilf_type(B,member_type(A)). [back_unit_del(56),unit_del(a,81),unit_del(c,81)]. 165 empty(A) | ilf_type(B,member_type(A)) | -member(B,A). [back_unit_del(55),unit_del(a,81),unit_del(c,81)]. 166 -empty(power_set(A)). [back_unit_del(53),unit_del(a,81)]. 167 -member(A,B) | member(A,C) | -member(B,power_set(C)). [back_unit_del(52),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. 168 member(A,power_set(B)) | -member(f9(A,B),B). [back_unit_del(51),unit_del(a,81),unit_del(b,81)]. 169 member(A,power_set(B)) | member(f9(A,B),A). [back_unit_del(50),unit_del(a,81),unit_del(b,81)]. 170 ilf_type(f8(A),subset_type(A)). [back_unit_del(46),unit_del(a,81)]. 171 ilf_type(A,member_type(power_set(B))) | -ilf_type(A,subset_type(B)). [back_unit_del(45),unit_del(a,81),unit_del(b,81)]. 172 ilf_type(A,subset_type(B)) | -ilf_type(A,member_type(power_set(B))). [back_unit_del(44),unit_del(a,81),unit_del(b,81)]. 173 subset(A,B) | A != B. [back_unit_del(38),unit_del(a,81),unit_del(b,81)]. 174 subset(A,B) | B != A. [back_unit_del(37),unit_del(a,81),unit_del(b,81)]. 175 -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | -member(ordered_pair(C,D),A) | member(ordered_pair(C,D),B) | -member(ordered_pair(f6(A,B),f7(A,B)),B). [back_unit_del(36),unit_del(c,81),unit_del(d,81)]. 176 -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | -member(ordered_pair(C,D),A) | member(ordered_pair(C,D),B) | member(ordered_pair(f6(A,B),f7(A,B)),A). [back_unit_del(35),unit_del(c,81),unit_del(d,81)]. 178 -member(A,B) | member(A,C) | -member(f3(B,C),C). [back_unit_del(27),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. 179 -member(A,B) | member(A,C) | member(f3(B,C),B). [back_unit_del(26),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. 180 -member(A,B) | member(A,C) | -subset(B,C). [back_unit_del(24),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. 181 subset(A,B) | -member(f2(A,B),B). [back_unit_del(23),unit_del(a,81),unit_del(b,81)]. 182 subset(A,B) | member(f2(A,B),A). [back_unit_del(22),unit_del(a,81),unit_del(b,81)]. 183 ilf_type(f1(A,B),relation_type(B,A)). [back_unit_del(20),unit_del(a,81),unit_del(b,81)]. 184 -ilf_type(A,relation_type(B,C)) | ilf_type(A,subset_type(cross_product(B,C))). [back_unit_del(19),unit_del(a,81),unit_del(b,81)]. 185 -ilf_type(A,subset_type(cross_product(B,C))) | ilf_type(A,relation_type(B,C)). [back_unit_del(18),unit_del(a,81),unit_del(b,81)]. 186 ilf_type(identity_relation_of(A),binary_relation_type). [back_unit_del(17),unit_del(a,81)]. 187 A = B | -member(ordered_pair(B,A),identity_relation_of(C)). [back_unit_del(16),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. 188 member(A,B) | -member(ordered_pair(A,C),identity_relation_of(B)). [back_unit_del(15),unit_del(a,81),unit_del(b,81),unit_del(d,81)]. 189 -member(A,B) | member(ordered_pair(A,C),identity_relation_of(B)) | C != A. [back_unit_del(14),unit_del(a,81),unit_del(b,81),unit_del(d,81)]. 190 -ilf_type(A,relation_type(B,C)) | -subset(identity_relation_of(D),A) | subset(D,range(B,C,A)). [back_unit_del(13),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. 191 -ilf_type(A,relation_type(B,C)) | -subset(identity_relation_of(D),A) | subset(D,domain(B,C,A)). [back_unit_del(12),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. 192 -subset(A,B) | -subset(B,A) | B = A. [back_unit_del(11),unit_del(a,81),unit_del(b,81)]. end_of_list. formulas(demodulators). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.02 seconds. given #1 (I,wt=18): 30 -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | subset(A,B) | member(ordered_pair(f4(A,B),f5(A,B)),A). [assumption]. given #2 (I,wt=18): 31 -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | subset(A,B) | -member(ordered_pair(f4(A,B),f5(A,B)),B). [assumption]. given #3 (I,wt=3): 43 ilf_type(c1,binary_relation_type). [assumption]. given #4 (I,wt=3): 81 ilf_type(A,set_type). [assumption]. given #5 (I,wt=5): 82 ilf_type(c4,relation_type(c3,c2)). [assumption]. given #6 (I,wt=4): 83 subset(identity_relation_of(c3),c4). [assumption]. given #7 (I,wt=6): 84 -subset(c3,range(c3,c2,c4)). [assumption]. given #8 (I,wt=7): 86 member(f11(A),A) | ilf_type(A,binary_relation_type). [copy(85),merge(c),unit_del(a,81)]. given #9 (I,wt=9): 88 f11(A) != ordered_pair(B,C) | ilf_type(A,binary_relation_type). [copy(87),flip(d),merge(e),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. given #10 (I,wt=15): 90 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | -ilf_type(B,binary_relation_type). [copy(89),merge(e),unit_del(a,81),unit_del(b,81)]. given #11 (I,wt=16): 92 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | member(f11(B),B). [copy(91),merge(e),unit_del(a,81),unit_del(b,81)]. given #12 (I,wt=18): 94 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | f11(B) != ordered_pair(C,D). [copy(93),flip(h),merge(e),unit_del(a,81),unit_del(b,81),unit_del(e,81),unit_del(f,81)]. given #13 (I,wt=9): 96 -ilf_type(A,subset_type(cross_product(B,C))) | ilf_type(A,binary_relation_type). [copy(95),unit_del(a,81),unit_del(b,81),unit_del(d,81)]. given #14 (I,wt=18): 98 -ilf_type(A,subset_type(cross_product(B,C))) | -member(D,A) | ordered_pair(f12(A,D),f13(A,D)) = D. [copy(97),unit_del(a,81),unit_del(b,81),unit_del(d,81),unit_del(e,81)]. given #15 (I,wt=5): 100 -empty(A) | ilf_type(A,binary_relation_type). [copy(99),merge(c),unit_del(b,81)]. given #16 (I,wt=9): 111 -member(A,B) | member(ordered_pair(A,A),identity_relation_of(B)). [factor(14,b,d),xx(e),unit_del(a,81),unit_del(b,81)]. given #17 (I,wt=3): 131 subset(A,A). [factor(37,a,b),xx(c),unit_del(a,81)]. given #18 (I,wt=9): 138 -member(power_set(A),power_set(A)) | member(power_set(A),A). [factor(52,d,f),merge(c),unit_del(a,81),unit_del(b,81)]. given #19 (I,wt=12): 154 -ilf_type(A,relation_type(B,C)) | ilf_type(range(B,C,A),subset_type(C)). [back_unit_del(80),unit_del(a,81),unit_del(b,81)]. given #20 (I,wt=12): 155 -ilf_type(A,relation_type(B,C)) | range(B,C,A) = range_of(A). [back_unit_del(79),unit_del(a,81),unit_del(b,81)]. given #21 (I,wt=12): 156 -ilf_type(A,relation_type(B,C)) | ilf_type(domain(B,C,A),subset_type(B)). [back_unit_del(77),unit_del(a,81),unit_del(b,81)]. given #22 (I,wt=12): 157 -ilf_type(A,relation_type(B,C)) | domain(B,C,A) = domain_of(A). [back_unit_del(76),unit_del(a,81),unit_del(b,81)]. given #23 (I,wt=7): 158 -member(A,B) | member(f18(B),B). [back_unit_del(74),unit_del(a,81),unit_del(b,81)]. given #24 (I,wt=5): 159 -member(A,B) | -empty(B). [back_unit_del(72),unit_del(a,81),unit_del(b,81)]. given #25 (I,wt=6): 160 empty(A) | member(f17(A),A). [back_unit_del(71),unit_del(a,81)]. given #26 (I,wt=18): 161 -member(A,B) | ordered_pair(f14(B,A),f15(B,A)) = A | f16(B) != ordered_pair(C,D). [back_unit_del(69),unit_del(a,81),unit_del(b,81),unit_del(e,81),unit_del(f,81)]. given #27 (I,wt=16): 162 -member(A,B) | ordered_pair(f14(B,A),f15(B,A)) = A | member(f16(B),B). [back_unit_del(67),unit_del(a,81),unit_del(b,81)]. given #28 (I,wt=7): 163 empty(A) | ilf_type(f10(A),member_type(A)). [back_unit_del(57),unit_del(b,81)]. given #29 (I,wt=9): 164 empty(A) | member(B,A) | -ilf_type(B,member_type(A)). [back_unit_del(56),unit_del(a,81),unit_del(c,81)]. given #30 (I,wt=9): 165 empty(A) | ilf_type(B,member_type(A)) | -member(B,A). [back_unit_del(55),unit_del(a,81),unit_del(c,81)]. given #31 (I,wt=3): 166 -empty(power_set(A)). [back_unit_del(53),unit_del(a,81)]. given #32 (I,wt=10): 167 -member(A,B) | member(A,C) | -member(B,power_set(C)). [back_unit_del(52),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. given #33 (I,wt=9): 168 member(A,power_set(B)) | -member(f9(A,B),B). [back_unit_del(51),unit_del(a,81),unit_del(b,81)]. given #34 (I,wt=9): 169 member(A,power_set(B)) | member(f9(A,B),A). [back_unit_del(50),unit_del(a,81),unit_del(b,81)]. given #35 (I,wt=5): 170 ilf_type(f8(A),subset_type(A)). [back_unit_del(46),unit_del(a,81)]. given #36 (I,wt=9): 171 ilf_type(A,member_type(power_set(B))) | -ilf_type(A,subset_type(B)). [back_unit_del(45),unit_del(a,81),unit_del(b,81)]. given #37 (I,wt=9): 172 ilf_type(A,subset_type(B)) | -ilf_type(A,member_type(power_set(B))). [back_unit_del(44),unit_del(a,81),unit_del(b,81)]. given #38 (I,wt=6): 173 subset(A,B) | A != B. [back_unit_del(38),unit_del(a,81),unit_del(b,81)]. given #39 (I,wt=6): 174 subset(A,B) | B != A. [back_unit_del(37),unit_del(a,81),unit_del(b,81)]. given #40 (I,wt=25): 175 -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | -member(ordered_pair(C,D),A) | member(ordered_pair(C,D),B) | -member(ordered_pair(f6(A,B),f7(A,B)),B). [back_unit_del(36),unit_del(c,81),unit_del(d,81)]. given #41 (I,wt=25): 176 -ilf_type(A,binary_relation_type) | -ilf_type(B,binary_relation_type) | -member(ordered_pair(C,D),A) | member(ordered_pair(C,D),B) | member(ordered_pair(f6(A,B),f7(A,B)),A). [back_unit_del(35),unit_del(c,81),unit_del(d,81)]. given #42 (I,wt=11): 178 -member(A,B) | member(A,C) | -member(f3(B,C),C). [back_unit_del(27),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. given #43 (I,wt=11): 179 -member(A,B) | member(A,C) | member(f3(B,C),B). [back_unit_del(26),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. given #44 (I,wt=9): 180 -member(A,B) | member(A,C) | -subset(B,C). [back_unit_del(24),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. given #45 (I,wt=8): 181 subset(A,B) | -member(f2(A,B),B). [back_unit_del(23),unit_del(a,81),unit_del(b,81)]. given #46 (I,wt=8): 182 subset(A,B) | member(f2(A,B),A). [back_unit_del(22),unit_del(a,81),unit_del(b,81)]. given #47 (I,wt=7): 183 ilf_type(f1(A,B),relation_type(B,A)). [back_unit_del(20),unit_del(a,81),unit_del(b,81)]. given #48 (I,wt=11): 184 -ilf_type(A,relation_type(B,C)) | ilf_type(A,subset_type(cross_product(B,C))). [back_unit_del(19),unit_del(a,81),unit_del(b,81)]. given #49 (I,wt=11): 185 -ilf_type(A,subset_type(cross_product(B,C))) | ilf_type(A,relation_type(B,C)). [back_unit_del(18),unit_del(a,81),unit_del(b,81)]. given #50 (I,wt=4): 186 ilf_type(identity_relation_of(A),binary_relation_type). [back_unit_del(17),unit_del(a,81)]. given #51 (I,wt=9): 187 A = B | -member(ordered_pair(B,A),identity_relation_of(C)). [back_unit_del(16),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. given #52 (I,wt=9): 188 member(A,B) | -member(ordered_pair(A,C),identity_relation_of(B)). [back_unit_del(15),unit_del(a,81),unit_del(b,81),unit_del(d,81)]. given #53 (I,wt=12): 189 -member(A,B) | member(ordered_pair(A,C),identity_relation_of(B)) | C != A. [back_unit_del(14),unit_del(a,81),unit_del(b,81),unit_del(d,81)]. given #54 (I,wt=15): 190 -ilf_type(A,relation_type(B,C)) | -subset(identity_relation_of(D),A) | subset(D,range(B,C,A)). [back_unit_del(13),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. given #55 (I,wt=15): 191 -ilf_type(A,relation_type(B,C)) | -subset(identity_relation_of(D),A) | subset(D,domain(B,C,A)). [back_unit_del(12),unit_del(a,81),unit_del(b,81),unit_del(c,81)]. given #56 (I,wt=9): 192 -subset(A,B) | -subset(B,A) | B = A. [back_unit_del(11),unit_del(a,81),unit_del(b,81)]. given #57 (F,wt=4): 199 -subset(c3,range_of(c4)). [back_rewrite(84),rewrite(197(5))]. given #58 (F,wt=4): 261 range_of(c4) != c3. [ur(174,a,199,a)]. given #59 (T,wt=4): 218 member(A,power_set(A)). [resolve(169,b,168,b),merge(b)]. given #60 (T,wt=5): 198 ilf_type(range_of(c4),subset_type(c2)). [back_rewrite(196),rewrite(197(4))]. given #61 (A,wt=15): 193 -ilf_type(A,binary_relation_type) | subset(A,c1) | member(ordered_pair(f4(A,c1),f5(A,c1)),A). [resolve(43,a,30,b)]. given #62 (F,wt=7): 260 -member(f2(c3,range_of(c4)),range_of(c4)). [ur(181,a,199,a)]. given #63 (F,wt=7): 262 -member(ordered_pair(c3,range_of(c4)),identity_relation_of(A)). [ur(187,a,261,a)]. given #64 (T,wt=5): 202 ilf_type(domain_of(c4),subset_type(c3)). [back_rewrite(200),rewrite(201(4))]. given #65 (T,wt=5): 269 ilf_type(A,member_type(power_set(A))). [resolve(218,a,165,c),unit_del(a,166)]. given #66 (A,wt=15): 194 -ilf_type(A,binary_relation_type) | subset(c1,A) | member(ordered_pair(f4(c1,A),f5(c1,A)),c1). [resolve(43,a,30,a)]. given #67 (F,wt=7): 263 -member(ordered_pair(range_of(c4),c3),identity_relation_of(A)). [ur(187,a,261,a(flip))]. given #68 (F,wt=8): 279 -subset(power_set(f2(c3,range_of(c4))),range_of(c4)). [ur(180,a,218,a,b,260,a)]. given #69 (T,wt=4): 287 ilf_type(A,subset_type(A)). [resolve(269,a,172,b)]. given #70 (T,wt=5): 297 ilf_type(cross_product(A,B),binary_relation_type). [resolve(287,a,96,a)]. given #71 (A,wt=11): 195 member(ordered_pair(f11(A),f11(A)),identity_relation_of(A)) | ilf_type(A,binary_relation_type). [resolve(111,a,86,a)]. given #72 (F,wt=8): 283 -subset(power_set(ordered_pair(c3,range_of(c4))),identity_relation_of(A)). [ur(180,a,218,a,b,262,a)]. given #73 (F,wt=8): 290 -subset(power_set(ordered_pair(range_of(c4),c3)),identity_relation_of(A)). [ur(180,a,218,a,b,263,a)]. given #74 (T,wt=6): 204 empty(A) | member(f18(A),A). [resolve(160,b,158,a)]. given #75 (T,wt=6): 211 empty(A) | member(f10(A),A). [resolve(164,c,163,b),merge(c)]. given #76 (A,wt=7): 197 range(c3,c2,c4) = range_of(c4). [resolve(155,a,82,a)]. given #77 (F,wt=8): 295 power_set(f2(c3,range_of(c4))) != range_of(c4). [ur(174,a,279,a),flip(a)]. given #78 (F,wt=8): 317 power_set(ordered_pair(c3,range_of(c4))) != identity_relation_of(A). [ur(174,a,283,a),flip(a)]. given #79 (T,wt=6): 223 member(A,power_set(B)) | -empty(A). [resolve(169,b,159,a)]. given #80 (T,wt=6): 230 ilf_type(f8(cross_product(A,B)),binary_relation_type). [resolve(170,a,96,a)]. given #81 (A,wt=7): 201 domain(c3,c2,c4) = domain_of(c4). [resolve(157,a,82,a)]. given #82 (F,wt=8): 320 power_set(ordered_pair(range_of(c4),c3)) != identity_relation_of(A). [ur(174,a,290,a),flip(a)]. given #83 (F,wt=9): 281 -member(power_set(f2(c3,range_of(c4))),power_set(range_of(c4))). [ur(167,a,218,a,b,260,a)]. given #84 (T,wt=6): 231 ilf_type(f8(A),member_type(power_set(A))). [resolve(171,b,170,a)]. given #85 (T,wt=5): 356 member(f8(A),power_set(A)). [resolve(231,a,164,c),unit_del(a,166)]. given #86 (A,wt=7): 203 member(f18(A),A) | ilf_type(A,binary_relation_type). [resolve(158,a,86,a)]. given #87 (F,wt=8): 367 -member(ordered_pair(range_of(c4),c3),f8(identity_relation_of(A))). [ur(167,b,263,a,c,356,a)]. given #88 (F,wt=8): 368 -member(ordered_pair(c3,range_of(c4)),f8(identity_relation_of(A))). [ur(167,b,262,a,c,356,a)]. given #89 (T,wt=6): 232 ilf_type(f10(power_set(A)),subset_type(A)). [resolve(172,b,163,b),unit_del(b,166)]. given #90 (T,wt=6): 246 ilf_type(c4,subset_type(cross_product(c3,c2))). [resolve(184,a,82,a)]. given #91 (A,wt=10): 205 empty(A) | member(ordered_pair(f17(A),f17(A)),identity_relation_of(A)). [resolve(160,b,111,a)]. given #92 (F,wt=8): 369 -member(f2(c3,range_of(c4)),f8(range_of(c4))). [ur(167,b,260,a,c,356,a)]. given #93 (F,wt=9): 285 -member(power_set(ordered_pair(c3,range_of(c4))),power_set(identity_relation_of(A))). [ur(167,a,218,a,b,262,a)]. given #94 (T,wt=3): 389 ilf_type(c4,binary_relation_type). [resolve(246,a,96,a)]. given #95 (T,wt=5): 397 empty(A) | -empty(identity_relation_of(A)). [resolve(205,b,159,a)]. given #96 (A,wt=20): 206 empty(A) | -ilf_type(A,subset_type(cross_product(B,C))) | ordered_pair(f12(A,f17(A)),f13(A,f17(A))) = f17(A). [resolve(160,b,98,b)]. given #97 (F,wt=4): 419 -empty(identity_relation_of(power_set(A))). [ur(397,a,166,a)]. given #98 (F,wt=5): 424 -empty(identity_relation_of(identity_relation_of(power_set(A)))). [ur(397,a,419,a)]. given #99 (T,wt=6): 259 member(f2(c3,range_of(c4)),c3). [resolve(199,a,182,a)]. given #100 (T,wt=4): 436 member(f18(c3),c3). [resolve(259,a,158,a)]. given #101 (A,wt=18): 207 empty(A) | ordered_pair(f12(A,f17(A)),f13(A,f17(A))) = f17(A) | member(f11(A),A). [resolve(160,b,92,a)]. given #102 (F,wt=2): 435 -empty(c3). [resolve(259,a,159,a)]. given #103 (F,wt=3): 469 -empty(identity_relation_of(c3)). [ur(397,a,435,a)]. given #104 (T,wt=5): 450 ilf_type(f18(c3),member_type(c3)). [resolve(436,a,165,c),unit_del(a,435)]. given #105 (T,wt=6): 271 member(f18(power_set(A)),power_set(A)). [resolve(218,a,158,a)]. given #106 (A,wt=17): 208 empty(A) | ordered_pair(f12(A,f17(A)),f13(A,f17(A))) = f17(A) | -ilf_type(A,binary_relation_type). [resolve(160,b,90,a)]. given #107 (F,wt=4): 470 -empty(identity_relation_of(identity_relation_of(c3))). [ur(397,a,469,a)]. given #108 (F,wt=5): 441 -subset(c3,f8(range_of(c4))). [ur(180,a,259,a,b,369,a)]. given #109 (T,wt=6): 276 ilf_type(range_of(c4),member_type(power_set(c2))). [resolve(198,a,171,b)]. given #110 (T,wt=5): 498 member(range_of(c4),power_set(c2)). [resolve(276,a,164,c),unit_del(a,166)]. given #111 (A,wt=18): 209 ordered_pair(f14(A,f17(A)),f15(A,f17(A))) = f17(A) | member(f16(A),A) | empty(A). [resolve(162,a,160,b)]. given #112 (F,wt=5): 445 -member(c3,power_set(range_of(c4))). [ur(167,a,259,a,b,260,a)]. given #113 (F,wt=5): 492 -empty(identity_relation_of(identity_relation_of(identity_relation_of(c3)))). [ur(397,a,470,a)]. given #114 (T,wt=6): 286 ilf_type(domain_of(c4),member_type(power_set(c3))). [resolve(202,a,171,b)]. given #115 (T,wt=5): 532 member(domain_of(c4),power_set(c3)). [resolve(286,a,164,c),unit_del(a,166)]. given #116 (A,wt=19): 210 ordered_pair(f14(A,f11(A)),f15(A,f11(A))) = f11(A) | member(f16(A),A) | ilf_type(A,binary_relation_type). [resolve(162,a,86,a)]. given #117 (F,wt=5): 497 f8(range_of(c4)) != c3. [ur(174,a,441,a)]. given #118 (F,wt=6): 427 -empty(identity_relation_of(identity_relation_of(identity_relation_of(power_set(A))))). [ur(397,a,424,a)]. given #119 (T,wt=6): 309 ilf_type(A,binary_relation_type) | -empty(identity_relation_of(A)). [resolve(195,a,159,a)]. given #120 (T,wt=7): 212 empty(A) | ilf_type(f17(A),member_type(A)). [resolve(165,c,160,b),merge(c)]. given #121 (A,wt=10): 213 empty(A) | ilf_type(f11(A),member_type(A)) | ilf_type(A,binary_relation_type). [resolve(165,c,86,a)]. given #122 (F,wt=6): 444 -member(c3,power_set(f8(range_of(c4)))). [ur(167,a,259,a,b,369,a)]. given #123 (F,wt=6): 522 -subset(power_set(c3),power_set(range_of(c4))). [ur(180,a,218,a,b,445,a)]. given #124 (T,wt=6): 553 ilf_type(f17(power_set(A)),subset_type(A)). [resolve(212,b,172,b),unit_del(a,166)]. given #125 (T,wt=7): 239 -member(A,identity_relation_of(c3)) | member(A,c4). [resolve(180,c,83,a)]. given #126 (A,wt=10): 214 member(f17(A),B) | -member(A,power_set(B)) | empty(A). [resolve(167,a,160,b)]. given #127 (F,wt=6): 525 -member(c3,f8(power_set(range_of(c4)))). [ur(167,b,445,a,c,356,a)]. given #128 (F,wt=6): 528 -ilf_type(c3,member_type(power_set(range_of(c4)))). [ur(164,a,166,a,b,445,a)]. given #129 (T,wt=5): 570 member(f10(identity_relation_of(c3)),c4). [resolve(239,a,211,b),unit_del(b,469)]. given #130 (T,wt=4): 597 member(f18(c4),c4). [resolve(570,a,158,a)]. given #131 (A,wt=11): 215 member(f11(A),B) | -member(A,power_set(B)) | ilf_type(A,binary_relation_type). [resolve(167,a,86,a)]. given #132 (F,wt=2): 596 -empty(c4). [resolve(570,a,159,a)]. given #133 (F,wt=3): 621 -empty(identity_relation_of(c4)). [ur(397,a,596,a)]. given #134 (T,wt=5): 572 member(f18(identity_relation_of(c3)),c4). [resolve(239,a,204,b),unit_del(b,469)]. given #135 (T,wt=5): 575 member(f17(identity_relation_of(c3)),c4). [resolve(239,a,160,b),unit_del(b,469)]. given #136 (A,wt=8): 216 -member(A,f17(power_set(B))) | member(A,B). [resolve(167,c,160,b),unit_del(c,166)]. given #137 (F,wt=4): 622 -empty(identity_relation_of(identity_relation_of(c4))). [ur(397,a,621,a)]. given #138 (F,wt=5): 590 -ilf_type(c3,subset_type(range_of(c4))). [ur(171,a,528,a)]. given #139 (T,wt=5): 607 ilf_type(f18(c4),member_type(c4)). [resolve(597,a,165,c),unit_del(a,596)]. given #140 (T,wt=6): 602 ilf_type(f10(identity_relation_of(c3)),member_type(c4)). [back_unit_del(594),unit_del(a,596)]. given #141 (A,wt=12): 217 -member(A,f11(power_set(B))) | member(A,B) | ilf_type(power_set(B),binary_relation_type). [resolve(167,c,86,a)]. given #142 (F,wt=5): 658 -empty(identity_relation_of(identity_relation_of(identity_relation_of(c4)))). [ur(397,a,622,a)]. given #143 (F,wt=6): 529 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(c3))))). [ur(397,a,492,a)]. given #144 (T,wt=6): 628 ilf_type(f18(identity_relation_of(c3)),member_type(c4)). [resolve(572,a,165,c),unit_del(a,596)]. given #145 (T,wt=6): 637 ilf_type(f17(identity_relation_of(c3)),member_type(c4)). [resolve(575,a,165,c),unit_del(a,596)]. given #146 (A,wt=14): 219 member(power_set(A),power_set(B)) | -member(C,f9(power_set(A),B)) | member(C,A). [resolve(169,b,167,c)]. given #147 (F,wt=6): 565 power_set(range_of(c4)) != power_set(c3). [ur(174,a,522,a)]. given #148 (F,wt=6): 665 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(c4))))). [ur(397,a,658,a)]. given #149 (T,wt=7): 242 ilf_type(domain_of(f1(A,B)),subset_type(B)). [resolve(183,a,156,a),rewrite(241(2))]. given #150 (T,wt=7): 244 ilf_type(range_of(f1(A,B)),subset_type(A)). [resolve(183,a,154,a),rewrite(243(2))]. given #151 (A,wt=13): 220 member(A,power_set(B)) | member(f9(A,B),C) | -member(A,power_set(C)). [resolve(169,b,167,a)]. given #152 (F,wt=7): 443 -member(f3(c3,range_of(c4)),range_of(c4)). [ur(178,a,259,a,b,260,a)]. given #153 (F,wt=7): 524 -member(f9(c3,range_of(c4)),range_of(c4)). [ur(168,a,445,a)]. given #154 (T,wt=7): 272 member(ordered_pair(A,A),identity_relation_of(power_set(A))). [resolve(218,a,111,a)]. given #155 (T,wt=7): 296 ilf_type(cross_product(A,B),relation_type(A,B)). [resolve(287,a,185,a)]. given #156 (A,wt=12): 221 member(A,power_set(B)) | empty(A) | ilf_type(f9(A,B),member_type(A)). [resolve(169,b,165,c)]. given #157 (F,wt=7): 526 -member(c3,f18(power_set(power_set(range_of(c4))))). [ur(167,b,445,a,c,271,a)]. given #158 (F,wt=7): 527 -member(power_set(c3),power_set(power_set(range_of(c4)))). [ur(167,a,218,a,b,445,a)]. given #159 (T,wt=7): 325 empty(A) | ilf_type(f18(A),member_type(A)). [resolve(204,b,165,c),merge(b)]. given #160 (T,wt=6): 765 ilf_type(f18(power_set(A)),subset_type(A)). [resolve(325,b,172,b),unit_del(a,166)]. given #161 (A,wt=23): 222 member(A,power_set(B)) | ordered_pair(f14(A,f9(A,B)),f15(A,f9(A,B))) = f9(A,B) | member(f16(A),A). [resolve(169,b,162,a)]. given #162 (F,wt=7): 550 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(power_set(A)))))). [ur(397,a,427,a)]. given #163 (F,wt=7): 556 -subset(power_set(c3),power_set(f8(range_of(c4)))). [ur(180,a,218,a,b,444,a)]. given #164 (T,wt=7): 359 -member(A,f8(B)) | member(A,B). [resolve(356,a,167,c)]. given #165 (T,wt=7): 386 ilf_type(f10(power_set(A)),member_type(power_set(A))). [resolve(232,a,171,b)]. given #166 (A,wt=8): 224 member(A,power_set(B)) | member(f18(A),A). [resolve(169,b,158,a)]. given #167 (F,wt=7): 559 -member(c3,f8(power_set(f8(range_of(c4))))). [ur(167,b,444,a,c,356,a)]. given #168 (F,wt=7): 562 -ilf_type(c3,member_type(power_set(f8(range_of(c4))))). [ur(164,a,166,a,b,444,a)]. given #169 (T,wt=6): 792 member(f10(power_set(A)),power_set(A)). [resolve(386,a,164,c),unit_del(a,166)]. given #170 (T,wt=7): 387 ilf_type(f10(power_set(cross_product(A,B))),binary_relation_type). [resolve(232,a,96,a)]. given #171 (A,wt=14): 225 member(A,power_set(B)) | member(ordered_pair(f9(A,B),f9(A,B)),identity_relation_of(A)). [resolve(169,b,111,a)]. given #172 (F,wt=6): 828 -ilf_type(c3,subset_type(f8(range_of(c4)))). [ur(171,a,562,a)]. given #173 (F,wt=7): 585 -subset(power_set(c3),f8(power_set(range_of(c4)))). [ur(180,a,218,a,b,525,a)]. given #174 (T,wt=7): 388 ilf_type(c4,member_type(power_set(cross_product(c3,c2)))). [resolve(246,a,171,b)]. given #175 (T,wt=6): 874 member(c4,power_set(cross_product(c3,c2))). [resolve(388,a,164,c),unit_del(a,166)]. given #176 (A,wt=25): 226 member(A,power_set(B)) | -ilf_type(A,subset_type(cross_product(C,D))) | ordered_pair(f12(A,f9(A,B)),f13(A,f9(A,B))) = f9(A,B). [resolve(169,b,98,b)]. given #177 (F,wt=7): 587 -member(c3,f8(f8(power_set(range_of(c4))))). [ur(167,b,525,a,c,356,a)]. given #178 (F,wt=7): 648 -member(c3,f17(power_set(power_set(range_of(c4))))). [ur(216,b,445,a)]. given #179 (T,wt=6): 876 member(f17(c4),cross_product(c3,c2)). [resolve(874,a,214,b),unit_del(b,596)]. given #180 (T,wt=7): 446 ilf_type(f2(c3,range_of(c4)),member_type(c3)). [back_unit_del(433),unit_del(a,435)]. given #181 (A,wt=23): 227 member(A,power_set(B)) | ordered_pair(f12(A,f9(A,B)),f13(A,f9(A,B))) = f9(A,B) | member(f11(A),A). [resolve(169,b,92,a)]. given #182 (F,wt=4): 915 -empty(cross_product(c3,c2)). [resolve(876,a,159,a)]. given #183 (F,wt=5): 936 -empty(identity_relation_of(cross_product(c3,c2))). [ur(397,a,915,a)]. given #184 (T,wt=7): 476 ilf_type(f18(power_set(A)),member_type(power_set(A))). [resolve(271,a,165,c),unit_del(a,166)]. given #185 (T,wt=7): 495 member(f2(c3,f8(range_of(c4))),c3). [resolve(441,a,182,a)]. given #186 (A,wt=22): 228 member(A,power_set(B)) | ordered_pair(f12(A,f9(A,B)),f13(A,f9(A,B))) = f9(A,B) | -ilf_type(A,binary_relation_type). [resolve(169,b,90,a)]. given #187 (F,wt=6): 937 -empty(identity_relation_of(identity_relation_of(cross_product(c3,c2)))). [ur(397,a,936,a)]. given #188 (F,wt=7): 668 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(c3)))))). [ur(397,a,529,a)]. given #189 (T,wt=7): 501 -member(A,range_of(c4)) | member(A,c2). [resolve(498,a,167,c)]. given #190 (T,wt=7): 535 -member(A,domain_of(c4)) | member(A,c3). [resolve(532,a,167,c)]. given #191 (A,wt=15): 229 member(power_set(power_set(A)),power_set(A)) | -member(power_set(power_set(A)),f9(power_set(power_set(A)),A)). [factor(219,a,c)]. given #192 (F,wt=7): 677 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(c4)))))). [ur(397,a,665,a)]. given #193 (F,wt=7): 788 power_set(f8(range_of(c4))) != power_set(c3). [ur(174,a,556,a)]. given #194 (T,wt=7): 547 member(f16(A),A) | ilf_type(A,binary_relation_type). [resolve(210,a,88,a(flip)),merge(c)]. given #195 (T,wt=7): 568 ilf_type(f17(power_set(A)),member_type(power_set(A))). [resolve(553,a,171,b)]. given #196 (A,wt=14): 233 member(f9(A,B),C) | -member(f3(A,C),C) | member(A,power_set(B)). [resolve(178,a,169,b)]. given #197 (F,wt=7): 842 -member(c3,f10(power_set(power_set(range_of(c4))))). [ur(167,b,445,a,c,792,a)]. given #198 (F,wt=7): 873 f8(power_set(range_of(c4))) != power_set(c3). [ur(174,a,585,a)]. given #199 (T,wt=6): 985 member(f17(power_set(A)),power_set(A)). [resolve(568,a,164,c),unit_del(a,166)]. given #200 (T,wt=7): 569 ilf_type(f17(power_set(cross_product(A,B))),binary_relation_type). [resolve(553,a,96,a)]. given #201 (A,wt=11): 234 member(f17(A),B) | -member(f3(A,B),B) | empty(A). [resolve(178,a,160,b)]. given #202 (F,wt=7): 951 -empty(identity_relation_of(identity_relation_of(identity_relation_of(cross_product(c3,c2))))). [ur(397,a,937,a)]. given #203 (F,wt=8): 471 -ilf_type(ordered_pair(range_of(c4),c3),member_type(identity_relation_of(c3))). [ur(164,a,469,a,b,263,a)]. given #204 (T,wt=7): 571 member(ordered_pair(f17(c3),f17(c3)),c4). [resolve(239,a,205,b),unit_del(b,435)]. given #205 (T,wt=7): 720 ilf_type(domain_of(cross_product(A,B)),subset_type(A)). [resolve(296,a,156,a),rewrite(719(2))]. given #206 (A,wt=12): 235 member(f11(A),B) | -member(f3(A,B),B) | ilf_type(A,binary_relation_type). [resolve(178,a,86,a)]. given #207 (F,wt=8): 472 -ilf_type(ordered_pair(c3,range_of(c4)),member_type(identity_relation_of(c3))). [ur(164,a,469,a,b,262,a)]. given #208 (F,wt=8): 521 -member(ordered_pair(c3,A),identity_relation_of(power_set(range_of(c4)))). [ur(188,a,445,a)]. given #209 (T,wt=7): 722 ilf_type(range_of(cross_product(A,B)),subset_type(B)). [resolve(296,a,154,a),rewrite(721(2))]. given #210 (T,wt=7): 723 ilf_type(f9(c3,range_of(c4)),member_type(c3)). [resolve(221,a,445,a),unit_del(a,435)]. given #211 (A,wt=14): 236 member(f9(A,B),C) | member(f3(A,C),A) | member(A,power_set(B)). [resolve(179,a,169,b)]. given #212 (F,wt=8): 548 -member(ordered_pair(c3,f8(range_of(c4))),identity_relation_of(A)). [ur(187,a,497,a)]. given #213 (F,wt=8): 549 -member(ordered_pair(f8(range_of(c4)),c3),identity_relation_of(A)). [ur(187,a,497,a(flip))]. given #214 (T,wt=6): 1051 member(f9(c3,range_of(c4)),c3). [resolve(723,a,164,c),unit_del(a,435)]. given #215 (T,wt=6): 1053 member(f3(c3,range_of(c4)),c3). [resolve(236,a,524,a),unit_del(b,445)]. given #216 (A,wt=11): 237 member(f17(A),B) | member(f3(A,B),A) | empty(A). [resolve(179,a,160,b)]. given #217 (F,wt=8): 560 -member(c3,f18(power_set(power_set(f8(range_of(c4)))))). [ur(167,b,444,a,c,271,a)]. given #218 (F,wt=8): 561 -member(power_set(c3),power_set(power_set(f8(range_of(c4))))). [ur(167,a,218,a,b,444,a)]. given #219 (T,wt=7): 768 ilf_type(f18(power_set(cross_product(A,B))),binary_relation_type). [resolve(765,a,96,a)]. given #220 (T,wt=7): 865 member(A,power_set(B)) | -empty(identity_relation_of(A)). [resolve(225,b,159,a)]. given #221 (A,wt=12): 238 member(f11(A),B) | member(f3(A,B),A) | ilf_type(A,binary_relation_type). [resolve(179,a,86,a)]. given #222 (F,wt=8): 588 -member(c3,f18(power_set(f8(power_set(range_of(c4)))))). [ur(167,b,525,a,c,271,a)]. given #223 (F,wt=8): 589 -member(power_set(c3),power_set(f8(power_set(range_of(c4))))). [ur(167,a,218,a,b,525,a)]. given #224 (T,wt=7): 921 ilf_type(f17(c4),member_type(cross_product(c3,c2))). [back_unit_del(913),unit_del(a,915)]. given #225 (T,wt=7): 1165 ilf_type(f3(c3,range_of(c4)),member_type(c3)). [resolve(1053,a,165,c),unit_del(a,435)]. given #226 (A,wt=11): 240 member(f2(A,B),A) | -member(C,A) | member(C,B). [resolve(182,a,180,c)]. given #227 (F,wt=8): 623 -ilf_type(ordered_pair(range_of(c4),c3),member_type(identity_relation_of(c4))). [ur(164,a,621,a,b,263,a)]. given #228 (F,wt=8): 624 -ilf_type(ordered_pair(c3,range_of(c4)),member_type(identity_relation_of(c4))). [ur(164,a,621,a,b,262,a)]. given #229 (T,wt=8): 245 ilf_type(f1(A,B),subset_type(cross_product(B,A))). [resolve(184,a,183,a)]. given #230 (T,wt=5): 1340 ilf_type(f1(A,B),binary_relation_type). [resolve(245,a,96,a)]. given #231 (A,wt=11): 241 domain(A,B,f1(B,A)) = domain_of(f1(B,A)). [resolve(183,a,157,a)]. given #232 (F,wt=8): 647 -member(c3,f17(power_set(f8(power_set(range_of(c4)))))). [ur(216,b,525,a)]. given #233 (F,wt=8): 649 -member(c3,f17(power_set(power_set(f8(range_of(c4)))))). [ur(216,b,444,a)]. given #234 (T,wt=8): 247 ilf_type(f8(cross_product(A,B)),relation_type(A,B)). [resolve(185,a,170,a)]. given #235 (T,wt=8): 257 -subset(c4,identity_relation_of(c3)) | identity_relation_of(c3) = c4. [resolve(192,a,83,a),flip(b)]. given #236 (A,wt=11): 243 range(A,B,f1(B,A)) = range_of(f1(B,A)). [resolve(183,a,155,a)]. given #237 (F,wt=8): 695 -subset(power_set(f3(c3,range_of(c4))),range_of(c4)). [ur(180,a,218,a,b,443,a)]. given #238 (F,wt=8): 697 -member(f3(c3,range_of(c4)),f8(range_of(c4))). [ur(167,b,443,a,c,356,a)]. given #239 (T,wt=8): 268 member(A,B) | -member(power_set(A),power_set(B)). [resolve(218,a,167,a)]. given #240 (T,wt=8): 323 -member(A,f18(power_set(B))) | member(A,B). [resolve(204,b,167,c),unit_del(a,166)]. given #241 (A,wt=18): 248 -ilf_type(A,binary_relation_type) | subset(A,identity_relation_of(B)) | member(ordered_pair(f4(A,identity_relation_of(B)),f5(A,identity_relation_of(B))),A). [resolve(186,a,30,b)]. given #242 (F,wt=8): 702 -subset(power_set(f9(c3,range_of(c4))),range_of(c4)). [ur(180,a,218,a,b,524,a)]. given #243 (F,wt=8): 704 -member(f9(c3,range_of(c4)),f8(range_of(c4))). [ur(167,b,524,a,c,356,a)]. given #244 (T,wt=7): 1400 member(f3(c3,f8(range_of(c4))),c3). [resolve(704,a,236,a),unit_del(b,445)]. given #245 (T,wt=8): 333 -member(A,f10(power_set(B))) | member(A,B). [resolve(211,b,167,c),unit_del(a,166)]. given #246 (A,wt=19): 249 -ilf_type(A,binary_relation_type) | subset(identity_relation_of(B),A) | member(ordered_pair(f4(identity_relation_of(B),A),f5(identity_relation_of(B),A)),identity_relation_of(B)). [resolve(186,a,30,a)]. given #247 (F,wt=8): 750 -subset(power_set(c3),f18(power_set(power_set(range_of(c4))))). [ur(180,a,218,a,b,526,a)]. given #248 (F,wt=8): 752 -member(c3,f8(f18(power_set(power_set(range_of(c4)))))). [ur(167,b,526,a,c,356,a)]. given #249 (T,wt=8): 398 empty(A) | member(f18(identity_relation_of(A)),identity_relation_of(A)). [resolve(205,b,158,a)]. given #250 (T,wt=8): 449 member(f18(c3),A) | -member(c3,power_set(A)). [resolve(436,a,167,a)]. given #251 (A,wt=18): 250 -ilf_type(A,relation_type(B,C)) | subset(D,range(B,C,A)) | member(f2(identity_relation_of(D),A),identity_relation_of(D)). [resolve(190,b,182,a)]. given #252 (F,wt=8): 758 -subset(power_set(power_set(c3)),power_set(power_set(range_of(c4)))). [ur(180,a,218,a,b,527,a)]. given #253 (F,wt=8): 761 -member(power_set(c3),f8(power_set(power_set(range_of(c4))))). [ur(167,b,527,a,c,356,a)]. given #254 (T,wt=8): 452 member(or