別のアプローチを使用して解決しました。コードを添付します（アルゴリズムはコード内にあります）。
前のいくつかの述語。ケースは残っていましたが（のようなtry_bind）。
コード：
% Author: Denis Korekov
% Description of algorithm:
% G1 is graph 1, G2 is graph 2
% E1 is edge of G1, E2 is edge of G2
% V1 is vertex of G1, V2 is vertex of G2
% 0) Check that graphs can be isomorphic (refer to "initial_verify" predicate)
% 1) Pick V1 and some V2 and remove them from vertices lists
% 2) Ensure that none of chosen vertices are in relative closed lists (otherwise continue but remove them)
% 3) Bind (map) V1 to V2
% 4) Expand V1 and V2
% 5) Ensure that degrees of expansions are the same
% 6) Append expansion results to the end of vertices lists and repeat
% define graph predicates here
% graph predicates end
% as we have undirected edges
way_g1(X, Y):- e(X, Y).
way_g1(X, Y):- e(Y, X).
way_g2(X, Y):- f(X, Y).
way_g2(X, Y):- f(Y, X).
% returns all vertices of graphs (non-repeating)
graph1_v(RES):-findall(X, way_g1(X, _), LS), nodes(LS, [], RES).
graph2_v(RES):-findall(X, way_g2(X, _), LS), nodes(LS, [], RES).
% returns all edges of graphs in form "e(X, Y)"
graph1_e(RES):-findall(edge(X, Y), e(X, Y), RES).
graph2_e(RES):-findall(edge(X, Y), f(X, Y), RES).
% returns a list of vertices (removes repeating vertices in a list)
% 1 - list of vertices
% 2 - closed list (discovered vertices)
% 3 - resulting list
nodes([], CL_LS, RES):-append(CL_LS, [], RES).
nodes([X|Rest], CL_LS, RES):- not(member(X, CL_LS)), nodes(Rest, .(X, CL_LS), RES).
nodes([X|Rest], CL_LS, RES):-member(X, CL_LS), nodes(Rest, CL_LS, RES).
% required predicate
iso:-graph1_v(V1), graph2_v(V2), graph1_e(E1), graph2_e(E2), initial_verify(V1, V2, E1, E2), iso_acc(V1, V2, [], [], [], _).
% same as above but outputs result (outputs resulting binding map)
iso_w:-graph1_v(V1), graph2_v(V2), graph1_e(E1), graph2_e(E2), initial_verify(V1, V2, E1, E2), iso_acc(V1, V2, [], [], [], RES_MAP), write(RES_MAP).
% initial verification that graphs at least CAN BE isomorphic
% checks the number of vertices and edges as well as degrees
% 1 - vertices of G1
% 2 - vertices of G2
% 3 - edges of G1
% 4 - edges of G2
initial_verify(X_V, Y_V, X_E, Y_E):-
length(X_V, X_VL),
length(Y_V, Y_VL),
X_VL=Y_VL,
length(X_E, X_EL),
length(Y_E, Y_EL),
X_EL=Y_EL,
get_degree_sequence_g1(X_V, [], X_S),
get_degree_sequence_g2(Y_V, [], Y_S),
%compare degree sequences
compare_lists(X_S, Y_S).
% main algorithm
% 1 - list of vertices of G1
% 2 - list of vertices of G2
% 3 - closed list of G1
% 4 - closed list of G2
% 5 - initial binding map
% 6 - resulting binding map
% if both vertices lists are empty -> isomorphic, backtrack and cut
iso_acc([], [], _, _, ISO_MAP, RES):-append(ISO_MAP, [], RES), !.
% otherwise for every node of G1, for every root of G2
iso_acc([X|X_Rest], Y_LS, CL_X, CL_Y, ISO_MAP, RES):-
select(Y, Y_LS, Y_Rest),
%if X or Y in closed -> continue (next predicate)
not(member(X, CL_X)),
not(member(Y, CL_Y)),
%map X to Y
try_bind(b(X, Y), ISO_MAP, UPD_MAP),
%expand X and Y, use CL_X and CL_Y
expand_g1(X, CL_X, CL_X_UPD, X_RES, X_L),
expand_g2(Y, CL_Y, CL_Y_UPD, Y_RES, Y_L),
%compare lengths of expansions
X_L=Y_L,
%if OK continue with iso_acc with new closed lists and new mapping
append(X_Rest, X_RES, X_NEW),
append(Y_Rest, Y_RES, Y_NEW),
iso_acc(X_NEW, Y_NEW, CL_X_UPD, CL_Y_UPD, UPD_MAP, RES).
% executed in case X and some Y are in closed list (skips such elements)
iso_acc([X|X_Rest], Y_LS, CL_X, CL_Y, ISO_MAP, RES):-
select(Y, Y_LS, Y_Rest),
member(X, CL_X),
member(Y, CL_Y),
iso_acc(X_Rest, Y_Rest, CL_X, CL_Y, ISO_MAP, RES).
% returns sorted degree sequence
% 1 - list of vertices
% 2 - current degree sequence
% 3 - resulting degree sequence
get_degree_sequence_g1([], DEG_S, RES):-
insert_sort(DEG_S, RES).
get_degree_sequence_g1([X|Rest], DEG_S, RES):-
findall(X, way_g1(X, _), LS),
length(LS, L),
append([L], DEG_S, DEG_S_UPD),
get_degree_sequence_g1(Rest, DEG_S_UPD, RES).
get_degree_sequence_g2([], DEG_S, RES):-
insert_sort(DEG_S, RES).
get_degree_sequence_g2([X|Rest], DEG_S, RES):-
findall(X, way_g2(X, _), LS),
length(LS, L),
append([L], DEG_S, DEG_S_UPD),
get_degree_sequence_g2(Rest, DEG_S_UPD, RES).
% compares two lists element by element
compare_lists([], []).
compare_lists([X|X_Rest], [Y|Y_Rest]):-
X=Y,
compare_lists(X_Rest, Y_Rest).
% checks whether binding exist, if not adds it (binding cannot be added if some other binding referring to same
% variables exists already (i.e. (1, 2) cannot be added if (2, 2) exists)
% 1 - binding to add / check in form "b(X, Y)"
% 2 - initial binding map
% 3 - resulting binding map (may remain the same)
try_bind(b(X, Y), MAP, MAP):-
member(b(X, Z), MAP),
Z=Y,
member(b(W, Y), MAP),
W=X.
try_bind(b(X, Y), MAP, UPD_MAP):-
not(member(b(X, _), MAP)),
not(member(b(_, Y), MAP)),
append([b(X, Y)], MAP, UPD_MAP).
% returns updated closed list (X goes to CL), children of X, Length of children, TODO: members of closed lists should not be repeated.
% 1 - Node to expand
% 2 - initial closed list
% 3 - updated closed list (result)
% 4 - updated binding map (result)
% 5 - quantity of children (result)
expand_g1(X, CL, CL_UPD, RES, L):-
findall(Y, (way_g1(X, Y), (not(member(Y, CL)))), LS),
%set results
append(LS, [], RES),
%update closed list
append([X], CL, CL_UPD),
%set length
length(RES, L).
expand_g2(X, CL, CL_UPD, RES, L):-
findall(Y, (way_g2(X, Y), (not(member(Y, CL)))), LS),
%set results
append(LS, [], RES),
%update closed list
append([X], CL, CL_UPD),
%set length
length(RES, L).
% sort algorithm, used in degree sequence verification (simple insertion sort)
% 1 - list to sort
% 2 - result
insert_sort(LS, RES):-insert_sort_acc(LS, [], RES).
insert_sort_acc([], RES, RES).
insert_sort_acc([X|Rest], LS, RES):-insert(X, LS, RES1), insert_sort_acc(Rest, RES1, RES).
% insert item at list
% 1 - item to insert
% 2 - list to insert to
% 3 - result
insert(X,[],[X]).
insert(X, [Y|Rest], [X, Y|Rest]):-X=<Y, !.
insert(X, [Y|Y_Rest], [Y|RES_Rest]):-insert(X, Y_Rest, RES_Rest).