============================== FOF-Prover9 =========================== FOF-Prover9 (32) version November-2006, November 2006. Process 3791 was started by mccune on cleo.thornwood, Wed Nov 22 11:23:45 2006 The command was "/home/mccune/bin/fof-prover9 -f SET667+3.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file SET667+3.in set(prolog_style_variables). formulas(assumptions). (all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> (all D (ilf_type(D,binary_relation_type) -> (member(ordered_pair(B,C),D) -> member(B,domain_of(D)) & member(C,range_of(D))))))))). (all B (ilf_type(B,set_type) -> (all C (ilf_type(C,set_type) -> (member(C,B) <-> member(ordered_pair(C,C),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) -> (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,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,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))))))))))). end_of_list. ============================== end of input ========================== % clear(auto_denials), because it is incompatiable with FOF reduction. Attempting problem reduction; original problem has = <461,102>. Problem reduction (0.00 sec) gives 2 independent subproblems: ( <610,81> <610,81> ). Max nnf_size of subproblems is 610; max cnf_max is 81. ============================== FOF REDUCTION MULTISEARCH ============= Subproblem 1 of 2 (negated): ((all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,binary_relation_type) | - member(ordered_pair(B,C),D) | member(B,domain_of(D)))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,binary_relation_type) | - member(ordered_pair(B,C),D) | member(C,range_of(D)))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | member(C,B) | - member(ordered_pair(C,C),identity_relation_of(B)))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | member(ordered_pair(C,C),identity_relation_of(B)) | - member(C,B))))) & (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,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(B,C,D),domain_of(D)))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,relation_type(B,C)) | ilf_type(domain(B,C,D),subset_type(B)))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,relation_type(B,C)) | =(range(B,C,D),range_of(D)))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,relation_type(B,C)) | ilf_type(range(B,C,D),subset_type(C)))))))) & (all B ilf_type(B,set_type)) & (exists B (ilf_type(B,set_type) & (exists C (ilf_type(C,set_type) & (exists D (ilf_type(D,set_type) & (exists E (ilf_type(E,relation_type(B,C)) & subset(identity_relation_of(D),E) & - subset(D,domain(B,C,E))))))))))). Child search process 3792 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) | -ilf_type(C,binary_relation_type) | -member(ordered_pair(A,B),C) | member(A,domain_of(C)). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,binary_relation_type) | -member(ordered_pair(A,B),C) | member(B,range_of(C)). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | member(B,A) | -member(ordered_pair(B,B),identity_relation_of(A)). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | member(ordered_pair(B,B),identity_relation_of(A)) | -member(B,A). [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,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(A,B,C) = domain_of(C). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,relation_type(A,B)) | ilf_type(domain(A,B,C),subset_type(A)). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,relation_type(A,B)) | range(A,B,C) = range_of(C). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,relation_type(A,B)) | ilf_type(range(A,B,C),subset_type(B)). [assumption]. ilf_type(A,set_type). [assumption]. ilf_type(c2,set_type). [assumption]. ilf_type(c3,set_type). [assumption]. ilf_type(c4,set_type). [assumption]. ilf_type(c5,relation_type(c2,c3)). [assumption]. subset(identity_relation_of(c4),c5). [assumption]. -subset(c4,domain(c2,c3,c5)). [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, c5, 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). 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)),A). [assumption]. 32 -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]. 42 ilf_type(c1,binary_relation_type). [assumption]. 78 ilf_type(A,set_type). [assumption]. 79 ilf_type(c5,relation_type(c2,c3)). [assumption]. 80 subset(identity_relation_of(c4),c5). [assumption]. 81 -subset(c4,domain(c2,c3,c5)). [assumption]. 83 member(f11(A),A) | ilf_type(A,binary_relation_type). [copy(82),merge(c),unit_del(a,78)]. 85 f11(A) != ordered_pair(B,C) | ilf_type(A,binary_relation_type). [copy(84),flip(d),merge(e),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. 87 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | -ilf_type(B,binary_relation_type). [copy(86),merge(e),unit_del(a,78),unit_del(b,78)]. 89 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | member(f11(B),B). [copy(88),merge(e),unit_del(a,78),unit_del(b,78)]. 91 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | f11(B) != ordered_pair(C,D). [copy(90),flip(h),merge(e),unit_del(a,78),unit_del(b,78),unit_del(e,78),unit_del(f,78)]. 93 -ilf_type(A,subset_type(cross_product(B,C))) | ilf_type(A,binary_relation_type). [copy(92),unit_del(a,78),unit_del(b,78),unit_del(d,78)]. 95 -ilf_type(A,subset_type(cross_product(B,C))) | -member(D,A) | ordered_pair(f12(A,D),f13(A,D)) = D. [copy(94),unit_del(a,78),unit_del(b,78),unit_del(d,78),unit_del(e,78)]. 97 -empty(A) | ilf_type(A,binary_relation_type). [copy(96),merge(c),unit_del(b,78)]. 106 -member(A,B) | member(ordered_pair(A,A),identity_relation_of(B)). [factor(15,b,d),xx(e),unit_del(a,78),unit_del(b,78)]. 132 -member(power_set(A),power_set(A)) | member(power_set(A),A). [factor(51,d,f),merge(c),unit_del(a,78),unit_del(b,78)]. 148 -ilf_type(A,relation_type(B,C)) | ilf_type(range(B,C,A),subset_type(C)). [back_unit_del(77),unit_del(a,78),unit_del(b,78)]. 149 -ilf_type(A,relation_type(B,C)) | range(B,C,A) = range_of(A). [back_unit_del(76),unit_del(a,78),unit_del(b,78)]. 150 -ilf_type(A,relation_type(B,C)) | ilf_type(domain(B,C,A),subset_type(B)). [back_unit_del(75),unit_del(a,78),unit_del(b,78)]. 151 -ilf_type(A,relation_type(B,C)) | domain(B,C,A) = domain_of(A). [back_unit_del(74),unit_del(a,78),unit_del(b,78)]. 152 -member(A,B) | member(f18(B),B). [back_unit_del(73),unit_del(a,78),unit_del(b,78)]. 153 -member(A,B) | -empty(B). [back_unit_del(71),unit_del(a,78),unit_del(b,78)]. 154 empty(A) | member(f17(A),A). [back_unit_del(70),unit_del(a,78)]. 155 -member(A,B) | ordered_pair(f14(B,A),f15(B,A)) = A | f16(B) != ordered_pair(C,D). [back_unit_del(68),unit_del(a,78),unit_del(b,78),unit_del(e,78),unit_del(f,78)]. 156 -member(A,B) | ordered_pair(f14(B,A),f15(B,A)) = A | member(f16(B),B). [back_unit_del(66),unit_del(a,78),unit_del(b,78)]. 157 empty(A) | ilf_type(f10(A),member_type(A)). [back_unit_del(56),unit_del(b,78)]. 158 empty(A) | member(B,A) | -ilf_type(B,member_type(A)). [back_unit_del(55),unit_del(a,78),unit_del(c,78)]. 159 empty(A) | ilf_type(B,member_type(A)) | -member(B,A). [back_unit_del(54),unit_del(a,78),unit_del(c,78)]. 160 -empty(power_set(A)). [back_unit_del(52),unit_del(a,78)]. 161 -member(A,B) | member(A,C) | -member(B,power_set(C)). [back_unit_del(51),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. 162 member(A,power_set(B)) | -member(f9(A,B),B). [back_unit_del(50),unit_del(a,78),unit_del(b,78)]. 163 member(A,power_set(B)) | member(f9(A,B),A). [back_unit_del(49),unit_del(a,78),unit_del(b,78)]. 164 subset(A,A). [back_unit_del(46),unit_del(a,78)]. 165 ilf_type(f8(A),subset_type(A)). [back_unit_del(45),unit_del(a,78)]. 166 ilf_type(A,member_type(power_set(B))) | -ilf_type(A,subset_type(B)). [back_unit_del(44),unit_del(a,78),unit_del(b,78)]. 167 ilf_type(A,subset_type(B)) | -ilf_type(A,member_type(power_set(B))). [back_unit_del(43),unit_del(a,78),unit_del(b,78)]. 168 -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(37),unit_del(c,78),unit_del(d,78)]. 169 -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(36),unit_del(c,78),unit_del(d,78)]. 171 -member(A,B) | member(A,C) | -member(f3(B,C),C). [back_unit_del(28),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. 172 -member(A,B) | member(A,C) | member(f3(B,C),B). [back_unit_del(27),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. 173 -member(A,B) | member(A,C) | -subset(B,C). [back_unit_del(25),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. 174 subset(A,B) | -member(f2(A,B),B). [back_unit_del(24),unit_del(a,78),unit_del(b,78)]. 175 subset(A,B) | member(f2(A,B),A). [back_unit_del(23),unit_del(a,78),unit_del(b,78)]. 176 ilf_type(f1(A,B),relation_type(B,A)). [back_unit_del(21),unit_del(a,78),unit_del(b,78)]. 177 -ilf_type(A,relation_type(B,C)) | ilf_type(A,subset_type(cross_product(B,C))). [back_unit_del(20),unit_del(a,78),unit_del(b,78)]. 178 -ilf_type(A,subset_type(cross_product(B,C))) | ilf_type(A,relation_type(B,C)). [back_unit_del(19),unit_del(a,78),unit_del(b,78)]. 179 ilf_type(identity_relation_of(A),binary_relation_type). [back_unit_del(18),unit_del(a,78)]. 180 A = B | -member(ordered_pair(B,A),identity_relation_of(C)). [back_unit_del(17),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. 181 member(A,B) | -member(ordered_pair(A,C),identity_relation_of(B)). [back_unit_del(16),unit_del(a,78),unit_del(b,78),unit_del(d,78)]. 182 -member(A,B) | member(ordered_pair(A,C),identity_relation_of(B)) | C != A. [back_unit_del(15),unit_del(a,78),unit_del(b,78),unit_del(d,78)]. 183 -ilf_type(A,binary_relation_type) | -member(ordered_pair(B,C),A) | member(C,range_of(A)). [back_unit_del(12),unit_del(a,78),unit_del(b,78)]. 184 -ilf_type(A,binary_relation_type) | -member(ordered_pair(B,C),A) | member(B,domain_of(A)). [back_unit_del(11),unit_del(a,78),unit_del(b,78)]. 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): 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)),A). [assumption]. given #2 (I,wt=18): 32 -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): 42 ilf_type(c1,binary_relation_type). [assumption]. given #4 (I,wt=3): 78 ilf_type(A,set_type). [assumption]. given #5 (I,wt=5): 79 ilf_type(c5,relation_type(c2,c3)). [assumption]. given #6 (I,wt=4): 80 subset(identity_relation_of(c4),c5). [assumption]. given #7 (I,wt=6): 81 -subset(c4,domain(c2,c3,c5)). [assumption]. given #8 (I,wt=7): 83 member(f11(A),A) | ilf_type(A,binary_relation_type). [copy(82),merge(c),unit_del(a,78)]. given #9 (I,wt=9): 85 f11(A) != ordered_pair(B,C) | ilf_type(A,binary_relation_type). [copy(84),flip(d),merge(e),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. given #10 (I,wt=15): 87 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | -ilf_type(B,binary_relation_type). [copy(86),merge(e),unit_del(a,78),unit_del(b,78)]. given #11 (I,wt=16): 89 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | member(f11(B),B). [copy(88),merge(e),unit_del(a,78),unit_del(b,78)]. given #12 (I,wt=18): 91 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | f11(B) != ordered_pair(C,D). [copy(90),flip(h),merge(e),unit_del(a,78),unit_del(b,78),unit_del(e,78),unit_del(f,78)]. given #13 (I,wt=9): 93 -ilf_type(A,subset_type(cross_product(B,C))) | ilf_type(A,binary_relation_type). [copy(92),unit_del(a,78),unit_del(b,78),unit_del(d,78)]. given #14 (I,wt=18): 95 -ilf_type(A,subset_type(cross_product(B,C))) | -member(D,A) | ordered_pair(f12(A,D),f13(A,D)) = D. [copy(94),unit_del(a,78),unit_del(b,78),unit_del(d,78),unit_del(e,78)]. given #15 (I,wt=5): 97 -empty(A) | ilf_type(A,binary_relation_type). [copy(96),merge(c),unit_del(b,78)]. given #16 (I,wt=9): 106 -member(A,B) | member(ordered_pair(A,A),identity_relation_of(B)). [factor(15,b,d),xx(e),unit_del(a,78),unit_del(b,78)]. given #17 (I,wt=9): 132 -member(power_set(A),power_set(A)) | member(power_set(A),A). [factor(51,d,f),merge(c),unit_del(a,78),unit_del(b,78)]. given #18 (I,wt=12): 148 -ilf_type(A,relation_type(B,C)) | ilf_type(range(B,C,A),subset_type(C)). [back_unit_del(77),unit_del(a,78),unit_del(b,78)]. given #19 (I,wt=12): 149 -ilf_type(A,relation_type(B,C)) | range(B,C,A) = range_of(A). [back_unit_del(76),unit_del(a,78),unit_del(b,78)]. given #20 (I,wt=12): 150 -ilf_type(A,relation_type(B,C)) | ilf_type(domain(B,C,A),subset_type(B)). [back_unit_del(75),unit_del(a,78),unit_del(b,78)]. given #21 (I,wt=12): 151 -ilf_type(A,relation_type(B,C)) | domain(B,C,A) = domain_of(A). [back_unit_del(74),unit_del(a,78),unit_del(b,78)]. given #22 (I,wt=7): 152 -member(A,B) | member(f18(B),B). [back_unit_del(73),unit_del(a,78),unit_del(b,78)]. given #23 (I,wt=5): 153 -member(A,B) | -empty(B). [back_unit_del(71),unit_del(a,78),unit_del(b,78)]. given #24 (I,wt=6): 154 empty(A) | member(f17(A),A). [back_unit_del(70),unit_del(a,78)]. given #25 (I,wt=18): 155 -member(A,B) | ordered_pair(f14(B,A),f15(B,A)) = A | f16(B) != ordered_pair(C,D). [back_unit_del(68),unit_del(a,78),unit_del(b,78),unit_del(e,78),unit_del(f,78)]. given #26 (I,wt=16): 156 -member(A,B) | ordered_pair(f14(B,A),f15(B,A)) = A | member(f16(B),B). [back_unit_del(66),unit_del(a,78),unit_del(b,78)]. given #27 (I,wt=7): 157 empty(A) | ilf_type(f10(A),member_type(A)). [back_unit_del(56),unit_del(b,78)]. given #28 (I,wt=9): 158 empty(A) | member(B,A) | -ilf_type(B,member_type(A)). [back_unit_del(55),unit_del(a,78),unit_del(c,78)]. given #29 (I,wt=9): 159 empty(A) | ilf_type(B,member_type(A)) | -member(B,A). [back_unit_del(54),unit_del(a,78),unit_del(c,78)]. given #30 (I,wt=3): 160 -empty(power_set(A)). [back_unit_del(52),unit_del(a,78)]. given #31 (I,wt=10): 161 -member(A,B) | member(A,C) | -member(B,power_set(C)). [back_unit_del(51),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. given #32 (I,wt=9): 162 member(A,power_set(B)) | -member(f9(A,B),B). [back_unit_del(50),unit_del(a,78),unit_del(b,78)]. given #33 (I,wt=9): 163 member(A,power_set(B)) | member(f9(A,B),A). [back_unit_del(49),unit_del(a,78),unit_del(b,78)]. given #34 (I,wt=3): 164 subset(A,A). [back_unit_del(46),unit_del(a,78)]. given #35 (I,wt=5): 165 ilf_type(f8(A),subset_type(A)). [back_unit_del(45),unit_del(a,78)]. given #36 (I,wt=9): 166 ilf_type(A,member_type(power_set(B))) | -ilf_type(A,subset_type(B)). [back_unit_del(44),unit_del(a,78),unit_del(b,78)]. given #37 (I,wt=9): 167 ilf_type(A,subset_type(B)) | -ilf_type(A,member_type(power_set(B))). [back_unit_del(43),unit_del(a,78),unit_del(b,78)]. given #38 (I,wt=25): 168 -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(37),unit_del(c,78),unit_del(d,78)]. given #39 (I,wt=25): 169 -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(36),unit_del(c,78),unit_del(d,78)]. given #40 (I,wt=11): 171 -member(A,B) | member(A,C) | -member(f3(B,C),C). [back_unit_del(28),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. given #41 (I,wt=11): 172 -member(A,B) | member(A,C) | member(f3(B,C),B). [back_unit_del(27),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. given #42 (I,wt=9): 173 -member(A,B) | member(A,C) | -subset(B,C). [back_unit_del(25),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. given #43 (I,wt=8): 174 subset(A,B) | -member(f2(A,B),B). [back_unit_del(24),unit_del(a,78),unit_del(b,78)]. given #44 (I,wt=8): 175 subset(A,B) | member(f2(A,B),A). [back_unit_del(23),unit_del(a,78),unit_del(b,78)]. given #45 (I,wt=7): 176 ilf_type(f1(A,B),relation_type(B,A)). [back_unit_del(21),unit_del(a,78),unit_del(b,78)]. given #46 (I,wt=11): 177 -ilf_type(A,relation_type(B,C)) | ilf_type(A,subset_type(cross_product(B,C))). [back_unit_del(20),unit_del(a,78),unit_del(b,78)]. given #47 (I,wt=11): 178 -ilf_type(A,subset_type(cross_product(B,C))) | ilf_type(A,relation_type(B,C)). [back_unit_del(19),unit_del(a,78),unit_del(b,78)]. given #48 (I,wt=4): 179 ilf_type(identity_relation_of(A),binary_relation_type). [back_unit_del(18),unit_del(a,78)]. given #49 (I,wt=9): 180 A = B | -member(ordered_pair(B,A),identity_relation_of(C)). [back_unit_del(17),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. given #50 (I,wt=9): 181 member(A,B) | -member(ordered_pair(A,C),identity_relation_of(B)). [back_unit_del(16),unit_del(a,78),unit_del(b,78),unit_del(d,78)]. given #51 (I,wt=12): 182 -member(A,B) | member(ordered_pair(A,C),identity_relation_of(B)) | C != A. [back_unit_del(15),unit_del(a,78),unit_del(b,78),unit_del(d,78)]. given #52 (I,wt=12): 183 -ilf_type(A,binary_relation_type) | -member(ordered_pair(B,C),A) | member(C,range_of(A)). [back_unit_del(12),unit_del(a,78),unit_del(b,78)]. given #53 (I,wt=12): 184 -ilf_type(A,binary_relation_type) | -member(ordered_pair(B,C),A) | member(B,domain_of(A)). [back_unit_del(11),unit_del(a,78),unit_del(b,78)]. given #54 (T,wt=4): 210 member(A,power_set(A)). [resolve(163,b,162,b),merge(b)]. given #55 (T,wt=5): 190 ilf_type(range_of(c5),subset_type(c3)). [back_rewrite(188),rewrite(189(4))]. given #56 (A,wt=15): 185 -ilf_type(A,binary_relation_type) | subset(A,c1) | member(ordered_pair(f4(A,c1),f5(A,c1)),A). [resolve(42,a,31,b)]. given #57 (F,wt=4): 194 -subset(c4,domain_of(c5)). [back_rewrite(81),rewrite(192(5))]. given #58 (F,wt=7): 259 -member(f2(c4,domain_of(c5)),domain_of(c5)). [ur(174,a,194,a)]. given #59 (T,wt=5): 193 ilf_type(domain_of(c5),subset_type(c2)). [back_rewrite(191),rewrite(192(4))]. given #60 (T,wt=5): 249 ilf_type(A,member_type(power_set(A))). [resolve(210,a,159,c),unit_del(a,160)]. given #61 (A,wt=15): 186 -ilf_type(A,binary_relation_type) | subset(c1,A) | member(ordered_pair(f4(c1,A),f5(c1,A)),c1). [resolve(42,a,31,a)]. given #62 (F,wt=8): 261 -subset(power_set(f2(c4,domain_of(c5))),domain_of(c5)). [ur(173,a,210,a,b,259,a)]. given #63 (F,wt=9): 263 -member(power_set(f2(c4,domain_of(c5))),power_set(domain_of(c5))). [ur(161,a,210,a,b,259,a)]. given #64 (T,wt=4): 265 ilf_type(A,subset_type(A)). [resolve(249,a,167,b)]. given #65 (T,wt=5): 276 ilf_type(cross_product(A,B),binary_relation_type). [resolve(265,a,93,a)]. given #66 (A,wt=11): 187 member(ordered_pair(f11(A),f11(A)),identity_relation_of(A)) | ilf_type(A,binary_relation_type). [resolve(106,a,83,a)]. given #67 (F,wt=10): 260 -member(ordered_pair(f2(c4,domain_of(c5)),A),identity_relation_of(domain_of(c5))). [ur(181,a,259,a)]. given #68 (F,wt=10): 270 -subset(power_set(power_set(f2(c4,domain_of(c5)))),power_set(domain_of(c5))). [ur(173,a,210,a,b,263,a)]. given #69 (T,wt=6): 196 empty(A) | member(f18(A),A). [resolve(154,b,152,a)]. given #70 (T,wt=6): 203 empty(A) | member(f10(A),A). [resolve(158,c,157,b),merge(c)]. given #71 (A,wt=7): 189 range(c2,c3,c5) = range_of(c5). [resolve(149,a,79,a)]. given #72 (F,wt=10): 274 -ilf_type(power_set(f2(c4,domain_of(c5))),member_type(power_set(domain_of(c5)))). [ur(158,a,160,a,b,263,a)]. given #73 (F,wt=9): 321 -ilf_type(power_set(f2(c4,domain_of(c5))),subset_type(domain_of(c5))). [ur(166,a,274,a)]. given #74 (T,wt=6): 215 member(A,power_set(B)) | -empty(A). [resolve(163,b,153,a)]. given #75 (T,wt=6): 222 ilf_type(f8(cross_product(A,B)),binary_relation_type). [resolve(165,a,93,a)]. given #76 (A,wt=7): 192 domain(c2,c3,c5) = domain_of(c5). [resolve(151,a,79,a)]. given #77 (F,wt=11): 262 -member(f3(power_set(f2(c4,domain_of(c5))),domain_of(c5)),domain_of(c5)). [ur(171,a,210,a,b,259,a)]. given #78 (F,wt=11): 268 -member(f2(power_set(f2(c4,domain_of(c5))),domain_of(c5)),domain_of(c5)). [ur(174,a,261,a)]. given #79 (T,wt=6): 223 ilf_type(f8(A),member_type(power_set(A))). [resolve(166,b,165,a)]. given #80 (T,wt=5): 334 member(f8(A),power_set(A)). [resolve(223,a,158,c),unit_del(a,160)]. given #81 (A,wt=7): 195 member(f18(A),A) | ilf_type(A,binary_relation_type). [resolve(152,a,83,a)]. given #82 (F,wt=8): 348 -member(f2(c4,domain_of(c5)),f8(domain_of(c5))). [ur(161,b,259,a,c,334,a)]. given #83 (F,wt=9): 355 -subset(power_set(f2(c4,domain_of(c5))),f8(domain_of(c5))). [ur(173,a,210,a,b,348,a)]. given #84 (T,wt=6): 224 ilf_type(f10(power_set(A)),subset_type(A)). [resolve(167,b,157,b),unit_del(b,160)]. given #85 (T,wt=6): 238 ilf_type(c5,subset_type(cross_product(c2,c3))). [resolve(177,a,79,a)]. given #86 (A,wt=10): 197 empty(A) | member(ordered_pair(f17(A),f17(A)),identity_relation_of(A)). [resolve(154,b,106,a)]. given #87 (F,wt=9): 357 -member(f2(c4,domain_of(c5)),f8(f8(domain_of(c5)))). [ur(161,b,348,a,c,334,a)]. given #88 (F,wt=10): 345 -member(power_set(f2(c4,domain_of(c5))),f8(power_set(domain_of(c5)))). [ur(161,b,263,a,c,334,a)]. given #89 (T,wt=3): 365 ilf_type(c5,binary_relation_type). [resolve(238,a,93,a)]. given #90 (T,wt=5): 375 empty(A) | -empty(identity_relation_of(A)). [resolve(197,b,153,a)]. given #91 (A,wt=20): 198 empty(A) | -ilf_type(A,subset_type(cross_product(B,C))) | ordered_pair(f12(A,f17(A)),f13(A,f17(A))) = f17(A). [resolve(154,b,95,b)]. given #92 (F,wt=4): 398 -empty(identity_relation_of(power_set(A))). [ur(375,a,160,a)]. given #93 (F,wt=5): 403 -empty(identity_relation_of(identity_relation_of(power_set(A)))). [ur(375,a,398,a)]. given #94 (T,wt=6): 251 member(f18(power_set(A)),power_set(A)). [resolve(210,a,152,a)]. given #95 (T,wt=6): 256 ilf_type(range_of(c5),member_type(power_set(c3))). [resolve(190,a,166,b)]. given #96 (A,wt=18): 199 empty(A) | ordered_pair(f12(A,f17(A)),f13(A,f17(A))) = f17(A) | member(f11(A),A). [resolve(154,b,89,a)]. given #97 (F,wt=6): 404 -empty(identity_relation_of(identity_relation_of(identity_relation_of(power_set(A))))). [ur(375,a,403,a)]. given #98 (F,wt=7): 436 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(power_set(A)))))). [ur(375,a,404,a)]. given #99 (T,wt=5): 422 member(range_of(c5),power_set(c3)). [resolve(256,a,158,c),unit_del(a,160)]. given #100 (T,wt=6): 258 member(f2(c4,domain_of(c5)),c4). [resolve(194,a,175,a)]. given #101 (A,wt=17): 200 empty(A) | ordered_pair(f12(A,f17(A)),f13(A,f17(A))) = f17(A) | -ilf_type(A,binary_relation_type). [resolve(154,b,87,a)]. given #102 (F,wt=2): 452 -empty(c4). [resolve(258,a,153,a)]. given #103 (F,wt=3): 469 -empty(identity_relation_of(c4)). [ur(375,a,452,a)]. given #104 (T,wt=4): 453 member(f18(c4),c4). [resolve(258,a,152,a)]. given #105 (T,wt=5): 474 ilf_type(f18(c4),member_type(c4)). [resolve(453,a,159,c),unit_del(a,452)]. given #106 (A,wt=18): 201 ordered_pair(f14(A,f17(A)),f15(A,f17(A))) = f17(A) | member(f16(A),A) | empty(A). [resolve(156,a,154,b)]. given #107 (F,wt=4): 470 -empty(identity_relation_of(identity_relation_of(c4))). [ur(375,a,469,a)]. given #108 (F,wt=5): 459 -subset(c4,f8(domain_of(c5))). [ur(173,a,258,a,b,348,a)]. given #109 (T,wt=6): 264 ilf_type(domain_of(c5),member_type(power_set(c2))). [resolve(193,a,166,b)]. given #110 (T,wt=5): 496 member(domain_of(c5),power_set(c2)). [resolve(264,a,158,c),unit_del(a,160)]. given #111 (A,wt=19): 202 ordered_pair(f14(A,f11(A)),f15(A,f11(A))) = f11(A) | member(f16(A),A) | ilf_type(A,binary_relation_type). [resolve(156,a,83,a)]. given #112 (F,wt=5): 465 -member(c4,power_set(domain_of(c5))). [ur(161,a,258,a,b,259,a)]. given #113 (F,wt=5): 493 -empty(identity_relation_of(identity_relation_of(identity_relation_of(c4)))). [ur(375,a,470,a)]. given #114 (T,wt=6): 290 ilf_type(A,binary_relation_type) | -empty(identity_relation_of(A)). [resolve(187,a,153,a)]. given #115 (T,wt=7): 204 empty(A) | ilf_type(f17(A),member_type(A)). [resolve(159,c,154,b),merge(c)]. given #116 (A,wt=10): 205 empty(A) | ilf_type(f11(A),member_type(A)) | ilf_type(A,binary_relation_type). [resolve(159,c,83,a)]. given #117 (F,wt=6): 458 -subset(c4,f8(f8(domain_of(c5)))). [ur(173,a,258,a,b,357,a)]. given #118 (F,wt=6): 464 -member(c4,power_set(f8(domain_of(c5)))). [ur(161,a,258,a,b,348,a)]. given #119 (T,wt=6): 519 ilf_type(f17(power_set(A)),subset_type(A)). [resolve(204,b,167,b),unit_del(a,160)]. given #120 (T,wt=7): 231 -member(A,identity_relation_of(c4)) | member(A,c5). [resolve(173,c,80,a)]. given #121 (A,wt=10): 206 member(f17(A),B) | -member(A,power_set(B)) | empty(A). [resolve(161,a,154,b)]. given #122 (F,wt=6): 511 -subset(power_set(c4),power_set(domain_of(c5))). [ur(173,a,210,a,b,465,a)]. given #123 (F,wt=6): 514 -member(c4,f8(power_set(domain_of(c5)))). [ur(161,b,465,a,c,334,a)]. given #124 (T,wt=5): 535 member(f10(identity_relation_of(c4)),c5). [resolve(231,a,203,b),unit_del(b,469)]. given #125 (T,wt=4): 563 member(f18(c5),c5). [resolve(535,a,152,a)]. given #126 (A,wt=11): 207 member(f11(A),B) | -member(A,power_set(B)) | ilf_type(A,binary_relation_type). [resolve(161,a,83,a)]. given #127 (F,wt=2): 562 -empty(c5). [resolve(535,a,153,a)]. given #128 (F,wt=3): 587 -empty(identity_relation_of(c5)). [ur(375,a,562,a)]. given #129 (T,wt=5): 537 member(f18(identity_relation_of(c4)),c5). [resolve(231,a,196,b),unit_del(b,469)]. given #130 (T,wt=5): 540 member(f17(identity_relation_of(c4)),c5). [resolve(231,a,154,b),unit_del(b,469)]. given #131 (A,wt=8): 208 -member(A,f17(power_set(B))) | member(A,B). [resolve(161,c,154,b),unit_del(c,160)]. given #132 (F,wt=4): 588 -empty(identity_relation_of(identity_relation_of(c5))). [ur(375,a,587,a)]. given #133 (F,wt=5): 622 -empty(identity_relation_of(identity_relation_of(identity_relation_of(c5)))). [ur(375,a,588,a)]. given #134 (T,wt=5): 573 ilf_type(f18(c5),member_type(c5)). [resolve(563,a,159,c),unit_del(a,562)]. given #135 (T,wt=6): 568 ilf_type(f10(identity_relation_of(c4)),member_type(c5)). [back_unit_del(560),unit_del(a,562)]. given #136 (A,wt=12): 209 -member(A,f11(power_set(B))) | member(A,B) | ilf_type(power_set(B),binary_relation_type). [resolve(161,c,83,a)]. given #137 (F,wt=6): 517 -ilf_type(c4,member_type(power_set(domain_of(c5)))). [ur(158,a,160,a,b,465,a)]. given #138 (F,wt=5): 628 -ilf_type(c4,subset_type(domain_of(c5))). [ur(166,a,517,a)]. given #139 (T,wt=6): 592 ilf_type(f18(identity_relation_of(c4)),member_type(c5)). [resolve(537,a,159,c),unit_del(a,562)]. given #140 (T,wt=6): 601 ilf_type(f17(identity_relation_of(c4)),member_type(c5)). [resolve(540,a,159,c),unit_del(a,562)]. given #141 (A,wt=14): 211 member(power_set(A),power_set(B)) | -member(C,f9(power_set(A),B)) | member(C,A). [resolve(163,b,161,c)]. given #142 (F,wt=6): 518 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(c4))))). [ur(375,a,493,a)]. given #143 (F,wt=6): 623 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(c5))))). [ur(375,a,622,a)]. given #144 (T,wt=7): 234 ilf_type(domain_of(f1(A,B)),subset_type(B)). [resolve(176,a,150,a),rewrite(233(2))]. given #145 (T,wt=7): 236 ilf_type(range_of(f1(A,B)),subset_type(A)). [resolve(176,a,148,a),rewrite(235(2))]. given #146 (A,wt=13): 212 member(A,power_set(B)) | member(f9(A,B),C) | -member(A,power_set(C)). [resolve(163,b,161,a)]. given #147 (F,wt=7): 462 -member(f3(c4,domain_of(c5)),domain_of(c5)). [ur(171,a,258,a,b,259,a)]. given #148 (F,wt=7): 463 -member(c4,power_set(f8(f8(domain_of(c5))))). [ur(161,a,258,a,b,357,a)]. given #149 (T,wt=7): 252 member(ordered_pair(A,A),identity_relation_of(power_set(A))). [resolve(210,a,106,a)]. given #150 (T,wt=6): 665 member(A,domain_of(identity_relation_of(power_set(A)))). [resolve(252,a,184,b),unit_del(a,179)]. given #151 (A,wt=12): 213 member(A,power_set(B)) | empty(A) | ilf_type(f9(A,B),member_type(A)). [resolve(163,b,159,c)]. given #152 (F,wt=5): 692 -empty(domain_of(identity_relation_of(power_set(A)))). [resolve(665,a,153,a)]. given #153 (F,wt=6): 765 -empty(identity_relation_of(domain_of(identity_relation_of(power_set(A))))). [ur(375,a,692,a)]. given #154 (T,wt=6): 666 member(A,range_of(identity_relation_of(power_set(A)))). [resolve(252,a,183,b),unit_del(a,179)]. given #155 (T,wt=7): 275 ilf_type(cross_product(A,B),relation_type(A,B)). [resolve(265,a,178,a)]. given #156 (A,wt=23): 214 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(163,b,156,a)]. given #157 (F,wt=5): 776 -empty(range_of(identity_relation_of(power_set(A)))). [resolve(666,a,153,a)]. given #158 (F,wt=6): 840 -empty(identity_relation_of(range_of(identity_relation_of(power_set(A))))). [ur(375,a,776,a)]. given #159 (T,wt=7): 306 empty(A) | ilf_type(f18(A),member_type(A)). [resolve(196,b,159,c),merge(b)]. given #160 (T,wt=6): 842 ilf_type(f18(power_set(A)),subset_type(A)). [resolve(306,b,167,b),unit_del(a,160)]. given #161 (A,wt=8): 216 member(A,power_set(B)) | member(f18(A),A). [resolve(163,b,152,a)]. given #162 (F,wt=7): 513 -member(f9(c4,domain_of(c5)),domain_of(c5)). [ur(162,a,465,a)]. given #163 (F,wt=7): 515 -member(c4,f18(power_set(power_set(domain_of(c5))))). [ur(161,b,465,a,c,251,a)]. given #164 (T,wt=7): 337 -member(A,f8(B)) | member(A,B). [resolve(334,a,161,c)]. given #165 (T,wt=7): 362 ilf_type(f10(power_set(A)),member_type(power_set(A))). [resolve(224,a,166,b)]. given #166 (A,wt=14): 217 member(A,power_set(B)) | member(ordered_pair(f9(A,B),f9(A,B)),identity_relation_of(A)). [resolve(163,b,106,a)]. given #167 (F,wt=7): 516 -member(power_set(c4),power_set(power_set(domain_of(c5)))). [ur(161,a,210,a,b,465,a)]. given #168 (F,wt=7): 524 -subset(power_set(c4),power_set(f8(domain_of(c5)))). [ur(173,a,210,a,b,464,a)]. given #169 (T,wt=6): 906 member(f10(power_set(A)),power_set(A)). [resolve(362,a,158,c),unit_del(a,160)]. given #170 (T,wt=7): 363 ilf_type(f10(power_set(cross_product(A,B))),binary_relation_type). [resolve(224,a,93,a)]. given #171 (A,wt=25): 218 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(163,b,95,b)]. given #172 (F,wt=7): 527 -member(c4,f8(power_set(f8(domain_of(c5))))). [ur(161,b,464,a,c,334,a)]. given #173 (F,wt=7): 530 -ilf_type(c4,member_type(power_set(f8(domain_of(c5))))). [ur(158,a,160,a,b,464,a)]. given #174 (T,wt=7): 364 ilf_type(c5,member_type(power_set(cross_product(c2,c3)))). [resolve(238,a,166,b)]. given #175 (T,wt=6): 992 member(c5,power_set(cross_product(c2,c3))). [resolve(364,a,158,c),unit_del(a,160)]. given #176 (A,wt=23): 219 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(163,b,89,a)]. given #177 (F,wt=6): 991 -ilf_type(c4,subset_type(f8(domain_of(c5)))). [ur(166,a,530,a)]. given #178 (F,wt=7): 552 -subset(power_set(c4),f8(power_set(domain_of(c5)))). [ur(173,a,210,a,b,514,a)]. given #179 (T,wt=6): 994 member(f17(c5),cross_product(c2,c3)). [resolve(992,a,206,b),unit_del(b,562)]. given #180 (T,wt=7): 408 ilf_type(f18(power_set(A)),member_type(power_set(A))). [resolve(251,a,159,c),unit_del(a,160)]. given #181 (A,wt=22): 220 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(163,b,87,a)]. given #182 (F,wt=4): 1025 -empty(cross_product(c2,c3)). [resolve(994,a,153,a)]. given #183 (F,wt=5): 1034 -empty(identity_relation_of(cross_product(c2,c3))). [ur(375,a,1025,a)]. given #184 (T,wt=7): 440 -member(A,range_of(c5)) | member(A,c3). [resolve(422,a,161,c)]. given #185 (T,wt=7): 466 ilf_type(f2(c4,domain_of(c5)),member_type(c4)). [back_unit_del(450),unit_del(a,452)]. given #186 (A,wt=15): 221 member(power_set(power_set(A)),power_set(A)) | -member(power_set(power_set(A)),f9(power_set(power_set(A)),A)). [factor(211,a,c)]. given #187 (F,wt=6): 1035 -empty(identity_relation_of(identity_relation_of(cross_product(c2,c3)))). [ur(375,a,1034,a)]. given #188 (F,wt=7): 554 -member(c4,f8(f8(power_set(domain_of(c5))))). [ur(161,b,514,a,c,334,a)]. given #189 (T,wt=7): 494 member(f2(c4,f8(domain_of(c5))),c4). [resolve(459,a,175,a)]. given #190 (T,wt=7): 499 -member(A,domain_of(c5)) | member(A,c2). [resolve(496,a,161,c)]. given #191 (A,wt=14): 225 member(f9(A,B),C) | -member(f3(A,C),C) | member(A,power_set(B)). [resolve(171,a,163,b)]. given #192 (F,wt=7): 612 -member(c4,f17(power_set(power_set(domain_of(c5))))). [ur(208,b,465,a)]. given #193 (F,wt=7): 633 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(c4)))))). [ur(375,a,518,a)]. given #194 (T,wt=7): 509 member(f16(A),A) | ilf_type(A,binary_relation_type). [resolve(202,a,85,a(flip)),merge(c)]. given #195 (T,wt=7): 533 ilf_type(f17(power_set(A)),member_type(power_set(A))). [resolve(519,a,166,b)]. given #196 (A,wt=11): 226 member(f17(A),B) | -member(f3(A,B),B) | empty(A). [resolve(171,a,154,b)]. given #197 (F,wt=7): 634 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(c5)))))). [ur(375,a,623,a)]. given #198 (F,wt=7): 766 -empty(identity_relation_of(identity_relation_of(domain_of(identity_relation_of(power_set(A)))))). [ur(375,a,765,a)]. given #199 (T,wt=6): 1100 member(f17(power_set(A)),power_set(A)). [resolve(533,a,158,c),unit_del(a,160)]. given #200 (T,wt=7): 534 ilf_type(f17(power_set(cross_product(A,B))),binary_relation_type). [resolve(519,a,93,a)]. given #201 (A,wt=12): 227 member(f11(A),B) | -member(f3(A,B),B) | ilf_type(A,binary_relation_type). [resolve(171,a,83,a)]. given #202 (F,wt=7): 841 -empty(identity_relation_of(identity_relation_of(range_of(identity_relation_of(power_set(A)))))). [ur(375,a,840,a)]. given #203 (F,wt=7): 953 -member(c4,f10(power_set(power_set(domain_of(c5))))). [ur(161,b,465,a,c,906,a)]. given #204 (T,wt=7): 536 member(ordered_pair(f17(c4),f17(c4)),c5). [resolve(231,a,197,b),unit_del(b,452)]. given #205 (T,wt=5): 1134 member(f17(c4),domain_of(c5)). [resolve(536,a,184,b),unit_del(a,365)]. given #206 (A,wt=14): 228 member(f9(A,B),C) | member(f3(A,C),A) | member(A,power_set(B)). [resolve(172,a,163,b)]. given #207 (F,wt=3): 1153 -empty(domain_of(c5)). [resolve(1134,a,153,a)]. given #208 (F,wt=4): 1215 -empty(identity_relation_of(domain_of(c5))). [ur(375,a,1153,a)]. given #209 (T,wt=4): 1147 member(f17(c4),c2). [resolve(1134,a,499,a)]. given #210 (T,wt=4): 1229 member(f18(c2),c2). [resolve(1147,a,152,a)]. given #211 (A,wt=11): 229 member(f17(A),B) | member(f3(A,B),A) | empty(A). [resolve(172,a,154,b)]. given #212 (F,wt=2): 1228 -empty(c2). [resolve(1147,a,153,a)]. given #213 (F,wt=3): 1288 -empty(identity_relation_of(c2)). [ur(375,a,1228,a)]. given #214 (T,wt=5): 1135 member(f17(c4),range_of(c5)). [resolve(536,a,183,b),unit_del(a,365)]. given #215 (T,wt=4): 1290 member(f17(c4),c3). [resolve(1135,a,440,a)]. given #216 (A,wt=12): 230 member(f11(A),B) | member(f3(A,B),A) | ilf_type(A,binary_relation_type). [resolve(172,a,83,a)]. given #217 (F,wt=2): 1312 -empty(c3). [resolve(1290,a,153,a)]. given #218 (F,wt=3): 1296 -empty(range_of(c5)). [resolve(1135,a,153,a)]. given #219 (T,wt=4): 1313 member(f18(c3),c3). [resolve(1290,a,152,a)]. given #220 (T,wt=5): 1160 member(f18(domain_of(c5)),c2). [back_unit_del(1066),unit_del(b,1153)]. given #221 (A,wt=11): 232 member(f2(A,B),A) | -member(C,A) | member(C,B). [resolve(175,a,173,c)]. given #222 (F,wt=3): 1359 -empty(identity_relation_of(c3)). [ur(375,a,1312,a)]. given #223 (F,wt=4): 1289 -empty(identity_relation_of(identity_relation_of(c2))). [ur(375,a,1288,a)]. given #224 (T,wt=5): 1161 member(f10(domain_of(c5)),c2). [back_unit_del(1065),unit_del(b,1153)]. given #225 (T,wt=5): 1162 member(f17(domain_of(c5)),c2). [back_unit_del(541),unit_del(b,1153)]. given #226 (A,wt=11): 233 domain(A,B,f1(B,A)) = domain_of(f1(B,A)). [resolve(176,a,151,a)]. given #227 (F,wt=4): 1360 -empty(identity_relation_of(range_of(c5))). [ur(375,a,1296,a)]. given #228 (F,wt=4): 1426 -empty(identity_relation_of(identity_relation_of(c3))). [ur(375,a,1359,a)]. given #229 (T,wt=5): 1234 ilf_type(f17(c4),member_type(c2)). [back_unit_del(1226),unit_del(a,1228)]. given #230 (T,wt=5): 1238 ilf_type(f18(c2),member_type(c2)). [resolve(1229,a,159,c),unit_del(a,1228)]. given #231 (A,wt=11): 235 range(A,B,f1(B,A)) = range_of(f1(B,A)). [resolve(176,a,149,a)]. given #232 (F,wt=5): 1221 -empty(identity_relation_of(identity_relation_of(domain_of(c5)))). [ur(375,a,1215,a)]. given #233 (F,wt=5): 1427 -empty(identity_relation_of(identity_relation_of(identity_relation_of(c2)))). [ur(375,a,1289,a)]. given #234 (T,wt=5): 1304 member(f18(range_of(c5)),c3). [back_unit_del(1038),unit_del(b,1296)]. given #235 (T,wt=5): 1305 member(f10(range_of(c5)),c3). [back_unit_del(1037),unit_del(b,1296)]. given #236 (A,wt=8): 237 ilf_type(f1(A,B),subset_type(cross_product(B,A))). [resolve(177,a,176,a)]. given #237 (F,wt=5): 1448 -empty(identity_relation_of(identity_relation_of(range_of(c5)))). [ur(375,a,1360,a)]. given #238 (F,wt=5): 1449 -empty(identity_relation_of(identity_relation_of(identity_relation_of(c3)))). [ur(375,a,1426,a)]. given #239 (T,wt=5): 1306 member(f17(range_of(c5)),c3). [back_unit_del(542),unit_del(b,1296)]. given #240 (T,wt=5): 1318 ilf_type(f17(c4),member_type(c3)). [back_unit_del(1310),unit_del(a,1312)]. given #241 (A,wt=8): 239 ilf_type(f8(cross_product(A,B)),relation_type(A,B)). [resolve(178,a,165,a)]. given #242 (F,wt=6): 1450 -empty(identity_relation_of(identity_relation_of(identity_relation_of(domain_of(c5))))). [ur(375,a,1221,a)]. given #243 (F,wt=6): 1451 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(c2))))). [ur(375,a,1427,a)]. given #244 (T,wt=5): 1364 ilf_type(f18(c3),member_type(c3)). [resolve(1313,a,159,c),unit_del(a,1312)]. given #245 (T,wt=5): 1475 ilf_type(f1(A,B),binary_relation_type). [resolve(237,a,93,a)]. given #246 (A,wt=18): 240 -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(179,a,31,b)]. given #247 (F,wt=6): 1476 -empty(identity_relation_of(identity_relation_of(identity_relation_of(range_of(c5))))). [ur(375,a,1448,a)]. given #248 (F,wt=6): 1477 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(c3))))). [ur(375,a,1449,a)]. given #249 (T,wt=6): 1154 member(f18(domain_of(c5)),domain_of(c5)). [resolve(1134,a,152,a)]. given #250 (T,wt=6): 1159 ilf_type(f17(c4),member_type(domain_of(c5))). [back_unit_del(1151),unit_del(a,1153)]. given #251 (A,wt=19): 241 -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(179,a,31,a)]. given #252 (F,wt=7): 1040 -empty(identity_relation_of(identity_relation_of(identity_relation_of(cross_product(c2,c3))))). [ur(375,a,1035,a)]. given #253 (F,wt=7): 1492 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(domain_of(c5)))))). [ur(375,a,1450,a)]. given #254 (T,wt=6): 1163 member(f3(c4,domain_of(c5)),c4). [resolve(228,a,513,a),unit_del(b,465)]. given #255 (T,wt=6): 1297 member(f18(range_of(c5)),range_of(c5)). [resolve(1135,a,152,a)]. given #256 (A,wt=13): 242 -ilf_type(power_set(ordered_pair(A,B)),binary_relation_type) | member(A,domain_of(power_set(ordered_pair(A,B)))). [resolve(210,a,184,b)]. given #257 (F,wt=7): 1493 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(c2)))))). [ur(375,a,1451,a)]. given #258 (F,wt=7): 1505 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(range_of(c5)))))). [ur(375,a,1476,a)]. given #259 (T,wt=6): 1302 ilf_type(f17(c4),member_type(range_of(c5))). [back_unit_del(1294),unit_del(a,1296)]. given #260 (T,wt=6): 1373 ilf_type(f18(domain_of(c5)),member_type(c2)). [resolve(1160,a,159,c),unit_del(a,1228)]. given #261 (A,wt=13): 243 -ilf_type(power_set(ordered_pair(A,B)),binary_relation_type) | member(B,range_of(power_set(ordered_pair(A,B)))). [resolve(210,a,183,b)]. given #262 (F,wt=7): 1506 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(c3)))))). [ur(375,a,1477,a)]. given #263 (F,wt=8): 397 -member(ordered_pair(f2(c4,domain_of(c5)),A),c5). [ur(184,a,365,a,c,259,a)]. ============================== PROOF ================================= % Proof 1 at 0.13 (+ 0.00) seconds. % Length of proof is 33. % Level of proof is 7. % Maximum clause weight is 21. % Given clauses 263. 2 -ilf_type(A,set_type) | ilf_type(A,binary_relation_type) | -relation_like(A). [assumption]. 9 -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,subset_type(cross_product(A,B))) | relation_like(C). [assumption]. 11 -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,binary_relation_type) | -member(ordered_pair(A,B),C) | member(A,domain_of(C)). [assumption]. 15 -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]. 20 -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]. 23 -ilf_type(A,set_type) | -ilf_type(B,set_type) | subset(A,B) | member(f2(A,B),A). [assumption]. 24 -ilf_type(A,set_type) | -ilf_type(B,set_type) | subset(A,B) | -member(f2(A,B),B). [assumption]. 25 -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]. 74 -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,relation_type(A,B)) | domain(A,B,C) = domain_of(C). [assumption]. 78 ilf_type(A,set_type). [assumption]. 79 ilf_type(c5,relation_type(c2,c3)). [assumption]. 80 subset(identity_relation_of(c4),c5). [assumption]. 81 -subset(c4,domain(c2,c3,c5)). [assumption]. 92 -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)]. 93 -ilf_type(A,subset_type(cross_product(B,C))) | ilf_type(A,binary_relation_type). [copy(92),unit_del(a,78),unit_del(b,78),unit_del(d,78)]. 106 -member(A,B) | member(ordered_pair(A,A),identity_relation_of(B)). [factor(15,b,d),xx(e),unit_del(a,78),unit_del(b,78)]. 151 -ilf_type(A,relation_type(B,C)) | domain(B,C,A) = domain_of(A). [back_unit_del(74),unit_del(a,78),unit_del(b,78)]. 173 -member(A,B) | member(A,C) | -subset(B,C). [back_unit_del(25),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. 174 subset(A,B) | -member(f2(A,B),B). [back_unit_del(24),unit_del(a,78),unit_del(b,78)]. 175 subset(A,B) | member(f2(A,B),A). [back_unit_del(23),unit_del(a,78),unit_del(b,78)]. 177 -ilf_type(A,relation_type(B,C)) | ilf_type(A,subset_type(cross_product(B,C))). [back_unit_del(20),unit_del(a,78),unit_del(b,78)]. 184 -ilf_type(A,binary_relation_type) | -member(ordered_pair(B,C),A) | member(B,domain_of(A)). [back_unit_del(11),unit_del(a,78),unit_del(b,78)]. 192 domain(c2,c3,c5) = domain_of(c5). [resolve(151,a,79,a)]. 194 -subset(c4,domain_of(c5)). [back_rewrite(81),rewrite(192(5))]. 231 -member(A,identity_relation_of(c4)) | member(A,c5). [resolve(173,c,80,a)]. 238 ilf_type(c5,subset_type(cross_product(c2,c3))). [resolve(177,a,79,a)]. 258 member(f2(c4,domain_of(c5)),c4). [resolve(194,a,175,a)]. 259 -member(f2(c4,domain_of(c5)),domain_of(c5)). [ur(174,a,194,a)]. 365 ilf_type(c5,binary_relation_type). [resolve(238,a,93,a)]. 397 -member(ordered_pair(f2(c4,domain_of(c5)),A),c5). [ur(184,a,365,a,c,259,a)]. 454 member(ordered_pair(f2(c4,domain_of(c5)),f2(c4,domain_of(c5))),identity_relation_of(c4)). [resolve(258,a,106,a)]. 1557 -member(ordered_pair(f2(c4,domain_of(c5)),A),identity_relation_of(c4)). [ur(231,b,397,a)]. 1558 $F. [resolve(1557,a,454,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=263. Generated=2015. Kept=1535. proofs=1. Usable=261. Sos=1114. Demods=16. Limbo=1, Disabled=248. Hints=0. Weight_deleted=4. Literals_deleted=0. Forward_subsumed=476. Back_subsumed=99. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=16 (0 lex), Back_demodulated=3. Back_unit_deleted=56. Demod_attempts=18440. Demod_rewrites=21. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=1483. Nonunit_bsub_feature_tests=1496. Megabytes=2.39. User_CPU=0.13, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 3792 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) | (all D (- ilf_type(D,binary_relation_type) | - member(ordered_pair(B,C),D) | member(B,domain_of(D)))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,binary_relation_type) | - member(ordered_pair(B,C),D) | member(C,range_of(D)))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | member(C,B) | - member(ordered_pair(C,C),identity_relation_of(B)))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | member(ordered_pair(C,C),identity_relation_of(B)) | - member(C,B))))) & (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,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(B,C,D),domain_of(D)))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,relation_type(B,C)) | ilf_type(domain(B,C,D),subset_type(B)))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,relation_type(B,C)) | =(range(B,C,D),range_of(D)))))))) & (all B (- ilf_type(B,set_type) | (all C (- ilf_type(C,set_type) | (all D (- ilf_type(D,relation_type(B,C)) | ilf_type(range(B,C,D),subset_type(C)))))))) & (all B ilf_type(B,set_type)) & (exists B (ilf_type(B,set_type) & (exists C (ilf_type(C,set_type) & (exists D (ilf_type(D,set_type) & (exists E (ilf_type(E,relation_type(B,C)) & subset(identity_relation_of(D),E) & - subset(D,range(B,C,E))))))))))). Child search process 3793 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) | -ilf_type(C,binary_relation_type) | -member(ordered_pair(A,B),C) | member(A,domain_of(C)). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,binary_relation_type) | -member(ordered_pair(A,B),C) | member(B,range_of(C)). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | member(B,A) | -member(ordered_pair(B,B),identity_relation_of(A)). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | member(ordered_pair(B,B),identity_relation_of(A)) | -member(B,A). [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,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(A,B,C) = domain_of(C). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,relation_type(A,B)) | ilf_type(domain(A,B,C),subset_type(A)). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,relation_type(A,B)) | range(A,B,C) = range_of(C). [assumption]. -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,relation_type(A,B)) | ilf_type(range(A,B,C),subset_type(B)). [assumption]. ilf_type(A,set_type). [assumption]. ilf_type(c2,set_type). [assumption]. ilf_type(c3,set_type). [assumption]. ilf_type(c4,set_type). [assumption]. ilf_type(c5,relation_type(c2,c3)). [assumption]. subset(identity_relation_of(c4),c5). [assumption]. -subset(c4,range(c2,c3,c5)). [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, c5, 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). 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)),A). [assumption]. 32 -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]. 42 ilf_type(c1,binary_relation_type). [assumption]. 78 ilf_type(A,set_type). [assumption]. 79 ilf_type(c5,relation_type(c2,c3)). [assumption]. 80 subset(identity_relation_of(c4),c5). [assumption]. 81 -subset(c4,range(c2,c3,c5)). [assumption]. 83 member(f11(A),A) | ilf_type(A,binary_relation_type). [copy(82),merge(c),unit_del(a,78)]. 85 f11(A) != ordered_pair(B,C) | ilf_type(A,binary_relation_type). [copy(84),flip(d),merge(e),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. 87 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | -ilf_type(B,binary_relation_type). [copy(86),merge(e),unit_del(a,78),unit_del(b,78)]. 89 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | member(f11(B),B). [copy(88),merge(e),unit_del(a,78),unit_del(b,78)]. 91 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | f11(B) != ordered_pair(C,D). [copy(90),flip(h),merge(e),unit_del(a,78),unit_del(b,78),unit_del(e,78),unit_del(f,78)]. 93 -ilf_type(A,subset_type(cross_product(B,C))) | ilf_type(A,binary_relation_type). [copy(92),unit_del(a,78),unit_del(b,78),unit_del(d,78)]. 95 -ilf_type(A,subset_type(cross_product(B,C))) | -member(D,A) | ordered_pair(f12(A,D),f13(A,D)) = D. [copy(94),unit_del(a,78),unit_del(b,78),unit_del(d,78),unit_del(e,78)]. 97 -empty(A) | ilf_type(A,binary_relation_type). [copy(96),merge(c),unit_del(b,78)]. 106 -member(A,B) | member(ordered_pair(A,A),identity_relation_of(B)). [factor(15,b,d),xx(e),unit_del(a,78),unit_del(b,78)]. 132 -member(power_set(A),power_set(A)) | member(power_set(A),A). [factor(51,d,f),merge(c),unit_del(a,78),unit_del(b,78)]. 148 -ilf_type(A,relation_type(B,C)) | ilf_type(range(B,C,A),subset_type(C)). [back_unit_del(77),unit_del(a,78),unit_del(b,78)]. 149 -ilf_type(A,relation_type(B,C)) | range(B,C,A) = range_of(A). [back_unit_del(76),unit_del(a,78),unit_del(b,78)]. 150 -ilf_type(A,relation_type(B,C)) | ilf_type(domain(B,C,A),subset_type(B)). [back_unit_del(75),unit_del(a,78),unit_del(b,78)]. 151 -ilf_type(A,relation_type(B,C)) | domain(B,C,A) = domain_of(A). [back_unit_del(74),unit_del(a,78),unit_del(b,78)]. 152 -member(A,B) | member(f18(B),B). [back_unit_del(73),unit_del(a,78),unit_del(b,78)]. 153 -member(A,B) | -empty(B). [back_unit_del(71),unit_del(a,78),unit_del(b,78)]. 154 empty(A) | member(f17(A),A). [back_unit_del(70),unit_del(a,78)]. 155 -member(A,B) | ordered_pair(f14(B,A),f15(B,A)) = A | f16(B) != ordered_pair(C,D). [back_unit_del(68),unit_del(a,78),unit_del(b,78),unit_del(e,78),unit_del(f,78)]. 156 -member(A,B) | ordered_pair(f14(B,A),f15(B,A)) = A | member(f16(B),B). [back_unit_del(66),unit_del(a,78),unit_del(b,78)]. 157 empty(A) | ilf_type(f10(A),member_type(A)). [back_unit_del(56),unit_del(b,78)]. 158 empty(A) | member(B,A) | -ilf_type(B,member_type(A)). [back_unit_del(55),unit_del(a,78),unit_del(c,78)]. 159 empty(A) | ilf_type(B,member_type(A)) | -member(B,A). [back_unit_del(54),unit_del(a,78),unit_del(c,78)]. 160 -empty(power_set(A)). [back_unit_del(52),unit_del(a,78)]. 161 -member(A,B) | member(A,C) | -member(B,power_set(C)). [back_unit_del(51),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. 162 member(A,power_set(B)) | -member(f9(A,B),B). [back_unit_del(50),unit_del(a,78),unit_del(b,78)]. 163 member(A,power_set(B)) | member(f9(A,B),A). [back_unit_del(49),unit_del(a,78),unit_del(b,78)]. 164 subset(A,A). [back_unit_del(46),unit_del(a,78)]. 165 ilf_type(f8(A),subset_type(A)). [back_unit_del(45),unit_del(a,78)]. 166 ilf_type(A,member_type(power_set(B))) | -ilf_type(A,subset_type(B)). [back_unit_del(44),unit_del(a,78),unit_del(b,78)]. 167 ilf_type(A,subset_type(B)) | -ilf_type(A,member_type(power_set(B))). [back_unit_del(43),unit_del(a,78),unit_del(b,78)]. 168 -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(37),unit_del(c,78),unit_del(d,78)]. 169 -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(36),unit_del(c,78),unit_del(d,78)]. 171 -member(A,B) | member(A,C) | -member(f3(B,C),C). [back_unit_del(28),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. 172 -member(A,B) | member(A,C) | member(f3(B,C),B). [back_unit_del(27),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. 173 -member(A,B) | member(A,C) | -subset(B,C). [back_unit_del(25),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. 174 subset(A,B) | -member(f2(A,B),B). [back_unit_del(24),unit_del(a,78),unit_del(b,78)]. 175 subset(A,B) | member(f2(A,B),A). [back_unit_del(23),unit_del(a,78),unit_del(b,78)]. 176 ilf_type(f1(A,B),relation_type(B,A)). [back_unit_del(21),unit_del(a,78),unit_del(b,78)]. 177 -ilf_type(A,relation_type(B,C)) | ilf_type(A,subset_type(cross_product(B,C))). [back_unit_del(20),unit_del(a,78),unit_del(b,78)]. 178 -ilf_type(A,subset_type(cross_product(B,C))) | ilf_type(A,relation_type(B,C)). [back_unit_del(19),unit_del(a,78),unit_del(b,78)]. 179 ilf_type(identity_relation_of(A),binary_relation_type). [back_unit_del(18),unit_del(a,78)]. 180 A = B | -member(ordered_pair(B,A),identity_relation_of(C)). [back_unit_del(17),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. 181 member(A,B) | -member(ordered_pair(A,C),identity_relation_of(B)). [back_unit_del(16),unit_del(a,78),unit_del(b,78),unit_del(d,78)]. 182 -member(A,B) | member(ordered_pair(A,C),identity_relation_of(B)) | C != A. [back_unit_del(15),unit_del(a,78),unit_del(b,78),unit_del(d,78)]. 183 -ilf_type(A,binary_relation_type) | -member(ordered_pair(B,C),A) | member(C,range_of(A)). [back_unit_del(12),unit_del(a,78),unit_del(b,78)]. 184 -ilf_type(A,binary_relation_type) | -member(ordered_pair(B,C),A) | member(B,domain_of(A)). [back_unit_del(11),unit_del(a,78),unit_del(b,78)]. 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): 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)),A). [assumption]. given #2 (I,wt=18): 32 -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): 42 ilf_type(c1,binary_relation_type). [assumption]. given #4 (I,wt=3): 78 ilf_type(A,set_type). [assumption]. given #5 (I,wt=5): 79 ilf_type(c5,relation_type(c2,c3)). [assumption]. given #6 (I,wt=4): 80 subset(identity_relation_of(c4),c5). [assumption]. given #7 (I,wt=6): 81 -subset(c4,range(c2,c3,c5)). [assumption]. given #8 (I,wt=7): 83 member(f11(A),A) | ilf_type(A,binary_relation_type). [copy(82),merge(c),unit_del(a,78)]. given #9 (I,wt=9): 85 f11(A) != ordered_pair(B,C) | ilf_type(A,binary_relation_type). [copy(84),flip(d),merge(e),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. given #10 (I,wt=15): 87 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | -ilf_type(B,binary_relation_type). [copy(86),merge(e),unit_del(a,78),unit_del(b,78)]. given #11 (I,wt=16): 89 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | member(f11(B),B). [copy(88),merge(e),unit_del(a,78),unit_del(b,78)]. given #12 (I,wt=18): 91 -member(A,B) | ordered_pair(f12(B,A),f13(B,A)) = A | f11(B) != ordered_pair(C,D). [copy(90),flip(h),merge(e),unit_del(a,78),unit_del(b,78),unit_del(e,78),unit_del(f,78)]. given #13 (I,wt=9): 93 -ilf_type(A,subset_type(cross_product(B,C))) | ilf_type(A,binary_relation_type). [copy(92),unit_del(a,78),unit_del(b,78),unit_del(d,78)]. given #14 (I,wt=18): 95 -ilf_type(A,subset_type(cross_product(B,C))) | -member(D,A) | ordered_pair(f12(A,D),f13(A,D)) = D. [copy(94),unit_del(a,78),unit_del(b,78),unit_del(d,78),unit_del(e,78)]. given #15 (I,wt=5): 97 -empty(A) | ilf_type(A,binary_relation_type). [copy(96),merge(c),unit_del(b,78)]. given #16 (I,wt=9): 106 -member(A,B) | member(ordered_pair(A,A),identity_relation_of(B)). [factor(15,b,d),xx(e),unit_del(a,78),unit_del(b,78)]. given #17 (I,wt=9): 132 -member(power_set(A),power_set(A)) | member(power_set(A),A). [factor(51,d,f),merge(c),unit_del(a,78),unit_del(b,78)]. given #18 (I,wt=12): 148 -ilf_type(A,relation_type(B,C)) | ilf_type(range(B,C,A),subset_type(C)). [back_unit_del(77),unit_del(a,78),unit_del(b,78)]. given #19 (I,wt=12): 149 -ilf_type(A,relation_type(B,C)) | range(B,C,A) = range_of(A). [back_unit_del(76),unit_del(a,78),unit_del(b,78)]. given #20 (I,wt=12): 150 -ilf_type(A,relation_type(B,C)) | ilf_type(domain(B,C,A),subset_type(B)). [back_unit_del(75),unit_del(a,78),unit_del(b,78)]. given #21 (I,wt=12): 151 -ilf_type(A,relation_type(B,C)) | domain(B,C,A) = domain_of(A). [back_unit_del(74),unit_del(a,78),unit_del(b,78)]. given #22 (I,wt=7): 152 -member(A,B) | member(f18(B),B). [back_unit_del(73),unit_del(a,78),unit_del(b,78)]. given #23 (I,wt=5): 153 -member(A,B) | -empty(B). [back_unit_del(71),unit_del(a,78),unit_del(b,78)]. given #24 (I,wt=6): 154 empty(A) | member(f17(A),A). [back_unit_del(70),unit_del(a,78)]. given #25 (I,wt=18): 155 -member(A,B) | ordered_pair(f14(B,A),f15(B,A)) = A | f16(B) != ordered_pair(C,D). [back_unit_del(68),unit_del(a,78),unit_del(b,78),unit_del(e,78),unit_del(f,78)]. given #26 (I,wt=16): 156 -member(A,B) | ordered_pair(f14(B,A),f15(B,A)) = A | member(f16(B),B). [back_unit_del(66),unit_del(a,78),unit_del(b,78)]. given #27 (I,wt=7): 157 empty(A) | ilf_type(f10(A),member_type(A)). [back_unit_del(56),unit_del(b,78)]. given #28 (I,wt=9): 158 empty(A) | member(B,A) | -ilf_type(B,member_type(A)). [back_unit_del(55),unit_del(a,78),unit_del(c,78)]. given #29 (I,wt=9): 159 empty(A) | ilf_type(B,member_type(A)) | -member(B,A). [back_unit_del(54),unit_del(a,78),unit_del(c,78)]. given #30 (I,wt=3): 160 -empty(power_set(A)). [back_unit_del(52),unit_del(a,78)]. given #31 (I,wt=10): 161 -member(A,B) | member(A,C) | -member(B,power_set(C)). [back_unit_del(51),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. given #32 (I,wt=9): 162 member(A,power_set(B)) | -member(f9(A,B),B). [back_unit_del(50),unit_del(a,78),unit_del(b,78)]. given #33 (I,wt=9): 163 member(A,power_set(B)) | member(f9(A,B),A). [back_unit_del(49),unit_del(a,78),unit_del(b,78)]. given #34 (I,wt=3): 164 subset(A,A). [back_unit_del(46),unit_del(a,78)]. given #35 (I,wt=5): 165 ilf_type(f8(A),subset_type(A)). [back_unit_del(45),unit_del(a,78)]. given #36 (I,wt=9): 166 ilf_type(A,member_type(power_set(B))) | -ilf_type(A,subset_type(B)). [back_unit_del(44),unit_del(a,78),unit_del(b,78)]. given #37 (I,wt=9): 167 ilf_type(A,subset_type(B)) | -ilf_type(A,member_type(power_set(B))). [back_unit_del(43),unit_del(a,78),unit_del(b,78)]. given #38 (I,wt=25): 168 -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(37),unit_del(c,78),unit_del(d,78)]. given #39 (I,wt=25): 169 -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(36),unit_del(c,78),unit_del(d,78)]. given #40 (I,wt=11): 171 -member(A,B) | member(A,C) | -member(f3(B,C),C). [back_unit_del(28),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. given #41 (I,wt=11): 172 -member(A,B) | member(A,C) | member(f3(B,C),B). [back_unit_del(27),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. given #42 (I,wt=9): 173 -member(A,B) | member(A,C) | -subset(B,C). [back_unit_del(25),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. given #43 (I,wt=8): 174 subset(A,B) | -member(f2(A,B),B). [back_unit_del(24),unit_del(a,78),unit_del(b,78)]. given #44 (I,wt=8): 175 subset(A,B) | member(f2(A,B),A). [back_unit_del(23),unit_del(a,78),unit_del(b,78)]. given #45 (I,wt=7): 176 ilf_type(f1(A,B),relation_type(B,A)). [back_unit_del(21),unit_del(a,78),unit_del(b,78)]. given #46 (I,wt=11): 177 -ilf_type(A,relation_type(B,C)) | ilf_type(A,subset_type(cross_product(B,C))). [back_unit_del(20),unit_del(a,78),unit_del(b,78)]. given #47 (I,wt=11): 178 -ilf_type(A,subset_type(cross_product(B,C))) | ilf_type(A,relation_type(B,C)). [back_unit_del(19),unit_del(a,78),unit_del(b,78)]. given #48 (I,wt=4): 179 ilf_type(identity_relation_of(A),binary_relation_type). [back_unit_del(18),unit_del(a,78)]. given #49 (I,wt=9): 180 A = B | -member(ordered_pair(B,A),identity_relation_of(C)). [back_unit_del(17),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. given #50 (I,wt=9): 181 member(A,B) | -member(ordered_pair(A,C),identity_relation_of(B)). [back_unit_del(16),unit_del(a,78),unit_del(b,78),unit_del(d,78)]. given #51 (I,wt=12): 182 -member(A,B) | member(ordered_pair(A,C),identity_relation_of(B)) | C != A. [back_unit_del(15),unit_del(a,78),unit_del(b,78),unit_del(d,78)]. given #52 (I,wt=12): 183 -ilf_type(A,binary_relation_type) | -member(ordered_pair(B,C),A) | member(C,range_of(A)). [back_unit_del(12),unit_del(a,78),unit_del(b,78)]. given #53 (I,wt=12): 184 -ilf_type(A,binary_relation_type) | -member(ordered_pair(B,C),A) | member(B,domain_of(A)). [back_unit_del(11),unit_del(a,78),unit_del(b,78)]. given #54 (T,wt=4): 210 member(A,power_set(A)). [resolve(163,b,162,b),merge(b)]. given #55 (T,wt=5): 190 ilf_type(range_of(c5),subset_type(c3)). [back_rewrite(188),rewrite(189(4))]. given #56 (A,wt=15): 185 -ilf_type(A,binary_relation_type) | subset(A,c1) | member(ordered_pair(f4(A,c1),f5(A,c1)),A). [resolve(42,a,31,b)]. given #57 (F,wt=4): 191 -subset(c4,range_of(c5)). [back_rewrite(81),rewrite(189(5))]. given #58 (F,wt=7): 259 -member(f2(c4,range_of(c5)),range_of(c5)). [ur(174,a,191,a)]. given #59 (T,wt=5): 194 ilf_type(domain_of(c5),subset_type(c2)). [back_rewrite(192),rewrite(193(4))]. given #60 (T,wt=5): 249 ilf_type(A,member_type(power_set(A))). [resolve(210,a,159,c),unit_del(a,160)]. given #61 (A,wt=15): 186 -ilf_type(A,binary_relation_type) | subset(c1,A) | member(ordered_pair(f4(c1,A),f5(c1,A)),c1). [resolve(42,a,31,a)]. given #62 (F,wt=8): 261 -subset(power_set(f2(c4,range_of(c5))),range_of(c5)). [ur(173,a,210,a,b,259,a)]. given #63 (F,wt=9): 263 -member(power_set(f2(c4,range_of(c5))),power_set(range_of(c5))). [ur(161,a,210,a,b,259,a)]. given #64 (T,wt=4): 265 ilf_type(A,subset_type(A)). [resolve(249,a,167,b)]. given #65 (T,wt=5): 276 ilf_type(cross_product(A,B),binary_relation_type). [resolve(265,a,93,a)]. given #66 (A,wt=11): 187 member(ordered_pair(f11(A),f11(A)),identity_relation_of(A)) | ilf_type(A,binary_relation_type). [resolve(106,a,83,a)]. given #67 (F,wt=10): 260 -member(ordered_pair(f2(c4,range_of(c5)),A),identity_relation_of(range_of(c5))). [ur(181,a,259,a)]. given #68 (F,wt=10): 270 -subset(power_set(power_set(f2(c4,range_of(c5)))),power_set(range_of(c5))). [ur(173,a,210,a,b,263,a)]. given #69 (T,wt=6): 196 empty(A) | member(f18(A),A). [resolve(154,b,152,a)]. given #70 (T,wt=6): 203 empty(A) | member(f10(A),A). [resolve(158,c,157,b),merge(c)]. given #71 (A,wt=7): 189 range(c2,c3,c5) = range_of(c5). [resolve(149,a,79,a)]. given #72 (F,wt=10): 274 -ilf_type(power_set(f2(c4,range_of(c5))),member_type(power_set(range_of(c5)))). [ur(158,a,160,a,b,263,a)]. given #73 (F,wt=9): 321 -ilf_type(power_set(f2(c4,range_of(c5))),subset_type(range_of(c5))). [ur(166,a,274,a)]. given #74 (T,wt=6): 215 member(A,power_set(B)) | -empty(A). [resolve(163,b,153,a)]. given #75 (T,wt=6): 222 ilf_type(f8(cross_product(A,B)),binary_relation_type). [resolve(165,a,93,a)]. given #76 (A,wt=7): 193 domain(c2,c3,c5) = domain_of(c5). [resolve(151,a,79,a)]. given #77 (F,wt=11): 262 -member(f3(power_set(f2(c4,range_of(c5))),range_of(c5)),range_of(c5)). [ur(171,a,210,a,b,259,a)]. given #78 (F,wt=11): 268 -member(f2(power_set(f2(c4,range_of(c5))),range_of(c5)),range_of(c5)). [ur(174,a,261,a)]. given #79 (T,wt=6): 223 ilf_type(f8(A),member_type(power_set(A))). [resolve(166,b,165,a)]. given #80 (T,wt=5): 334 member(f8(A),power_set(A)). [resolve(223,a,158,c),unit_del(a,160)]. given #81 (A,wt=7): 195 member(f18(A),A) | ilf_type(A,binary_relation_type). [resolve(152,a,83,a)]. given #82 (F,wt=8): 348 -member(f2(c4,range_of(c5)),f8(range_of(c5))). [ur(161,b,259,a,c,334,a)]. given #83 (F,wt=9): 355 -subset(power_set(f2(c4,range_of(c5))),f8(range_of(c5))). [ur(173,a,210,a,b,348,a)]. given #84 (T,wt=6): 224 ilf_type(f10(power_set(A)),subset_type(A)). [resolve(167,b,157,b),unit_del(b,160)]. given #85 (T,wt=6): 238 ilf_type(c5,subset_type(cross_product(c2,c3))). [resolve(177,a,79,a)]. given #86 (A,wt=10): 197 empty(A) | member(ordered_pair(f17(A),f17(A)),identity_relation_of(A)). [resolve(154,b,106,a)]. given #87 (F,wt=9): 357 -member(f2(c4,range_of(c5)),f8(f8(range_of(c5)))). [ur(161,b,348,a,c,334,a)]. given #88 (F,wt=10): 345 -member(power_set(f2(c4,range_of(c5))),f8(power_set(range_of(c5)))). [ur(161,b,263,a,c,334,a)]. given #89 (T,wt=3): 365 ilf_type(c5,binary_relation_type). [resolve(238,a,93,a)]. given #90 (T,wt=5): 375 empty(A) | -empty(identity_relation_of(A)). [resolve(197,b,153,a)]. given #91 (A,wt=20): 198 empty(A) | -ilf_type(A,subset_type(cross_product(B,C))) | ordered_pair(f12(A,f17(A)),f13(A,f17(A))) = f17(A). [resolve(154,b,95,b)]. given #92 (F,wt=4): 398 -empty(identity_relation_of(power_set(A))). [ur(375,a,160,a)]. given #93 (F,wt=5): 403 -empty(identity_relation_of(identity_relation_of(power_set(A)))). [ur(375,a,398,a)]. given #94 (T,wt=6): 251 member(f18(power_set(A)),power_set(A)). [resolve(210,a,152,a)]. given #95 (T,wt=6): 256 ilf_type(range_of(c5),member_type(power_set(c3))). [resolve(190,a,166,b)]. given #96 (A,wt=18): 199 empty(A) | ordered_pair(f12(A,f17(A)),f13(A,f17(A))) = f17(A) | member(f11(A),A). [resolve(154,b,89,a)]. given #97 (F,wt=6): 404 -empty(identity_relation_of(identity_relation_of(identity_relation_of(power_set(A))))). [ur(375,a,403,a)]. given #98 (F,wt=7): 436 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(power_set(A)))))). [ur(375,a,404,a)]. given #99 (T,wt=5): 422 member(range_of(c5),power_set(c3)). [resolve(256,a,158,c),unit_del(a,160)]. given #100 (T,wt=6): 258 member(f2(c4,range_of(c5)),c4). [resolve(191,a,175,a)]. given #101 (A,wt=17): 200 empty(A) | ordered_pair(f12(A,f17(A)),f13(A,f17(A))) = f17(A) | -ilf_type(A,binary_relation_type). [resolve(154,b,87,a)]. given #102 (F,wt=2): 452 -empty(c4). [resolve(258,a,153,a)]. given #103 (F,wt=3): 469 -empty(identity_relation_of(c4)). [ur(375,a,452,a)]. given #104 (T,wt=4): 453 member(f18(c4),c4). [resolve(258,a,152,a)]. given #105 (T,wt=5): 474 ilf_type(f18(c4),member_type(c4)). [resolve(453,a,159,c),unit_del(a,452)]. given #106 (A,wt=18): 201 ordered_pair(f14(A,f17(A)),f15(A,f17(A))) = f17(A) | member(f16(A),A) | empty(A). [resolve(156,a,154,b)]. given #107 (F,wt=4): 470 -empty(identity_relation_of(identity_relation_of(c4))). [ur(375,a,469,a)]. given #108 (F,wt=5): 459 -subset(c4,f8(range_of(c5))). [ur(173,a,258,a,b,348,a)]. given #109 (T,wt=6): 264 ilf_type(domain_of(c5),member_type(power_set(c2))). [resolve(194,a,166,b)]. given #110 (T,wt=5): 496 member(domain_of(c5),power_set(c2)). [resolve(264,a,158,c),unit_del(a,160)]. given #111 (A,wt=19): 202 ordered_pair(f14(A,f11(A)),f15(A,f11(A))) = f11(A) | member(f16(A),A) | ilf_type(A,binary_relation_type). [resolve(156,a,83,a)]. given #112 (F,wt=5): 465 -member(c4,power_set(range_of(c5))). [ur(161,a,258,a,b,259,a)]. given #113 (F,wt=5): 493 -empty(identity_relation_of(identity_relation_of(identity_relation_of(c4)))). [ur(375,a,470,a)]. given #114 (T,wt=6): 290 ilf_type(A,binary_relation_type) | -empty(identity_relation_of(A)). [resolve(187,a,153,a)]. given #115 (T,wt=7): 204 empty(A) | ilf_type(f17(A),member_type(A)). [resolve(159,c,154,b),merge(c)]. given #116 (A,wt=10): 205 empty(A) | ilf_type(f11(A),member_type(A)) | ilf_type(A,binary_relation_type). [resolve(159,c,83,a)]. given #117 (F,wt=6): 458 -subset(c4,f8(f8(range_of(c5)))). [ur(173,a,258,a,b,357,a)]. given #118 (F,wt=6): 464 -member(c4,power_set(f8(range_of(c5)))). [ur(161,a,258,a,b,348,a)]. given #119 (T,wt=6): 519 ilf_type(f17(power_set(A)),subset_type(A)). [resolve(204,b,167,b),unit_del(a,160)]. given #120 (T,wt=7): 231 -member(A,identity_relation_of(c4)) | member(A,c5). [resolve(173,c,80,a)]. given #121 (A,wt=10): 206 member(f17(A),B) | -member(A,power_set(B)) | empty(A). [resolve(161,a,154,b)]. given #122 (F,wt=6): 511 -subset(power_set(c4),power_set(range_of(c5))). [ur(173,a,210,a,b,465,a)]. given #123 (F,wt=6): 514 -member(c4,f8(power_set(range_of(c5)))). [ur(161,b,465,a,c,334,a)]. given #124 (T,wt=5): 535 member(f10(identity_relation_of(c4)),c5). [resolve(231,a,203,b),unit_del(b,469)]. given #125 (T,wt=4): 563 member(f18(c5),c5). [resolve(535,a,152,a)]. given #126 (A,wt=11): 207 member(f11(A),B) | -member(A,power_set(B)) | ilf_type(A,binary_relation_type). [resolve(161,a,83,a)]. given #127 (F,wt=2): 562 -empty(c5). [resolve(535,a,153,a)]. given #128 (F,wt=3): 587 -empty(identity_relation_of(c5)). [ur(375,a,562,a)]. given #129 (T,wt=5): 537 member(f18(identity_relation_of(c4)),c5). [resolve(231,a,196,b),unit_del(b,469)]. given #130 (T,wt=5): 540 member(f17(identity_relation_of(c4)),c5). [resolve(231,a,154,b),unit_del(b,469)]. given #131 (A,wt=8): 208 -member(A,f17(power_set(B))) | member(A,B). [resolve(161,c,154,b),unit_del(c,160)]. given #132 (F,wt=4): 588 -empty(identity_relation_of(identity_relation_of(c5))). [ur(375,a,587,a)]. given #133 (F,wt=5): 622 -empty(identity_relation_of(identity_relation_of(identity_relation_of(c5)))). [ur(375,a,588,a)]. given #134 (T,wt=5): 573 ilf_type(f18(c5),member_type(c5)). [resolve(563,a,159,c),unit_del(a,562)]. given #135 (T,wt=6): 568 ilf_type(f10(identity_relation_of(c4)),member_type(c5)). [back_unit_del(560),unit_del(a,562)]. given #136 (A,wt=12): 209 -member(A,f11(power_set(B))) | member(A,B) | ilf_type(power_set(B),binary_relation_type). [resolve(161,c,83,a)]. given #137 (F,wt=6): 517 -ilf_type(c4,member_type(power_set(range_of(c5)))). [ur(158,a,160,a,b,465,a)]. given #138 (F,wt=5): 628 -ilf_type(c4,subset_type(range_of(c5))). [ur(166,a,517,a)]. given #139 (T,wt=6): 592 ilf_type(f18(identity_relation_of(c4)),member_type(c5)). [resolve(537,a,159,c),unit_del(a,562)]. given #140 (T,wt=6): 601 ilf_type(f17(identity_relation_of(c4)),member_type(c5)). [resolve(540,a,159,c),unit_del(a,562)]. given #141 (A,wt=14): 211 member(power_set(A),power_set(B)) | -member(C,f9(power_set(A),B)) | member(C,A). [resolve(163,b,161,c)]. given #142 (F,wt=6): 518 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(c4))))). [ur(375,a,493,a)]. given #143 (F,wt=6): 623 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(c5))))). [ur(375,a,622,a)]. given #144 (T,wt=7): 234 ilf_type(domain_of(f1(A,B)),subset_type(B)). [resolve(176,a,150,a),rewrite(233(2))]. given #145 (T,wt=7): 236 ilf_type(range_of(f1(A,B)),subset_type(A)). [resolve(176,a,148,a),rewrite(235(2))]. given #146 (A,wt=13): 212 member(A,power_set(B)) | member(f9(A,B),C) | -member(A,power_set(C)). [resolve(163,b,161,a)]. given #147 (F,wt=7): 462 -member(f3(c4,range_of(c5)),range_of(c5)). [ur(171,a,258,a,b,259,a)]. given #148 (F,wt=7): 463 -member(c4,power_set(f8(f8(range_of(c5))))). [ur(161,a,258,a,b,357,a)]. given #149 (T,wt=7): 252 member(ordered_pair(A,A),identity_relation_of(power_set(A))). [resolve(210,a,106,a)]. given #150 (T,wt=6): 665 member(A,domain_of(identity_relation_of(power_set(A)))). [resolve(252,a,184,b),unit_del(a,179)]. given #151 (A,wt=12): 213 member(A,power_set(B)) | empty(A) | ilf_type(f9(A,B),member_type(A)). [resolve(163,b,159,c)]. given #152 (F,wt=5): 692 -empty(domain_of(identity_relation_of(power_set(A)))). [resolve(665,a,153,a)]. given #153 (F,wt=6): 765 -empty(identity_relation_of(domain_of(identity_relation_of(power_set(A))))). [ur(375,a,692,a)]. given #154 (T,wt=6): 666 member(A,range_of(identity_relation_of(power_set(A)))). [resolve(252,a,183,b),unit_del(a,179)]. given #155 (T,wt=7): 275 ilf_type(cross_product(A,B),relation_type(A,B)). [resolve(265,a,178,a)]. given #156 (A,wt=23): 214 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(163,b,156,a)]. given #157 (F,wt=5): 776 -empty(range_of(identity_relation_of(power_set(A)))). [resolve(666,a,153,a)]. given #158 (F,wt=6): 840 -empty(identity_relation_of(range_of(identity_relation_of(power_set(A))))). [ur(375,a,776,a)]. given #159 (T,wt=7): 306 empty(A) | ilf_type(f18(A),member_type(A)). [resolve(196,b,159,c),merge(b)]. given #160 (T,wt=6): 842 ilf_type(f18(power_set(A)),subset_type(A)). [resolve(306,b,167,b),unit_del(a,160)]. given #161 (A,wt=8): 216 member(A,power_set(B)) | member(f18(A),A). [resolve(163,b,152,a)]. given #162 (F,wt=7): 513 -member(f9(c4,range_of(c5)),range_of(c5)). [ur(162,a,465,a)]. given #163 (F,wt=7): 515 -member(c4,f18(power_set(power_set(range_of(c5))))). [ur(161,b,465,a,c,251,a)]. given #164 (T,wt=7): 337 -member(A,f8(B)) | member(A,B). [resolve(334,a,161,c)]. given #165 (T,wt=7): 362 ilf_type(f10(power_set(A)),member_type(power_set(A))). [resolve(224,a,166,b)]. given #166 (A,wt=14): 217 member(A,power_set(B)) | member(ordered_pair(f9(A,B),f9(A,B)),identity_relation_of(A)). [resolve(163,b,106,a)]. given #167 (F,wt=7): 516 -member(power_set(c4),power_set(power_set(range_of(c5)))). [ur(161,a,210,a,b,465,a)]. given #168 (F,wt=7): 524 -subset(power_set(c4),power_set(f8(range_of(c5)))). [ur(173,a,210,a,b,464,a)]. given #169 (T,wt=6): 906 member(f10(power_set(A)),power_set(A)). [resolve(362,a,158,c),unit_del(a,160)]. given #170 (T,wt=7): 363 ilf_type(f10(power_set(cross_product(A,B))),binary_relation_type). [resolve(224,a,93,a)]. given #171 (A,wt=25): 218 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(163,b,95,b)]. given #172 (F,wt=7): 527 -member(c4,f8(power_set(f8(range_of(c5))))). [ur(161,b,464,a,c,334,a)]. given #173 (F,wt=7): 530 -ilf_type(c4,member_type(power_set(f8(range_of(c5))))). [ur(158,a,160,a,b,464,a)]. given #174 (T,wt=7): 364 ilf_type(c5,member_type(power_set(cross_product(c2,c3)))). [resolve(238,a,166,b)]. given #175 (T,wt=6): 992 member(c5,power_set(cross_product(c2,c3))). [resolve(364,a,158,c),unit_del(a,160)]. given #176 (A,wt=23): 219 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(163,b,89,a)]. given #177 (F,wt=6): 991 -ilf_type(c4,subset_type(f8(range_of(c5)))). [ur(166,a,530,a)]. given #178 (F,wt=7): 552 -subset(power_set(c4),f8(power_set(range_of(c5)))). [ur(173,a,210,a,b,514,a)]. given #179 (T,wt=6): 994 member(f17(c5),cross_product(c2,c3)). [resolve(992,a,206,b),unit_del(b,562)]. given #180 (T,wt=7): 408 ilf_type(f18(power_set(A)),member_type(power_set(A))). [resolve(251,a,159,c),unit_del(a,160)]. given #181 (A,wt=22): 220 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(163,b,87,a)]. given #182 (F,wt=4): 1025 -empty(cross_product(c2,c3)). [resolve(994,a,153,a)]. given #183 (F,wt=5): 1034 -empty(identity_relation_of(cross_product(c2,c3))). [ur(375,a,1025,a)]. given #184 (T,wt=7): 440 -member(A,range_of(c5)) | member(A,c3). [resolve(422,a,161,c)]. given #185 (T,wt=7): 466 ilf_type(f2(c4,range_of(c5)),member_type(c4)). [back_unit_del(450),unit_del(a,452)]. given #186 (A,wt=15): 221 member(power_set(power_set(A)),power_set(A)) | -member(power_set(power_set(A)),f9(power_set(power_set(A)),A)). [factor(211,a,c)]. given #187 (F,wt=6): 1035 -empty(identity_relation_of(identity_relation_of(cross_product(c2,c3)))). [ur(375,a,1034,a)]. given #188 (F,wt=7): 554 -member(c4,f8(f8(power_set(range_of(c5))))). [ur(161,b,514,a,c,334,a)]. given #189 (T,wt=7): 494 member(f2(c4,f8(range_of(c5))),c4). [resolve(459,a,175,a)]. given #190 (T,wt=7): 499 -member(A,domain_of(c5)) | member(A,c2). [resolve(496,a,161,c)]. given #191 (A,wt=14): 225 member(f9(A,B),C) | -member(f3(A,C),C) | member(A,power_set(B)). [resolve(171,a,163,b)]. given #192 (F,wt=7): 612 -member(c4,f17(power_set(power_set(range_of(c5))))). [ur(208,b,465,a)]. given #193 (F,wt=7): 633 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(c4)))))). [ur(375,a,518,a)]. given #194 (T,wt=7): 509 member(f16(A),A) | ilf_type(A,binary_relation_type). [resolve(202,a,85,a(flip)),merge(c)]. given #195 (T,wt=7): 533 ilf_type(f17(power_set(A)),member_type(power_set(A))). [resolve(519,a,166,b)]. given #196 (A,wt=11): 226 member(f17(A),B) | -member(f3(A,B),B) | empty(A). [resolve(171,a,154,b)]. given #197 (F,wt=7): 634 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(c5)))))). [ur(375,a,623,a)]. given #198 (F,wt=7): 766 -empty(identity_relation_of(identity_relation_of(domain_of(identity_relation_of(power_set(A)))))). [ur(375,a,765,a)]. given #199 (T,wt=6): 1100 member(f17(power_set(A)),power_set(A)). [resolve(533,a,158,c),unit_del(a,160)]. given #200 (T,wt=7): 534 ilf_type(f17(power_set(cross_product(A,B))),binary_relation_type). [resolve(519,a,93,a)]. given #201 (A,wt=12): 227 member(f11(A),B) | -member(f3(A,B),B) | ilf_type(A,binary_relation_type). [resolve(171,a,83,a)]. given #202 (F,wt=7): 841 -empty(identity_relation_of(identity_relation_of(range_of(identity_relation_of(power_set(A)))))). [ur(375,a,840,a)]. given #203 (F,wt=7): 953 -member(c4,f10(power_set(power_set(range_of(c5))))). [ur(161,b,465,a,c,906,a)]. given #204 (T,wt=7): 536 member(ordered_pair(f17(c4),f17(c4)),c5). [resolve(231,a,197,b),unit_del(b,452)]. given #205 (T,wt=5): 1134 member(f17(c4),domain_of(c5)). [resolve(536,a,184,b),unit_del(a,365)]. given #206 (A,wt=14): 228 member(f9(A,B),C) | member(f3(A,C),A) | member(A,power_set(B)). [resolve(172,a,163,b)]. given #207 (F,wt=3): 1153 -empty(domain_of(c5)). [resolve(1134,a,153,a)]. given #208 (F,wt=4): 1215 -empty(identity_relation_of(domain_of(c5))). [ur(375,a,1153,a)]. given #209 (T,wt=4): 1147 member(f17(c4),c2). [resolve(1134,a,499,a)]. given #210 (T,wt=4): 1223 member(f18(c2),c2). [resolve(1147,a,152,a)]. given #211 (A,wt=11): 229 member(f17(A),B) | member(f3(A,B),A) | empty(A). [resolve(172,a,154,b)]. given #212 (F,wt=2): 1222 -empty(c2). [resolve(1147,a,153,a)]. given #213 (F,wt=3): 1282 -empty(identity_relation_of(c2)). [ur(375,a,1222,a)]. given #214 (T,wt=5): 1135 member(f17(c4),range_of(c5)). [resolve(536,a,183,b),unit_del(a,365)]. given #215 (T,wt=4): 1284 member(f17(c4),c3). [resolve(1135,a,440,a)]. given #216 (A,wt=12): 230 member(f11(A),B) | member(f3(A,B),A) | ilf_type(A,binary_relation_type). [resolve(172,a,83,a)]. given #217 (F,wt=2): 1306 -empty(c3). [resolve(1284,a,153,a)]. given #218 (F,wt=3): 1290 -empty(range_of(c5)). [resolve(1135,a,153,a)]. given #219 (T,wt=4): 1307 member(f18(c3),c3). [resolve(1284,a,152,a)]. given #220 (T,wt=5): 1160 member(f18(domain_of(c5)),c2). [back_unit_del(1066),unit_del(b,1153)]. given #221 (A,wt=11): 232 member(f2(A,B),A) | -member(C,A) | member(C,B). [resolve(175,a,173,c)]. given #222 (F,wt=3): 1353 -empty(identity_relation_of(c3)). [ur(375,a,1306,a)]. given #223 (F,wt=4): 1283 -empty(identity_relation_of(identity_relation_of(c2))). [ur(375,a,1282,a)]. given #224 (T,wt=5): 1161 member(f10(domain_of(c5)),c2). [back_unit_del(1065),unit_del(b,1153)]. given #225 (T,wt=5): 1162 member(f17(domain_of(c5)),c2). [back_unit_del(541),unit_del(b,1153)]. given #226 (A,wt=11): 233 domain(A,B,f1(B,A)) = domain_of(f1(B,A)). [resolve(176,a,151,a)]. given #227 (F,wt=4): 1354 -empty(identity_relation_of(range_of(c5))). [ur(375,a,1290,a)]. given #228 (F,wt=4): 1425 -empty(identity_relation_of(identity_relation_of(c3))). [ur(375,a,1353,a)]. given #229 (T,wt=5): 1228 ilf_type(f17(c4),member_type(c2)). [back_unit_del(1220),unit_del(a,1222)]. given #230 (T,wt=5): 1232 ilf_type(f18(c2),member_type(c2)). [resolve(1223,a,159,c),unit_del(a,1222)]. given #231 (A,wt=11): 235 range(A,B,f1(B,A)) = range_of(f1(B,A)). [resolve(176,a,149,a)]. given #232 (F,wt=5): 1216 -empty(identity_relation_of(identity_relation_of(domain_of(c5)))). [ur(375,a,1215,a)]. given #233 (F,wt=5): 1426 -empty(identity_relation_of(identity_relation_of(identity_relation_of(c2)))). [ur(375,a,1283,a)]. given #234 (T,wt=5): 1298 member(f18(range_of(c5)),c3). [back_unit_del(1038),unit_del(b,1290)]. given #235 (T,wt=5): 1299 member(f10(range_of(c5)),c3). [back_unit_del(1037),unit_del(b,1290)]. given #236 (A,wt=8): 237 ilf_type(f1(A,B),subset_type(cross_product(B,A))). [resolve(177,a,176,a)]. given #237 (F,wt=5): 1447 -empty(identity_relation_of(identity_relation_of(range_of(c5)))). [ur(375,a,1354,a)]. given #238 (F,wt=5): 1449 -empty(identity_relation_of(identity_relation_of(identity_relation_of(c3)))). [ur(375,a,1425,a)]. given #239 (T,wt=5): 1300 member(f17(range_of(c5)),c3). [back_unit_del(542),unit_del(b,1290)]. given #240 (T,wt=5): 1312 ilf_type(f17(c4),member_type(c3)). [back_unit_del(1304),unit_del(a,1306)]. given #241 (A,wt=8): 239 ilf_type(f8(cross_product(A,B)),relation_type(A,B)). [resolve(178,a,165,a)]. given #242 (F,wt=6): 1450 -empty(identity_relation_of(identity_relation_of(identity_relation_of(domain_of(c5))))). [ur(375,a,1216,a)]. given #243 (F,wt=6): 1451 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(c2))))). [ur(375,a,1426,a)]. given #244 (T,wt=5): 1363 ilf_type(f18(c3),member_type(c3)). [resolve(1307,a,159,c),unit_del(a,1306)]. given #245 (T,wt=5): 1475 ilf_type(f1(A,B),binary_relation_type). [resolve(237,a,93,a)]. given #246 (A,wt=18): 240 -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(179,a,31,b)]. given #247 (F,wt=6): 1476 -empty(identity_relation_of(identity_relation_of(identity_relation_of(range_of(c5))))). [ur(375,a,1447,a)]. given #248 (F,wt=6): 1477 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(c3))))). [ur(375,a,1449,a)]. given #249 (T,wt=6): 1154 member(f18(domain_of(c5)),domain_of(c5)). [resolve(1134,a,152,a)]. given #250 (T,wt=6): 1159 ilf_type(f17(c4),member_type(domain_of(c5))). [back_unit_del(1151),unit_del(a,1153)]. given #251 (A,wt=19): 241 -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(179,a,31,a)]. given #252 (F,wt=7): 1040 -empty(identity_relation_of(identity_relation_of(identity_relation_of(cross_product(c2,c3))))). [ur(375,a,1035,a)]. given #253 (F,wt=7): 1492 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(domain_of(c5)))))). [ur(375,a,1450,a)]. given #254 (T,wt=6): 1163 member(f3(c4,range_of(c5)),c4). [resolve(228,a,513,a),unit_del(b,465)]. given #255 (T,wt=6): 1291 member(f18(range_of(c5)),range_of(c5)). [resolve(1135,a,152,a)]. given #256 (A,wt=13): 242 -ilf_type(power_set(ordered_pair(A,B)),binary_relation_type) | member(A,domain_of(power_set(ordered_pair(A,B)))). [resolve(210,a,184,b)]. given #257 (F,wt=7): 1493 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(c2)))))). [ur(375,a,1451,a)]. given #258 (F,wt=7): 1505 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(range_of(c5)))))). [ur(375,a,1476,a)]. given #259 (T,wt=6): 1296 ilf_type(f17(c4),member_type(range_of(c5))). [back_unit_del(1288),unit_del(a,1290)]. given #260 (T,wt=6): 1372 ilf_type(f18(domain_of(c5)),member_type(c2)). [resolve(1160,a,159,c),unit_del(a,1222)]. given #261 (A,wt=13): 243 -ilf_type(power_set(ordered_pair(A,B)),binary_relation_type) | member(B,range_of(power_set(ordered_pair(A,B)))). [resolve(210,a,183,b)]. given #262 (F,wt=7): 1506 -empty(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(identity_relation_of(c3)))))). [ur(375,a,1477,a)]. given #263 (F,wt=8): 397 -member(ordered_pair(A,f2(c4,range_of(c5))),c5). [ur(183,a,365,a,c,259,a)]. ============================== PROOF ================================= % Proof 1 at 0.12 (+ 0.01) seconds. % Length of proof is 33. % Level of proof is 7. % Maximum clause weight is 21. % Given clauses 263. 2 -ilf_type(A,set_type) | ilf_type(A,binary_relation_type) | -relation_like(A). [assumption]. 9 -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,subset_type(cross_product(A,B))) | relation_like(C). [assumption]. 12 -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,binary_relation_type) | -member(ordered_pair(A,B),C) | member(B,range_of(C)). [assumption]. 15 -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]. 20 -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]. 23 -ilf_type(A,set_type) | -ilf_type(B,set_type) | subset(A,B) | member(f2(A,B),A). [assumption]. 24 -ilf_type(A,set_type) | -ilf_type(B,set_type) | subset(A,B) | -member(f2(A,B),B). [assumption]. 25 -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]. 76 -ilf_type(A,set_type) | -ilf_type(B,set_type) | -ilf_type(C,relation_type(A,B)) | range(A,B,C) = range_of(C). [assumption]. 78 ilf_type(A,set_type). [assumption]. 79 ilf_type(c5,relation_type(c2,c3)). [assumption]. 80 subset(identity_relation_of(c4),c5). [assumption]. 81 -subset(c4,range(c2,c3,c5)). [assumption]. 92 -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)]. 93 -ilf_type(A,subset_type(cross_product(B,C))) | ilf_type(A,binary_relation_type). [copy(92),unit_del(a,78),unit_del(b,78),unit_del(d,78)]. 106 -member(A,B) | member(ordered_pair(A,A),identity_relation_of(B)). [factor(15,b,d),xx(e),unit_del(a,78),unit_del(b,78)]. 149 -ilf_type(A,relation_type(B,C)) | range(B,C,A) = range_of(A). [back_unit_del(76),unit_del(a,78),unit_del(b,78)]. 173 -member(A,B) | member(A,C) | -subset(B,C). [back_unit_del(25),unit_del(a,78),unit_del(b,78),unit_del(c,78)]. 174 subset(A,B) | -member(f2(A,B),B). [back_unit_del(24),unit_del(a,78),unit_del(b,78)]. 175 subset(A,B) | member(f2(A,B),A). [back_unit_del(23),unit_del(a,78),unit_del(b,78)]. 177 -ilf_type(A,relation_type(B,C)) | ilf_type(A,subset_type(cross_product(B,C))). [back_unit_del(20),unit_del(a,78),unit_del(b,78)]. 183 -ilf_type(A,binary_relation_type) | -member(ordered_pair(B,C),A) | member(C,range_of(A)). [back_unit_del(12),unit_del(a,78),unit_del(b,78)]. 189 range(c2,c3,c5) = range_of(c5). [resolve(149,a,79,a)]. 191 -subset(c4,range_of(c5)). [back_rewrite(81),rewrite(189(5))]. 231 -member(A,identity_relation_of(c4)) | member(A,c5). [resolve(173,c,80,a)]. 238 ilf_type(c5,subset_type(cross_product(c2,c3))). [resolve(177,a,79,a)]. 258 member(f2(c4,range_of(c5)),c4). [resolve(191,a,175,a)]. 259 -member(f2(c4,range_of(c5)),range_of(c5)). [ur(174,a,191,a)]. 365 ilf_type(c5,binary_relation_type). [resolve(238,a,93,a)]. 397 -member(ordered_pair(A,f2(c4,range_of(c5))),c5). [ur(183,a,365,a,c,259,a)]. 454 member(ordered_pair(f2(c4,range_of(c5)),f2(c4,range_of(c5))),identity_relation_of(c4)). [resolve(258,a,106,a)]. 1557 -member(ordered_pair(A,f2(c4,range_of(c5))),identity_relation_of(c4)). [ur(231,b,397,a)]. 1558 $F. [resolve(1557,a,454,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=263. Generated=2015. Kept=1535. proofs=1. Usable=261. Sos=1114. Demods=16. Limbo=1, Disabled=248. Hints=0. Weight_deleted=4. Literals_deleted=0. Forward_subsumed=476. Back_subsumed=99. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=16 (0 lex), Back_demodulated=3. Back_unit_deleted=56. Demod_attempts=18440. Demod_rewrites=21. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=1483. Nonunit_bsub_feature_tests=1496. Megabytes=2.40. User_CPU=0.12, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= Exiting with 1 proof. Process 3793 exit (max_proofs) Wed Nov 22 11:23:45 2006 ============================== end of multisearch ==================== All 2 subproblems have been proved, so we are done. Total user_CPU=0.26, system_CPU=0.02, wall_clock=0. THEOREM PROVED Exiting. Process 3791 exit (max_proofs) Wed Nov 22 11:23:45 2006