Next: NET Benchmark
Up: Benchmark Sources
Previous: nrev Benchmark
This benchmark was called with the procedure go4.
Only the time for finding the first solution was measured.
literal(z0).
literal(z1).
literal(z2).
literal(z3).
literal(z4).
literal(z5).
literal(z6).
literal(z7).
literal(z8).
literal(z9).
literal(n[X]) :- literal(X).
norm(X, X) :- literal(X).
norm(o[X, Y], o[X, Y]) :-
literal(X),
literal(Y).
norm(a[X, Y], a[X, Y]) :-
literal(X),
literal(Y).
norm(o[X, Y], o[X1, Y]) :-
literal(Y),
norm(X, X1).
norm(o[X, o[Y, Z]], W) :-
norm(o[o[X, Y], Z], W).
norm(o[X, a[Y1, Y2]], o[X1, Y12]) :-
norm(X, X1),
norm(a[Y1, Y2], Y12).
norm(a[X, Y], a[X1, Y]) :-
literal(Y),
norm(X, X1).
norm(a[X, a[Y, Z]], W) :-
norm(a[a[X, Y], Z], W).
norm(a[X, o[Y1, Y2]], a[X1, Y12]) :-
norm(X, X1),
norm(o[Y1, Y2], Y12).
dnf(X, X) :- literal(X).
dnf(o[X, Y], o[X, Y]) :-
literal(X),
literal(Y).
dnf(a[X, Y], a[X, Y]) :-
literal(X),
literal(Y).
dnf(n[n[X]], W) :- dnf(X, W).
dnf(n[o[X, Y]], W) :- dnf(a[n[X], n[Y]], W).
dnf(n[a[X, Y]], W) :- dnf(o[n[X], n[Y]], W).
dnf(o[X, Y], W) :- dnf(X, X1),
dnf(Y, Y1),
norm(o[X1, Y1], W).
dnf(a[X, Y], a[a[X1, X2], Y]) :-
literal(Y),
dnf(X, a[X1, X2]).
dnf(a[X, Y], a[a[Y1, Y2], X]) :-
literal(X),
dnf(Y, a[Y1, Y2]).
dnf(a[X, Y], W) :-
dnf(X, a[X1, X2]),
dnf(Y, a[Y1, Y2]),
norm(a[a[X1, X2], a[Y1, Y2]], W).
dnf(a[X, Y], W) :-
dnf(X, o[X1, X2]),
dnf(Y, Y1),
dnf(o[a[X1, Y1], a[X2, Y1]], W).
dnf(a[X, Y], W) :-
dnf(X, X1),
dnf(Y, o[Y1, Y2]),
dnf(o[a[X1, Y1], a[X1, Y2]], W).
go1(X) :- dnf(a[z1,
a[z2,
o[z3,
a[z4,
a[z5, z6]]]]],
X).
go2(X) :- dnf(o[o[a[z1, z2], z3],
o[a[z4,
a[a[z5, z6],
z7]],
o[z8, z9]]],
X).
go3(X) :- dnf(a[a[z1, a[o[z2, z3], z4]],
a[z5, o[z6, z7]]],
X).
go4(X) :- dnf(n[o[a[n[o[z1, z2]],
n[a[z3, z4]]],
a[n[z5],
o[a[z6, a[z7, z8]],
z9]]]],
X),
dnf(n[o[a[n[o[z1, z2]],
n[a[z3, z4]]],
a[n[z5],
o[a[z6, a[z7, z8]],
z9]]]],
X).