prover9-doc 0.0.200902a-2 / usr / share / doc / prover9-doc / examples / non-MOL-OML.interps

% These are all of the nonmodular OMLs up through size 16.

interpretation(10, [], [
    function(c(_), [1,0,5,6,7,2,3,4,9,8]),
    function(v(_,_), [0,1,2,3,4,5,6,7,8,9,1,1,1,1,1,1,1,1,1,1,2,1,2,1,1,1,1,2,1,2,3,1,1,3,1,1,1,1,1,1,4,1,1,1,4,4,1,1,1,4,5,1,1,1,4,5,1,8,8,4,6,1,1,1,1,1,6,1,1,1,7,1,2,1,1,8,1,7,8,2,8,1,1,1,1,8,1,8,8,1,9,1,2,1,4,4,1,2,1,9]),
    function(^(_,_), [0,0,0,0,0,0,0,0,0,0,0,1,2,3,4,5,6,7,8,9,0,2,2,0,9,0,0,7,7,9,0,3,0,3,0,0,0,0,0,0,0,4,9,0,4,5,0,0,5,9,0,5,0,0,5,5,0,0,5,0,0,6,0,0,0,0,6,0,0,0,0,7,7,0,0,0,0,7,7,0,0,8,7,0,5,5,0,7,8,0,0,9,9,0,9,0,0,0,0,9]),
    function(f(_,_), [1,1,1,1,1,1,1,1,1,1,1,0,5,6,7,2,3,4,9,8,1,5,5,1,8,1,1,4,4,8,1,6,1,6,1,1,1,1,1,1,1,7,8,1,7,2,1,1,2,8,1,2,1,1,2,2,1,1,2,1,1,3,1,1,1,1,3,1,1,1,1,4,4,1,1,1,1,4,4,1,1,9,4,1,2,2,1,4,9,1,1,8,8,1,8,1,1,1,1,8])]).
% isofilter: input=2, kept=1, checks=1, perms=5, 0.02 seconds.
interpretation(12, [], [
    function(c(_), [1,0,5,6,7,2,3,4,9,8,11,10]),
    function(v(_,_), [0,1,2,3,4,5,6,7,8,9,10,11,1,1,1,1,1,1,1,1,1,1,1,1,2,1,2,1,1,1,1,2,1,2,1,1,3,1,1,3,1,1,1,1,1,1,1,1,4,1,1,1,4,4,1,1,1,4,1,1,5,1,1,1,4,5,1,8,8,4,1,1,6,1,1,1,1,1,6,1,1,1,1,1,7,1,2,1,1,8,1,7,8,2,1,1,8,1,1,1,1,8,1,8,8,1,1,1,9,1,2,1,4,4,1,2,1,9,1,1,10,1,1,1,1,1,1,1,1,1,10,1,11,1,1,1,1,1,1,1,1,1,1,11]),
    function(^(_,_), [0,0,0,0,0,0,0,0,0,0,0,0,0,1,2,3,4,5,6,7,8,9,10,11,0,2,2,0,9,0,0,7,7,9,0,0,0,3,0,3,0,0,0,0,0,0,0,0,0,4,9,0,4,5,0,0,5,9,0,0,0,5,0,0,5,5,0,0,5,0,0,0,0,6,0,0,0,0,6,0,0,0,0,0,0,7,7,0,0,0,0,7,7,0,0,0,0,8,7,0,5,5,0,7,8,0,0,0,0,9,9,0,9,0,0,0,0,9,0,0,0,10,0,0,0,0,0,0,0,0,10,0,0,11,0,0,0,0,0,0,0,0,0,11]),
    function(f(_,_), [1,1,1,1,1,1,1,1,1,1,1,1,1,0,5,6,7,2,3,4,9,8,11,10,1,5,5,1,8,1,1,4,4,8,1,1,1,6,1,6,1,1,1,1,1,1,1,1,1,7,8,1,7,2,1,1,2,8,1,1,1,2,1,1,2,2,1,1,2,1,1,1,1,3,1,1,1,1,3,1,1,1,1,1,1,4,4,1,1,1,1,4,4,1,1,1,1,9,4,1,2,2,1,4,9,1,1,1,1,8,8,1,8,1,1,1,1,8,1,1,1,11,1,1,1,1,1,1,1,1,11,1,1,10,1,1,1,1,1,1,1,1,1,10])]).
% isofilter: input=2, kept=1, checks=1, perms=49, 0.03 seconds.
interpretation(14, [], [
    function(c(_), [1,0,5,6,7,2,3,4,9,8,11,10,13,12]),
    function(v(_,_), [0,1,2,3,4,5,6,7,8,9,10,11,12,13,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,2,1,1,1,1,1,1,2,1,2,1,1,3,1,1,3,1,1,1,1,1,1,1,1,1,1,4,1,1,1,4,1,1,1,1,4,1,1,1,4,5,1,1,1,1,5,1,8,8,10,10,8,1,8,6,1,1,1,1,1,6,1,1,1,1,1,1,1,7,1,1,1,1,8,1,7,8,12,1,8,12,8,8,1,1,1,1,8,1,8,8,1,1,8,1,8,9,1,2,1,4,10,1,12,1,9,10,2,12,4,10,1,1,1,1,10,1,1,1,10,10,1,1,1,11,1,2,1,1,8,1,8,8,2,1,11,1,8,12,1,1,1,1,1,1,12,1,12,1,1,12,1,13,1,1,1,4,8,1,8,8,4,1,8,1,13]),
    function(^(_,_), [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,2,3,4,5,6,7,8,9,10,11,12,13,0,2,2,0,9,0,0,0,11,9,9,11,9,0,0,3,0,3,0,0,0,0,0,0,0,0,0,0,0,4,9,0,4,0,0,0,13,9,9,0,9,13,0,5,0,0,0,5,0,0,5,0,5,0,0,0,0,6,0,0,0,0,6,0,0,0,0,0,0,0,0,7,0,0,0,0,0,7,7,0,0,0,7,0,0,8,11,0,13,5,0,7,8,0,5,11,7,13,0,9,9,0,9,0,0,0,0,9,9,0,9,0,0,10,9,0,9,5,0,0,5,9,10,0,9,0,0,11,11,0,0,0,0,0,11,0,0,11,0,0,0,12,9,0,9,0,0,7,7,9,9,0,12,0,0,13,0,0,13,0,0,0,13,0,0,0,0,13]),
    function(f(_,_), [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,5,6,7,2,3,4,9,8,11,10,13,12,1,5,5,1,8,1,1,1,10,8,8,10,8,1,1,6,1,6,1,1,1,1,1,1,1,1,1,1,1,7,8,1,7,1,1,1,12,8,8,1,8,12,1,2,1,1,1,2,1,1,2,1,2,1,1,1,1,3,1,1,1,1,3,1,1,1,1,1,1,1,1,4,1,1,1,1,1,4,4,1,1,1,4,1,1,9,10,1,12,2,1,4,9,1,2,10,4,12,1,8,8,1,8,1,1,1,1,8,8,1,8,1,1,11,8,1,8,2,1,1,2,8,11,1,8,1,1,10,10,1,1,1,1,1,10,1,1,10,1,1,1,13,8,1,8,1,1,4,4,8,8,1,13,1,1,12,1,1,12,1,1,1,12,1,1,1,1,12])]).
interpretation(14, [], [
    function(c(_), [1,0,5,6,7,2,3,4,9,8,11,10,13,12]),
    function(v(_,_), [0,1,2,3,4,5,6,7,8,9,10,11,12,13,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,2,1,1,1,1,2,1,2,1,1,1,1,3,1,1,3,1,1,1,1,1,1,1,1,1,1,4,1,1,1,4,4,1,1,1,4,1,1,1,1,5,1,1,1,4,5,1,8,8,4,1,1,1,1,6,1,1,1,1,1,6,1,1,1,1,1,1,1,7,1,2,1,1,8,1,7,8,2,1,1,1,1,8,1,1,1,1,8,1,8,8,1,1,1,1,1,9,1,2,1,4,4,1,2,1,9,1,1,1,1,10,1,1,1,1,1,1,1,1,1,10,1,1,1,11,1,1,1,1,1,1,1,1,1,1,11,1,1,12,1,1,1,1,1,1,1,1,1,1,1,12,1,13,1,1,1,1,1,1,1,1,1,1,1,1,13]),
    function(^(_,_), [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,2,3,4,5,6,7,8,9,10,11,12,13,0,2,2,0,9,0,0,7,7,9,0,0,0,0,0,3,0,3,0,0,0,0,0,0,0,0,0,0,0,4,9,0,4,5,0,0,5,9,0,0,0,0,0,5,0,0,5,5,0,0,5,0,0,0,0,0,0,6,0,0,0,0,6,0,0,0,0,0,0,0,0,7,7,0,0,0,0,7,7,0,0,0,0,0,0,8,7,0,5,5,0,7,8,0,0,0,0,0,0,9,9,0,9,0,0,0,0,9,0,0,0,0,0,10,0,0,0,0,0,0,0,0,10,0,0,0,0,11,0,0,0,0,0,0,0,0,0,11,0,0,0,12,0,0,0,0,0,0,0,0,0,0,12,0,0,13,0,0,0,0,0,0,0,0,0,0,0,13]),
    function(f(_,_), [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,5,6,7,2,3,4,9,8,11,10,13,12,1,5,5,1,8,1,1,4,4,8,1,1,1,1,1,6,1,6,1,1,1,1,1,1,1,1,1,1,1,7,8,1,7,2,1,1,2,8,1,1,1,1,1,2,1,1,2,2,1,1,2,1,1,1,1,1,1,3,1,1,1,1,3,1,1,1,1,1,1,1,1,4,4,1,1,1,1,4,4,1,1,1,1,1,1,9,4,1,2,2,1,4,9,1,1,1,1,1,1,8,8,1,8,1,1,1,1,8,1,1,1,1,1,11,1,1,1,1,1,1,1,1,11,1,1,1,1,10,1,1,1,1,1,1,1,1,1,10,1,1,1,13,1,1,1,1,1,1,1,1,1,1,13,1,1,12,1,1,1,1,1,1,1,1,1,1,1,12])]).
interpretation(14, [], [
    function(c(_), [1,0,5,6,7,2,3,4,9,8,11,10,13,12]),
    function(v(_,_), [0,1,2,3,4,5,6,7,8,9,10,11,12,13,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,2,1,1,1,1,2,1,2,1,1,1,1,3,1,1,3,1,1,1,1,1,1,1,3,1,3,4,1,1,1,4,4,1,1,1,4,1,1,1,1,5,1,1,1,4,5,1,8,8,4,1,1,1,1,6,1,1,1,1,1,6,1,1,1,10,12,12,10,7,1,2,1,1,8,1,7,8,2,1,1,1,1,8,1,1,1,1,8,1,8,8,1,1,1,1,1,9,1,2,1,4,4,1,2,1,9,1,1,1,1,10,1,1,1,1,1,10,1,1,1,10,1,1,10,11,1,1,3,1,1,12,1,1,1,1,11,12,3,12,1,1,1,1,1,12,1,1,1,1,12,12,1,13,1,1,3,1,1,10,1,1,1,10,3,1,13]),
    function(^(_,_), [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,2,3,4,5,6,7,8,9,10,11,12,13,0,2,2,0,9,0,0,7,7,9,0,0,0,0,0,3,0,3,0,0,0,0,0,0,13,11,11,13,0,4,9,0,4,5,0,0,5,9,0,0,0,0,0,5,0,0,5,5,0,0,5,0,0,0,0,0,0,6,0,0,0,0,6,0,0,0,6,0,6,0,0,7,7,0,0,0,0,7,7,0,0,0,0,0,0,8,7,0,5,5,0,7,8,0,0,0,0,0,0,9,9,0,9,0,0,0,0,9,0,0,0,0,0,10,0,13,0,0,6,0,0,0,10,0,6,13,0,11,0,11,0,0,0,0,0,0,0,11,11,0,0,12,0,11,0,0,6,0,0,0,6,11,12,0,0,13,0,13,0,0,0,0,0,0,13,0,0,13]),
    function(f(_,_), [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,5,6,7,2,3,4,9,8,11,10,13,12,1,5,5,1,8,1,1,4,4,8,1,1,1,1,1,6,1,6,1,1,1,1,1,1,12,10,10,12,1,7,8,1,7,2,1,1,2,8,1,1,1,1,1,2,1,1,2,2,1,1,2,1,1,1,1,1,1,3,1,1,1,1,3,1,1,1,3,1,3,1,1,4,4,1,1,1,1,4,4,1,1,1,1,1,1,9,4,1,2,2,1,4,9,1,1,1,1,1,1,8,8,1,8,1,1,1,1,8,1,1,1,1,1,11,1,12,1,1,3,1,1,1,11,1,3,12,1,10,1,10,1,1,1,1,1,1,1,10,10,1,1,13,1,10,1,1,3,1,1,1,3,10,13,1,1,12,1,12,1,1,1,1,1,1,12,1,1,12])]).
% isofilter: input=23, kept=3, checks=20, perms=38324, 0.52 seconds.
interpretation(16, [], [
    function(c(_), [1,0,5,6,7,2,3,4,9,8,11,10,13,12,15,14]),
    function(v(_,_), [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,2,1,1,1,1,1,1,2,1,2,1,1,1,1,3,1,1,3,1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,4,1,1,1,1,4,1,1,1,4,1,1,5,1,1,1,1,5,1,8,8,10,10,8,1,8,1,1,6,1,1,1,1,1,6,1,1,1,1,1,1,1,1,1,7,1,1,1,1,8,1,7,8,12,1,8,12,8,1,1,8,1,1,1,1,8,1,8,8,1,1,8,1,8,1,1,9,1,2,1,4,10,1,12,1,9,10,2,12,4,1,1,10,1,1,1,1,10,1,1,1,10,10,1,1,1,1,1,11,1,2,1,1,8,1,8,8,2,1,11,1,8,1,1,12,1,1,1,1,1,1,12,1,12,1,1,12,1,1,1,13,1,1,1,4,8,1,8,8,4,1,8,1,13,1,1,14,1,1,1,1,1,1,1,1,1,1,1,1,1,14,1,15,1,1,1,1,1,1,1,1,1,1,1,1,1,1,15]),
    function(^(_,_), [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,0,2,2,0,9,0,0,0,11,9,9,11,9,0,0,0,0,3,0,3,0,0,0,0,0,0,0,0,0,0,0,0,0,4,9,0,4,0,0,0,13,9,9,0,9,13,0,0,0,5,0,0,0,5,0,0,5,0,5,0,0,0,0,0,0,6,0,0,0,0,6,0,0,0,0,0,0,0,0,0,0,7,0,0,0,0,0,7,7,0,0,0,7,0,0,0,0,8,11,0,13,5,0,7,8,0,5,11,7,13,0,0,0,9,9,0,9,0,0,0,0,9,9,0,9,0,0,0,0,10,9,0,9,5,0,0,5,9,10,0,9,0,0,0,0,11,11,0,0,0,0,0,11,0,0,11,0,0,0,0,0,12,9,0,9,0,0,7,7,9,9,0,12,0,0,0,0,13,0,0,13,0,0,0,13,0,0,0,0,13,0,0,0,14,0,0,0,0,0,0,0,0,0,0,0,0,14,0,0,15,0,0,0,0,0,0,0,0,0,0,0,0,0,15]),
    function(f(_,_), [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,5,6,7,2,3,4,9,8,11,10,13,12,15,14,1,5,5,1,8,1,1,1,10,8,8,10,8,1,1,1,1,6,1,6,1,1,1,1,1,1,1,1,1,1,1,1,1,7,8,1,7,1,1,1,12,8,8,1,8,12,1,1,1,2,1,1,1,2,1,1,2,1,2,1,1,1,1,1,1,3,1,1,1,1,3,1,1,1,1,1,1,1,1,1,1,4,1,1,1,1,1,4,4,1,1,1,4,1,1,1,1,9,10,1,12,2,1,4,9,1,2,10,4,12,1,1,1,8,8,1,8,1,1,1,1,8,8,1,8,1,1,1,1,11,8,1,8,2,1,1,2,8,11,1,8,1,1,1,1,10,10,1,1,1,1,1,10,1,1,10,1,1,1,1,1,13,8,1,8,1,1,4,4,8,8,1,13,1,1,1,1,12,1,1,12,1,1,1,12,1,1,1,1,12,1,1,1,15,1,1,1,1,1,1,1,1,1,1,1,1,15,1,1,14,1,1,1,1,1,1,1,1,1,1,1,1,1,14])]).
interpretation(16, [], [
    function(c(_), [1,0,5,6,7,2,3,4,9,8,11,10,13,12,15,14]),
    function(v(_,_), [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,2,1,1,1,1,1,1,2,1,2,1,1,1,1,3,1,1,3,1,1,1,1,1,1,1,1,1,3,1,3,4,1,1,1,4,1,1,1,1,4,1,1,1,4,1,1,5,1,1,1,1,5,1,8,8,10,10,8,1,8,1,1,6,1,1,1,1,1,6,12,1,12,1,1,12,14,14,12,7,1,1,1,1,8,12,7,8,12,1,8,12,8,1,12,8,1,1,1,1,8,1,8,8,1,1,8,1,8,1,1,9,1,2,1,4,10,12,12,1,9,10,2,12,4,1,12,10,1,1,1,1,10,1,1,1,10,10,1,1,1,1,1,11,1,2,1,1,8,1,8,8,2,1,11,1,8,1,1,12,1,1,1,1,1,12,12,1,12,1,1,12,1,1,12,13,1,1,3,4,8,14,8,8,4,1,8,1,13,14,3,14,1,1,1,1,1,14,1,1,1,1,1,1,14,14,1,15,1,1,3,1,1,12,12,1,12,1,1,12,3,1,15]),
    function(^(_,_), [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,0,2,2,0,9,0,0,0,11,9,9,11,9,0,0,0,0,3,0,3,13,0,0,0,13,0,0,0,15,13,13,15,0,4,9,13,4,0,0,0,13,9,9,0,9,13,13,0,0,5,0,0,0,5,0,0,5,0,5,0,0,0,0,0,0,6,0,0,0,0,6,0,0,0,0,0,6,0,6,0,0,7,0,0,0,0,0,7,7,0,0,0,7,0,0,0,0,8,11,13,13,5,0,7,8,0,5,11,7,13,13,0,0,9,9,0,9,0,0,0,0,9,9,0,9,0,0,0,0,10,9,0,9,5,0,0,5,9,10,0,9,0,0,0,0,11,11,0,0,0,0,0,11,0,0,11,0,0,0,0,0,12,9,15,9,0,6,7,7,9,9,0,12,0,6,15,0,13,0,13,13,0,0,0,13,0,0,0,0,13,13,0,0,14,0,13,13,0,6,0,13,0,0,0,6,13,14,0,0,15,0,15,0,0,0,0,0,0,0,0,15,0,0,15]),
    function(f(_,_), [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,5,6,7,2,3,4,9,8,11,10,13,12,15,14,1,5,5,1,8,1,1,1,10,8,8,10,8,1,1,1,1,6,1,6,12,1,1,1,12,1,1,1,14,12,12,14,1,7,8,12,7,1,1,1,12,8,8,1,8,12,12,1,1,2,1,1,1,2,1,1,2,1,2,1,1,1,1,1,1,3,1,1,1,1,3,1,1,1,1,1,3,1,3,1,1,4,1,1,1,1,1,4,4,1,1,1,4,1,1,1,1,9,10,12,12,2,1,4,9,1,2,10,4,12,12,1,1,8,8,1,8,1,1,1,1,8,8,1,8,1,1,1,1,11,8,1,8,2,1,1,2,8,11,1,8,1,1,1,1,10,10,1,1,1,1,1,10,1,1,10,1,1,1,1,1,13,8,14,8,1,3,4,4,8,8,1,13,1,3,14,1,12,1,12,12,1,1,1,12,1,1,1,1,12,12,1,1,15,1,12,12,1,3,1,12,1,1,1,3,12,15,1,1,14,1,14,1,1,1,1,1,1,1,1,14,1,1,14])]).
interpretation(16, [], [
    function(c(_), [1,0,5,6,7,2,3,4,9,8,11,10,13,12,15,14]),
    function(v(_,_), [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,2,1,1,1,1,2,1,2,1,1,1,1,1,1,3,1,1,3,1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,4,4,1,1,1,4,1,1,1,1,1,1,5,1,1,1,4,5,1,8,8,4,1,1,1,1,1,1,6,1,1,1,1,1,6,1,1,1,1,1,1,1,1,1,7,1,2,1,1,8,1,7,8,2,1,1,1,1,1,1,8,1,1,1,1,8,1,8,8,1,1,1,1,1,1,1,9,1,2,1,4,4,1,2,1,9,1,1,1,1,1,1,10,1,1,1,1,1,1,1,1,1,10,1,1,1,1,1,11,1,1,1,1,1,1,1,1,1,1,11,1,1,1,1,12,1,1,1,1,1,1,1,1,1,1,1,12,1,1,1,13,1,1,1,1,1,1,1,1,1,1,1,1,13,1,1,14,1,1,1,1,1,1,1,1,1,1,1,1,1,14,1,15,1,1,1,1,1,1,1,1,1,1,1,1,1,1,15]),
    function(^(_,_), [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,0,2,2,0,9,0,0,7,7,9,0,0,0,0,0,0,0,3,0,3,0,0,0,0,0,0,0,0,0,0,0,0,0,4,9,0,4,5,0,0,5,9,0,0,0,0,0,0,0,5,0,0,5,5,0,0,5,0,0,0,0,0,0,0,0,6,0,0,0,0,6,0,0,0,0,0,0,0,0,0,0,7,7,0,0,0,0,7,7,0,0,0,0,0,0,0,0,8,7,0,5,5,0,7,8,0,0,0,0,0,0,0,0,9,9,0,9,0,0,0,0,9,0,0,0,0,0,0,0,10,0,0,0,0,0,0,0,0,10,0,0,0,0,0,0,11,0,0,0,0,0,0,0,0,0,11,0,0,0,0,0,12,0,0,0,0,0,0,0,0,0,0,12,0,0,0,0,13,0,0,0,0,0,0,0,0,0,0,0,13,0,0,0,14,0,0,0,0,0,0,0,0,0,0,0,0,14,0,0,15,0,0,0,0,0,0,0,0,0,0,0,0,0,15]),
    function(f(_,_), [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,5,6,7,2,3,4,9,8,11,10,13,12,15,14,1,5,5,1,8,1,1,4,4,8,1,1,1,1,1,1,1,6,1,6,1,1,1,1,1,1,1,1,1,1,1,1,1,7,8,1,7,2,1,1,2,8,1,1,1,1,1,1,1,2,1,1,2,2,1,1,2,1,1,1,1,1,1,1,1,3,1,1,1,1,3,1,1,1,1,1,1,1,1,1,1,4,4,1,1,1,1,4,4,1,1,1,1,1,1,1,1,9,4,1,2,2,1,4,9,1,1,1,1,1,1,1,1,8,8,1,8,1,1,1,1,8,1,1,1,1,1,1,1,11,1,1,1,1,1,1,1,1,11,1,1,1,1,1,1,10,1,1,1,1,1,1,1,1,1,10,1,1,1,1,1,13,1,1,1,1,1,1,1,1,1,1,13,1,1,1,1,12,1,1,1,1,1,1,1,1,1,1,1,12,1,1,1,15,1,1,1,1,1,1,1,1,1,1,1,1,15,1,1,14,1,1,1,1,1,1,1,1,1,1,1,1,1,14])]).
interpretation(16, [], [
    function(c(_), [1,0,5,6,7,2,3,4,9,8,11,10,13,12,15,14]),
    function(v(_,_), [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,2,1,2,1,1,1,1,2,1,2,1,1,1,1,1,1,3,1,1,3,1,1,1,1,1,1,1,1,1,1,1,1,4,1,1,1,4,4,1,1,1,4,1,1,1,1,1,1,5,1,1,1,4,5,1,8,8,4,1,1,1,1,1,1,6,1,1,1,1,1,6,1,1,1,1,1,1,1,1,1,7,1,2,1,1,8,1,7,8,2,1,1,1,1,1,1,8,1,1,1,1,8,1,8,8,1,1,1,1,1,1,1,9,1,2,1,4,4,1,2,1,9,1,1,1,1,1,1,10,1,1,1,1,1,1,1,1,1,10,1,1,10,1,10,11,1,1,1,1,1,1,1,1,1,1,11,12,14,14,12,12,1,1,1,1,1,1,1,1,1,1,12,12,1,1,12,13,1,1,1,1,1,1,1,1,1,10,14,1,13,14,10,14,1,1,1,1,1,1,1,1,1,1,14,1,14,14,1,15,1,1,1,1,1,1,1,1,1,10,12,12,10,1,15]),
    function(^(_,_), [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,0,2,2,0,9,0,0,7,7,9,0,0,0,0,0,0,0,3,0,3,0,0,0,0,0,0,0,0,0,0,0,0,0,4,9,0,4,5,0,0,5,9,0,0,0,0,0,0,0,5,0,0,5,5,0,0,5,0,0,0,0,0,0,0,0,6,0,0,0,0,6,0,0,0,0,0,0,0,0,0,0,7,7,0,0,0,0,7,7,0,0,0,0,0,0,0,0,8,7,0,5,5,0,7,8,0,0,0,0,0,0,0,0,9,9,0,9,0,0,0,0,9,0,0,0,0,0,0,0,10,0,0,0,0,0,0,0,0,10,0,15,13,13,15,0,11,0,0,0,0,0,0,0,0,0,11,11,0,11,0,0,12,0,0,0,0,0,0,0,0,15,11,12,0,11,15,0,13,0,0,0,0,0,0,0,0,13,0,0,13,13,0,0,14,0,0,0,0,0,0,0,0,13,11,11,13,14,0,0,15,0,0,0,0,0,0,0,0,15,0,15,0,0,15]),
    function(f(_,_), [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,0,5,6,7,2,3,4,9,8,11,10,13,12,15,14,1,5,5,1,8,1,1,4,4,8,1,1,1,1,1,1,1,6,1,6,1,1,1,1,1,1,1,1,1,1,1,1,1,7,8,1,7,2,1,1,2,8,1,1,1,1,1,1,1,2,1,1,2,2,1,1,2,1,1,1,1,1,1,1,1,3,1,1,1,1,3,1,1,1,1,1,1,1,1,1,1,4,4,1,1,1,1,4,4,1,1,1,1,1,1,1,1,9,4,1,2,2,1,4,9,1,1,1,1,1,1,1,1,8,8,1,8,1,1,1,1,8,1,1,1,1,1,1,1,11,1,1,1,1,1,1,1,1,11,1,14,12,12,14,1,10,1,1,1,1,1,1,1,1,1,10,10,1,10,1,1,13,1,1,1,1,1,1,1,1,14,10,13,1,10,14,1,12,1,1,1,1,1,1,1,1,12,1,1,12,12,1,1,15,1,1,1,1,1,1,1,1,12,10,10,12,15,1,1,14,1,1,1,1,1,1,1,1,14,1,14,1,1,14])]).
% isofilter: input=61, kept=4, checks=57, perms=993828, 3.45 seconds.