MAYBE Left Termination proof of ../tpdb/LP/talp/maria/bid.pl
Left Termination of the query pattern bid_in_4(g, a, a, a) w.r.t. the given Prolog program could not be shown:



↳ Prolog
  ↳ PredefinedPredicateTransformerProof

Clauses:

bid(Hand, Attributes, Points, Bid) :- ','(sort_hand(Hand, SortedHand), ','(evaluate(SortedHand, Attributes, Points), make_bid(SortedHand, Attributes, Points, Bid))).
evaluate(Hand, [], P) :- ','(hcp(Hand, 0, HCP), ','(adjustments(Hand, MP), is(P, +(HCP, MP)))).
adjustments(_, 0).
make_bid(Hand, Attributes, Points, 'punt...').
hcp([], N, N).
hcp(.(=(_X, C), Sn), Ni, No) :- ','(hcp_suit(C, N), ','(is(Nt, +(N, Ni)), hcp(Sn, Nt, No))).
hcp_suit(S, P) :- ','(honors(S, 0, HP), ','(dist(S, DP), ','(misc(S, MP), is(P, +(HP, +(DP, MP)))))).
honors([], Pi, Pi).
honors(.(C1, Cn), Pi, Po) :- ','(honor(C1, P), ','(>(P, 0), ','(is(Pt, +(P, Pi)), honors(Cn, Pt, Po)))).
honors(.(C1, Cn), Pi, Pi) :- honor(C1, 0).
honor(C, N) :- face_card(C, N).
honor(C, 0) :- integer(C).
face_card(ace, 4).
face_card(king, 3).
face_card(queen, 2).
face_card(jack, 1).
dist([], 3).
dist(.(_, []), 2).
dist(.(_, .(_, [])), 1).
dist(.(_, .(_, .(_, _))), 0).
misc(.(ace, []), -1).
misc(.(king, []), -2).
misc(.(queen, .(_, [])), -2).
misc(.(jack, .(_, [])), -1).
misc(.(_X, .(_Y, .(H3, Rem))), P) :- ','(honor(H3, X), ','(>(X, 0), ','(length(Rem, N), ','(>(N, 2), is(P, -(N, 2)))))).
misc(_, 0).
sort_hand(Hand, SortedHand) :- ','(split_suits(Hand, SplitHand), sort_suits(SplitHand, SortedHand)).
split_suits(Hand, .(=(spades, S), .(=(hearts, H), .(=(diamonds, D), .(=(clubs, C), []))))) :- ','(filter(Hand, spades, S), ','(filter(Hand, hearts, H), ','(filter(Hand, diamonds, D), filter(Hand, clubs, C)))).
filter([], _, []).
filter(.(-(Card, Suit), In), Suit, .(Card, Out)) :- filter(In, Suit, Out).
filter(.(-(_A, X), In), Suit, Out) :- ','(\==(Suit, X), filter(In, Suit, Out)).
sort_suits([], []).
sort_suits(.(=(S, Ci), In), .(=(S, Co), Out)) :- ','(i_sort(Ci, [], Co), sort_suits(In, Out)).
i_sort([], L, L).
i_sort(.(C1, Cn), Li, Lo) :- ','(insert(C1, Li, Lt), i_sort(Cn, Lt, Lo)).
insert(X, [], .(X, [])).
insert(X, .(Y, Z), .(X, .(Y, Z))) :- higher(X, Y).
insert(X, .(Y, Z), .(Y, L)) :- ','(lower(X, Y), insert(X, Z, L)).
higher(ace, _).
higher(king, X) :- \==(X, ace).
higher(queen, X) :- ','(\==(X, ace), \==(X, king)).
higher(jack, X) :- integer(X).
higher(jack, jack).
higher(X, Y) :- ','(integer(X), ','(integer(Y), >=(X, Y))).
lower(king, ace).
lower(queen, X) :- ','(honor(X, N), >(N, 2)).
lower(jack, X) :- ','(honor(X, N), >(N, 1)).
lower(X, Y) :- ','(integer(X), honor(Y, _M)).
lower(X, Y) :- ','(integer(X), ','(integer(Y), <(X, Y))).
goal :- bid(.(-(ace, clubs), .(-(3, hearts), .(-(4, spades), .(-(4, diamonds), .(-(king, clubs), .(-(jack, hearts), .(-(ace, spades), .(-(ace, hearts), .(-(10, clubs), .(-(9, clubs), .(-(6, clubs), .(-(queen, diamonds), .(-(king, spades), []))))))))))))), Attr, Pts, Bid).

Queries:

bid(g,a,a,a).

Added definitions of predefined predicates.

↳ Prolog
  ↳ PredefinedPredicateTransformerProof
    ↳ Prolog
      ↳ OrTransformerProof

Clauses:

bid(Hand, Attributes, Points, Bid) :- ','(sort_hand(Hand, SortedHand), ','(evaluate(SortedHand, Attributes, Points), make_bid(SortedHand, Attributes, Points, Bid))).
evaluate(Hand, [], P) :- ','(hcp(Hand, zero, HCP), ','(adjustments(Hand, MP), ','(isPlus(HCP, MP, U), =(P, U)))).
adjustments(_, zero).
make_bid(Hand, Attributes, Points, 'punt...').
hcp([], N, N).
hcp(.(=(_X, C), Sn), Ni, No) :- ','(hcp_suit(C, N), ','(','(isPlus(N, Ni, U), =(Nt, U)), hcp(Sn, Nt, No))).
hcp_suit(S, P) :- ','(honors(S, zero, HP), ','(dist(S, DP), ','(misc(S, MP), ','(isPlus(DP, MP, U), ','(isPlus(HP, U, U1), =(P, U1)))))).
honors([], Pi, Pi).
honors(.(C1, Cn), Pi, Po) :- ','(honor(C1, P), ','(','(=(X, P), ','(=(X1, zero), isGreater(X, X1))), ','(','(isPlus(P, Pi, U), =(Pt, U)), honors(Cn, Pt, Po)))).
honors(.(C1, Cn), Pi, Pi) :- honor(C1, zero).
honor(C, N) :- face_card(C, N).
honor(C, zero) :- integer(C).
face_card(ace, succ(succ(succ(succ(zero))))).
face_card(king, succ(succ(succ(zero)))).
face_card(queen, succ(succ(zero))).
face_card(jack, succ(zero)).
dist([], succ(succ(succ(zero)))).
dist(.(_, []), succ(succ(zero))).
dist(.(_, .(_, [])), succ(zero)).
dist(.(_, .(_, .(_, _))), zero).
misc(.(ace, []), pred(zero)).
misc(.(king, []), pred(pred(zero))).
misc(.(queen, .(_, [])), pred(pred(zero))).
misc(.(jack, .(_, [])), pred(zero)).
misc(.(_X, .(_Y, .(H3, Rem))), P) :- ','(honor(H3, X), ','(','(=(X1, X), ','(=(X2, zero), isGreater(X1, X2))), ','(length(Rem, N), ','(','(=(X3, N), ','(=(X4, succ(succ(zero))), isGreater(X3, X4))), ','(isMinus(N, succ(succ(zero)), U), =(P, U)))))).
misc(_, zero).
sort_hand(Hand, SortedHand) :- ','(split_suits(Hand, SplitHand), sort_suits(SplitHand, SortedHand)).
split_suits(Hand, .(=(spades, S), .(=(hearts, H), .(=(diamonds, D), .(=(clubs, C), []))))) :- ','(filter(Hand, spades, S), ','(filter(Hand, hearts, H), ','(filter(Hand, diamonds, D), filter(Hand, clubs, C)))).
filter([], _, []).
filter(.(-(Card, Suit), In), Suit, .(Card, Out)) :- filter(In, Suit, Out).
filter(.(-(_A, X), In), Suit, Out) :- ','(\==(Suit, X), filter(In, Suit, Out)).
sort_suits([], []).
sort_suits(.(=(S, Ci), In), .(=(S, Co), Out)) :- ','(i_sort(Ci, [], Co), sort_suits(In, Out)).
i_sort([], L, L).
i_sort(.(C1, Cn), Li, Lo) :- ','(insert(C1, Li, Lt), i_sort(Cn, Lt, Lo)).
insert(X, [], .(X, [])).
insert(X, .(Y, Z), .(X, .(Y, Z))) :- higher(X, Y).
insert(X, .(Y, Z), .(Y, L)) :- ','(lower(X, Y), insert(X, Z, L)).
higher(ace, _).
higher(king, X) :- \==(X, ace).
higher(queen, X) :- ','(\==(X, ace), \==(X, king)).
higher(jack, X) :- integer(X).
higher(jack, jack).
higher(X, Y) :- ','(integer(X), ','(integer(Y), ','(=(X1, X), ','(=(X2, Y), ;(=(X1, X2), isGreater(X1, X2)))))).
lower(king, ace).
lower(queen, X) :- ','(honor(X, N), ','(=(X1, N), ','(=(X2, succ(succ(zero))), isGreater(X1, X2)))).
lower(jack, X) :- ','(honor(X, N), ','(=(X1, N), ','(=(X2, succ(zero)), isGreater(X1, X2)))).
lower(X, Y) :- ','(integer(X), honor(Y, _M)).
lower(X, Y) :- ','(integer(X), ','(integer(Y), ','(=(X1, X), ','(=(X2, Y), isLess(X1, X2))))).
goal :- bid(.(-(ace, clubs), .(-(succ(succ(succ(zero))), hearts), .(-(succ(succ(succ(succ(zero)))), spades), .(-(succ(succ(succ(succ(zero)))), diamonds), .(-(king, clubs), .(-(jack, hearts), .(-(ace, spades), .(-(ace, hearts), .(-(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))))), clubs), .(-(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), clubs), .(-(succ(succ(succ(succ(succ(succ(zero)))))), clubs), .(-(queen, diamonds), .(-(king, spades), []))))))))))))), Attr, Pts, Bid).
isPlus(zero, X, X).
isPlus(succ(X), zero, succ(X)).
isPlus(succ(X), succ(Y), succ(succ(Z))) :- isPlus(X, Y, Z).
isPlus(succ(X), pred(Y), Z) :- isPlus(X, Y, Z).
isPlus(pred(X), zero, pred(X)).
isPlus(pred(X), succ(Y), Z) :- isPlus(X, Y, Z).
isPlus(pred(X), pred(Y), pred(pred(Z))) :- isPlus(X, Y, Z).
isMinus(X, zero, X).
isMinus(zero, succ(Y), pred(Z)) :- isMinus(zero, Y, Z).
isMinus(zero, pred(Y), succ(Z)) :- isMinus(zero, Y, Z).
isMinus(succ(X), succ(Y), Z) :- isMinus(X, Y, Z).
isMinus(succ(X), pred(Y), succ(succ(Z))) :- isMinus(X, Y, Z).
isMinus(pred(X), succ(Y), pred(pred(Z))) :- isMinus(X, Y, Z).
isMinus(pred(X), pred(Y), Z) :- isMinus(X, Y, Z).
isTimes(X, zero, zero).
isTimes(zero, succ(Y), zero).
isTimes(zero, pred(Y), zero).
isTimes(succ(X), succ(Y), Z) :- ','(isTimes(succ(X), Y, A), isPlus(A, succ(X), Z)).
isTimes(succ(X), pred(Y), Z) :- ','(isTimes(succ(X), Y, A), isMinus(A, succ(X), Z)).
isTimes(pred(X), succ(Y), Z) :- ','(isTimes(pred(X), Y, A), isPlus(A, pred(X), Z)).
isTimes(pred(X), pred(Y), Z) :- ','(isTimes(pred(X), Y, A), isMinus(A, pred(X), Z)).
isDiv(zero, succ(Y), zero).
isDiv(zero, pred(Y), zero).
isDiv(succ(X), succ(Y), zero) :- isMinus(succ(X), succ(Y), pred(Z)).
isDiv(succ(X), succ(Y), succ(Z)) :- ','(isMinus(succ(X), succ(Y), A), isDiv(A, succ(Y), Z)).
isDiv(succ(X), pred(Y), Z) :- ','(isMinus(zero, pred(Y), A), ','(isDiv(succ(X), A, B), isMinus(zero, B, Z))).
isDiv(pred(X), pred(Y), zero) :- isMinus(pred(X), pred(Y), succ(Z)).
isDiv(pred(X), pred(Y), succ(Z)) :- ','(isMinus(pred(X), pred(Y), A), isDiv(A, pred(Y), Z)).
isDiv(pred(X), succ(Y), Z) :- ','(isMinus(zero, pred(X), A), ','(isDiv(A, succ(Y), B), isMinus(zero, B, Z))).
isModulo(X, Y, Z) :- ','(isDiv(X, Y, A), ','(isTimes(A, Y, B), isMinus(X, B, Z))).
=(X, X).
isGreater(succ(X), zero).
isGreater(succ(X), pred(Y)).
isGreater(succ(X), succ(Y)) :- isGreater(X, Y).
isGreater(zero, pred(Y)).
isGreater(pred(X), pred(Y)) :- isGreater(X, Y).
isLess(pred(X), zero).
isLess(pred(X), succ(Y)).
isLess(pred(X), pred(Y)) :- isLess(X, Y).
isLess(zero, succ(Y)).
isLess(succ(X), succ(Y)) :- isLess(X, Y).

Queries:

bid(g,a,a,a).

Eliminated all or-constructs.

↳ Prolog
  ↳ PredefinedPredicateTransformerProof
    ↳ Prolog
      ↳ OrTransformerProof
        ↳ Prolog
          ↳ UndefinedPredicateHandlerProof

Clauses:

bid(Hand, Attributes, Points, Bid) :- ','(sort_hand(Hand, SortedHand), ','(evaluate(SortedHand, Attributes, Points), make_bid(SortedHand, Attributes, Points, Bid))).
evaluate(Hand, [], P) :- ','(hcp(Hand, zero, HCP), ','(adjustments(Hand, MP), ','(isPlus(HCP, MP, U), =(P, U)))).
adjustments(_, zero).
make_bid(Hand, Attributes, Points, 'punt...').
hcp([], N, N).
hcp(.(=(_X, C), Sn), Ni, No) :- ','(hcp_suit(C, N), ','(','(isPlus(N, Ni, U), =(Nt, U)), hcp(Sn, Nt, No))).
hcp_suit(S, P) :- ','(honors(S, zero, HP), ','(dist(S, DP), ','(misc(S, MP), ','(isPlus(DP, MP, U), ','(isPlus(HP, U, U1), =(P, U1)))))).
honors([], Pi, Pi).
honors(.(C1, Cn), Pi, Po) :- ','(honor(C1, P), ','(','(=(X, P), ','(=(X1, zero), isGreater(X, X1))), ','(','(isPlus(P, Pi, U), =(Pt, U)), honors(Cn, Pt, Po)))).
honors(.(C1, Cn), Pi, Pi) :- honor(C1, zero).
honor(C, N) :- face_card(C, N).
honor(C, zero) :- integer(C).
face_card(ace, succ(succ(succ(succ(zero))))).
face_card(king, succ(succ(succ(zero)))).
face_card(queen, succ(succ(zero))).
face_card(jack, succ(zero)).
dist([], succ(succ(succ(zero)))).
dist(.(_, []), succ(succ(zero))).
dist(.(_, .(_, [])), succ(zero)).
dist(.(_, .(_, .(_, _))), zero).
misc(.(ace, []), pred(zero)).
misc(.(king, []), pred(pred(zero))).
misc(.(queen, .(_, [])), pred(pred(zero))).
misc(.(jack, .(_, [])), pred(zero)).
misc(.(_X, .(_Y, .(H3, Rem))), P) :- ','(honor(H3, X), ','(','(=(X1, X), ','(=(X2, zero), isGreater(X1, X2))), ','(length(Rem, N), ','(','(=(X3, N), ','(=(X4, succ(succ(zero))), isGreater(X3, X4))), ','(isMinus(N, succ(succ(zero)), U), =(P, U)))))).
misc(_, zero).
sort_hand(Hand, SortedHand) :- ','(split_suits(Hand, SplitHand), sort_suits(SplitHand, SortedHand)).
split_suits(Hand, .(=(spades, S), .(=(hearts, H), .(=(diamonds, D), .(=(clubs, C), []))))) :- ','(filter(Hand, spades, S), ','(filter(Hand, hearts, H), ','(filter(Hand, diamonds, D), filter(Hand, clubs, C)))).
filter([], _, []).
filter(.(-(Card, Suit), In), Suit, .(Card, Out)) :- filter(In, Suit, Out).
filter(.(-(_A, X), In), Suit, Out) :- ','(\==(Suit, X), filter(In, Suit, Out)).
sort_suits([], []).
sort_suits(.(=(S, Ci), In), .(=(S, Co), Out)) :- ','(i_sort(Ci, [], Co), sort_suits(In, Out)).
i_sort([], L, L).
i_sort(.(C1, Cn), Li, Lo) :- ','(insert(C1, Li, Lt), i_sort(Cn, Lt, Lo)).
insert(X, [], .(X, [])).
insert(X, .(Y, Z), .(X, .(Y, Z))) :- higher(X, Y).
insert(X, .(Y, Z), .(Y, L)) :- ','(lower(X, Y), insert(X, Z, L)).
higher(ace, _).
higher(king, X) :- \==(X, ace).
higher(queen, X) :- ','(\==(X, ace), \==(X, king)).
higher(jack, X) :- integer(X).
higher(jack, jack).
lower(king, ace).
lower(queen, X) :- ','(honor(X, N), ','(=(X1, N), ','(=(X2, succ(succ(zero))), isGreater(X1, X2)))).
lower(jack, X) :- ','(honor(X, N), ','(=(X1, N), ','(=(X2, succ(zero)), isGreater(X1, X2)))).
lower(X, Y) :- ','(integer(X), honor(Y, _M)).
lower(X, Y) :- ','(integer(X), ','(integer(Y), ','(=(X1, X), ','(=(X2, Y), isLess(X1, X2))))).
goal :- bid(.(-(ace, clubs), .(-(succ(succ(succ(zero))), hearts), .(-(succ(succ(succ(succ(zero)))), spades), .(-(succ(succ(succ(succ(zero)))), diamonds), .(-(king, clubs), .(-(jack, hearts), .(-(ace, spades), .(-(ace, hearts), .(-(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))))), clubs), .(-(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), clubs), .(-(succ(succ(succ(succ(succ(succ(zero)))))), clubs), .(-(queen, diamonds), .(-(king, spades), []))))))))))))), Attr, Pts, Bid).
isPlus(zero, X, X).
isPlus(succ(X), zero, succ(X)).
isPlus(succ(X), succ(Y), succ(succ(Z))) :- isPlus(X, Y, Z).
isPlus(succ(X), pred(Y), Z) :- isPlus(X, Y, Z).
isPlus(pred(X), zero, pred(X)).
isPlus(pred(X), succ(Y), Z) :- isPlus(X, Y, Z).
isPlus(pred(X), pred(Y), pred(pred(Z))) :- isPlus(X, Y, Z).
isMinus(X, zero, X).
isMinus(zero, succ(Y), pred(Z)) :- isMinus(zero, Y, Z).
isMinus(zero, pred(Y), succ(Z)) :- isMinus(zero, Y, Z).
isMinus(succ(X), succ(Y), Z) :- isMinus(X, Y, Z).
isMinus(succ(X), pred(Y), succ(succ(Z))) :- isMinus(X, Y, Z).
isMinus(pred(X), succ(Y), pred(pred(Z))) :- isMinus(X, Y, Z).
isMinus(pred(X), pred(Y), Z) :- isMinus(X, Y, Z).
isTimes(X, zero, zero).
isTimes(zero, succ(Y), zero).
isTimes(zero, pred(Y), zero).
isTimes(succ(X), succ(Y), Z) :- ','(isTimes(succ(X), Y, A), isPlus(A, succ(X), Z)).
isTimes(succ(X), pred(Y), Z) :- ','(isTimes(succ(X), Y, A), isMinus(A, succ(X), Z)).
isTimes(pred(X), succ(Y), Z) :- ','(isTimes(pred(X), Y, A), isPlus(A, pred(X), Z)).
isTimes(pred(X), pred(Y), Z) :- ','(isTimes(pred(X), Y, A), isMinus(A, pred(X), Z)).
isDiv(zero, succ(Y), zero).
isDiv(zero, pred(Y), zero).
isDiv(succ(X), succ(Y), zero) :- isMinus(succ(X), succ(Y), pred(Z)).
isDiv(succ(X), succ(Y), succ(Z)) :- ','(isMinus(succ(X), succ(Y), A), isDiv(A, succ(Y), Z)).
isDiv(succ(X), pred(Y), Z) :- ','(isMinus(zero, pred(Y), A), ','(isDiv(succ(X), A, B), isMinus(zero, B, Z))).
isDiv(pred(X), pred(Y), zero) :- isMinus(pred(X), pred(Y), succ(Z)).
isDiv(pred(X), pred(Y), succ(Z)) :- ','(isMinus(pred(X), pred(Y), A), isDiv(A, pred(Y), Z)).
isDiv(pred(X), succ(Y), Z) :- ','(isMinus(zero, pred(X), A), ','(isDiv(A, succ(Y), B), isMinus(zero, B, Z))).
isModulo(X, Y, Z) :- ','(isDiv(X, Y, A), ','(isTimes(A, Y, B), isMinus(X, B, Z))).
=(X, X).
isGreater(succ(X), zero).
isGreater(succ(X), pred(Y)).
isGreater(succ(X), succ(Y)) :- isGreater(X, Y).
isGreater(zero, pred(Y)).
isGreater(pred(X), pred(Y)) :- isGreater(X, Y).
isLess(pred(X), zero).
isLess(pred(X), succ(Y)).
isLess(pred(X), pred(Y)) :- isLess(X, Y).
isLess(zero, succ(Y)).
isLess(succ(X), succ(Y)) :- isLess(X, Y).
higher(X, Y) :- ','(integer(X), ','(integer(Y), ','(=(X1, X), ','(=(X2, Y), =(X1, X2))))).
higher(X, Y) :- ','(integer(X), ','(integer(Y), ','(=(X1, X), ','(=(X2, Y), isGreater(X1, X2))))).

Queries:

bid(g,a,a,a).

Added facts for all undefined predicates.

↳ Prolog
  ↳ PredefinedPredicateTransformerProof
    ↳ Prolog
      ↳ OrTransformerProof
        ↳ Prolog
          ↳ UndefinedPredicateHandlerProof
            ↳ Prolog

Clauses:

bid(Hand, Attributes, Points, Bid) :- ','(sort_hand(Hand, SortedHand), ','(evaluate(SortedHand, Attributes, Points), make_bid(SortedHand, Attributes, Points, Bid))).
evaluate(Hand, [], P) :- ','(hcp(Hand, zero, HCP), ','(adjustments(Hand, MP), ','(isPlus(HCP, MP, U), =(P, U)))).
adjustments(_, zero).
make_bid(Hand, Attributes, Points, 'punt...').
hcp([], N, N).
hcp(.(=(_X, C), Sn), Ni, No) :- ','(hcp_suit(C, N), ','(isPlus(N, Ni, U), ','(=(Nt, U), hcp(Sn, Nt, No)))).
hcp_suit(S, P) :- ','(honors(S, zero, HP), ','(dist(S, DP), ','(misc(S, MP), ','(isPlus(DP, MP, U), ','(isPlus(HP, U, U1), =(P, U1)))))).
honors([], Pi, Pi).
honors(.(C1, Cn), Pi, Po) :- ','(honor(C1, P), ','(=(X, P), ','(=(X1, zero), ','(isGreater(X, X1), ','(isPlus(P, Pi, U), ','(=(Pt, U), honors(Cn, Pt, Po))))))).
honors(.(C1, Cn), Pi, Pi) :- honor(C1, zero).
honor(C, N) :- face_card(C, N).
honor(C, zero) :- integer(C).
face_card(ace, succ(succ(succ(succ(zero))))).
face_card(king, succ(succ(succ(zero)))).
face_card(queen, succ(succ(zero))).
face_card(jack, succ(zero)).
dist([], succ(succ(succ(zero)))).
dist(.(_, []), succ(succ(zero))).
dist(.(_, .(_, [])), succ(zero)).
dist(.(_, .(_, .(_, _))), zero).
misc(.(ace, []), pred(zero)).
misc(.(king, []), pred(pred(zero))).
misc(.(queen, .(_, [])), pred(pred(zero))).
misc(.(jack, .(_, [])), pred(zero)).
misc(.(_X, .(_Y, .(H3, Rem))), P) :- ','(honor(H3, X), ','(=(X1, X), ','(=(X2, zero), ','(isGreater(X1, X2), ','(length(Rem, N), ','(=(X3, N), ','(=(X4, succ(succ(zero))), ','(isGreater(X3, X4), ','(isMinus(N, succ(succ(zero)), U), =(P, U)))))))))).
misc(_, zero).
sort_hand(Hand, SortedHand) :- ','(split_suits(Hand, SplitHand), sort_suits(SplitHand, SortedHand)).
split_suits(Hand, .(=(spades, S), .(=(hearts, H), .(=(diamonds, D), .(=(clubs, C), []))))) :- ','(filter(Hand, spades, S), ','(filter(Hand, hearts, H), ','(filter(Hand, diamonds, D), filter(Hand, clubs, C)))).
filter([], _, []).
filter(.(-(Card, Suit), In), Suit, .(Card, Out)) :- filter(In, Suit, Out).
filter(.(-(_A, X), In), Suit, Out) :- ','(\==(Suit, X), filter(In, Suit, Out)).
sort_suits([], []).
sort_suits(.(=(S, Ci), In), .(=(S, Co), Out)) :- ','(i_sort(Ci, [], Co), sort_suits(In, Out)).
i_sort([], L, L).
i_sort(.(C1, Cn), Li, Lo) :- ','(insert(C1, Li, Lt), i_sort(Cn, Lt, Lo)).
insert(X, [], .(X, [])).
insert(X, .(Y, Z), .(X, .(Y, Z))) :- higher(X, Y).
insert(X, .(Y, Z), .(Y, L)) :- ','(lower(X, Y), insert(X, Z, L)).
higher(ace, _).
higher(king, X) :- \==(X, ace).
higher(queen, X) :- ','(\==(X, ace), \==(X, king)).
higher(jack, X) :- integer(X).
higher(jack, jack).
lower(king, ace).
lower(queen, X) :- ','(honor(X, N), ','(=(X1, N), ','(=(X2, succ(succ(zero))), isGreater(X1, X2)))).
lower(jack, X) :- ','(honor(X, N), ','(=(X1, N), ','(=(X2, succ(zero)), isGreater(X1, X2)))).
lower(X, Y) :- ','(integer(X), honor(Y, _M)).
lower(X, Y) :- ','(integer(X), ','(integer(Y), ','(=(X1, X), ','(=(X2, Y), isLess(X1, X2))))).
goal :- bid(.(-(ace, clubs), .(-(succ(succ(succ(zero))), hearts), .(-(succ(succ(succ(succ(zero)))), spades), .(-(succ(succ(succ(succ(zero)))), diamonds), .(-(king, clubs), .(-(jack, hearts), .(-(ace, spades), .(-(ace, hearts), .(-(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero)))))))))), clubs), .(-(succ(succ(succ(succ(succ(succ(succ(succ(succ(zero))))))))), clubs), .(-(succ(succ(succ(succ(succ(succ(zero)))))), clubs), .(-(queen, diamonds), .(-(king, spades), []))))))))))))), Attr, Pts, Bid).
isPlus(zero, X, X).
isPlus(succ(X), zero, succ(X)).
isPlus(succ(X), succ(Y), succ(succ(Z))) :- isPlus(X, Y, Z).
isPlus(succ(X), pred(Y), Z) :- isPlus(X, Y, Z).
isPlus(pred(X), zero, pred(X)).
isPlus(pred(X), succ(Y), Z) :- isPlus(X, Y, Z).
isPlus(pred(X), pred(Y), pred(pred(Z))) :- isPlus(X, Y, Z).
isMinus(X, zero, X).
isMinus(zero, succ(Y), pred(Z)) :- isMinus(zero, Y, Z).
isMinus(zero, pred(Y), succ(Z)) :- isMinus(zero, Y, Z).
isMinus(succ(X), succ(Y), Z) :- isMinus(X, Y, Z).
isMinus(succ(X), pred(Y), succ(succ(Z))) :- isMinus(X, Y, Z).
isMinus(pred(X), succ(Y), pred(pred(Z))) :- isMinus(X, Y, Z).
isMinus(pred(X), pred(Y), Z) :- isMinus(X, Y, Z).
isTimes(X, zero, zero).
isTimes(zero, succ(Y), zero).
isTimes(zero, pred(Y), zero).
isTimes(succ(X), succ(Y), Z) :- ','(isTimes(succ(X), Y, A), isPlus(A, succ(X), Z)).
isTimes(succ(X), pred(Y), Z) :- ','(isTimes(succ(X), Y, A), isMinus(A, succ(X), Z)).
isTimes(pred(X), succ(Y), Z) :- ','(isTimes(pred(X), Y, A), isPlus(A, pred(X), Z)).
isTimes(pred(X), pred(Y), Z) :- ','(isTimes(pred(X), Y, A), isMinus(A, pred(X), Z)).
isDiv(zero, succ(Y), zero).
isDiv(zero, pred(Y), zero).
isDiv(succ(X), succ(Y), zero) :- isMinus(succ(X), succ(Y), pred(Z)).
isDiv(succ(X), succ(Y), succ(Z)) :- ','(isMinus(succ(X), succ(Y), A), isDiv(A, succ(Y), Z)).
isDiv(succ(X), pred(Y), Z) :- ','(isMinus(zero, pred(Y), A), ','(isDiv(succ(X), A, B), isMinus(zero, B, Z))).
isDiv(pred(X), pred(Y), zero) :- isMinus(pred(X), pred(Y), succ(Z)).
isDiv(pred(X), pred(Y), succ(Z)) :- ','(isMinus(pred(X), pred(Y), A), isDiv(A, pred(Y), Z)).
isDiv(pred(X), succ(Y), Z) :- ','(isMinus(zero, pred(X), A), ','(isDiv(A, succ(Y), B), isMinus(zero, B, Z))).
isModulo(X, Y, Z) :- ','(isDiv(X, Y, A), ','(isTimes(A, Y, B), isMinus(X, B, Z))).
=(X, X).
isGreater(succ(X), zero).
isGreater(succ(X), pred(Y)).
isGreater(succ(X), succ(Y)) :- isGreater(X, Y).
isGreater(zero, pred(Y)).
isGreater(pred(X), pred(Y)) :- isGreater(X, Y).
isLess(pred(X), zero).
isLess(pred(X), succ(Y)).
isLess(pred(X), pred(Y)) :- isLess(X, Y).
isLess(zero, succ(Y)).
isLess(succ(X), succ(Y)) :- isLess(X, Y).
higher(X, Y) :- ','(integer(X), ','(integer(Y), ','(=(X1, X), ','(=(X2, Y), =(X1, X2))))).
higher(X, Y) :- ','(integer(X), ','(integer(Y), ','(=(X1, X), ','(=(X2, Y), isGreater(X1, X2))))).
integer(X0).
length(X0, X1).
\==(X0, X1).

Queries:

bid(g,a,a,a).