Tool CaT
| Execution Time | Unknown |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | SK90 4.47 |
|---|
stdout:
YES(?,O(n^1))
Problem:
f(g(i(a(),b(),b'()),c()),d()) -> if(e(),f(.(b(),c()),d'()),f(.(b'(),c()),d'()))
f(g(h(a(),b()),c()),d()) -> if(e(),f(.(b(),g(h(a(),b()),c())),d()),f(c(),d'()))
Proof:
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {13}
transitions:
if1(22,40,34) -> 13*
if1(22,21,18) -> 13*
e1() -> 22*
f1(17,14) -> 18*
f1(39,35) -> 40*
f1(20,14) -> 21*
f1(15,14) -> 34*
.1(19,38) -> 39*
.1(19,15) -> 20*
.1(16,15) -> 17*
b1() -> 19*
g1(37,15) -> 38*
h1(36,19) -> 37*
a1() -> 36*
c1() -> 15*
d1() -> 35*
d'1() -> 14*
b'1() -> 16*
f0(7,12) -> 13*
f0(2,12) -> 13*
f0(8,1) -> 13*
f0(3,1) -> 13*
f0(8,3) -> 13*
f0(3,3) -> 13*
f0(8,5) -> 13*
f0(3,5) -> 13*
f0(8,7) -> 13*
f0(3,7) -> 13*
f0(8,9) -> 13*
f0(3,9) -> 13*
f0(8,11) -> 13*
f0(3,11) -> 13*
f0(9,2) -> 13*
f0(4,2) -> 13*
f0(9,4) -> 13*
f0(4,4) -> 13*
f0(9,6) -> 13*
f0(4,6) -> 13*
f0(9,8) -> 13*
f0(4,8) -> 13*
f0(9,10) -> 13*
f0(4,10) -> 13*
f0(9,12) -> 13*
f0(4,12) -> 13*
f0(10,1) -> 13*
f0(5,1) -> 13*
f0(10,3) -> 13*
f0(5,3) -> 13*
f0(10,5) -> 13*
f0(5,5) -> 13*
f0(10,7) -> 13*
f0(5,7) -> 13*
f0(10,9) -> 13*
f0(5,9) -> 13*
f0(10,11) -> 13*
f0(5,11) -> 13*
f0(11,2) -> 13*
f0(6,2) -> 13*
f0(1,2) -> 13*
f0(11,4) -> 13*
f0(6,4) -> 13*
f0(1,4) -> 13*
f0(11,6) -> 13*
f0(6,6) -> 13*
f0(1,6) -> 13*
f0(11,8) -> 13*
f0(6,8) -> 13*
f0(1,8) -> 13*
f0(11,10) -> 13*
f0(6,10) -> 13*
f0(1,10) -> 13*
f0(11,12) -> 13*
f0(6,12) -> 13*
f0(1,12) -> 13*
f0(12,1) -> 13*
f0(7,1) -> 13*
f0(2,1) -> 13*
f0(12,3) -> 13*
f0(7,3) -> 13*
f0(2,3) -> 13*
f0(12,5) -> 13*
f0(7,5) -> 13*
f0(2,5) -> 13*
f0(12,7) -> 13*
f0(7,7) -> 13*
f0(2,7) -> 13*
f0(12,9) -> 13*
f0(7,9) -> 13*
f0(2,9) -> 13*
f0(12,11) -> 13*
f0(7,11) -> 13*
f0(2,11) -> 13*
f0(8,2) -> 13*
f0(3,2) -> 13*
f0(8,4) -> 13*
f0(3,4) -> 13*
f0(8,6) -> 13*
f0(3,6) -> 13*
f0(8,8) -> 13*
f0(3,8) -> 13*
f0(8,10) -> 13*
f0(3,10) -> 13*
f0(8,12) -> 13*
f0(3,12) -> 13*
f0(9,1) -> 13*
f0(4,1) -> 13*
f0(9,3) -> 13*
f0(4,3) -> 13*
f0(9,5) -> 13*
f0(4,5) -> 13*
f0(9,7) -> 13*
f0(4,7) -> 13*
f0(9,9) -> 13*
f0(4,9) -> 13*
f0(9,11) -> 13*
f0(4,11) -> 13*
f0(10,2) -> 13*
f0(5,2) -> 13*
f0(10,4) -> 13*
f0(5,4) -> 13*
f0(10,6) -> 13*
f0(5,6) -> 13*
f0(10,8) -> 13*
f0(5,8) -> 13*
f0(10,10) -> 13*
f0(5,10) -> 13*
f0(10,12) -> 13*
f0(5,12) -> 13*
f0(11,1) -> 13*
f0(6,1) -> 13*
f0(1,1) -> 13*
f0(11,3) -> 13*
f0(6,3) -> 13*
f0(1,3) -> 13*
f0(11,5) -> 13*
f0(6,5) -> 13*
f0(1,5) -> 13*
f0(11,7) -> 13*
f0(6,7) -> 13*
f0(1,7) -> 13*
f0(11,9) -> 13*
f0(6,9) -> 13*
f0(1,9) -> 13*
f0(11,11) -> 13*
f0(6,11) -> 13*
f0(1,11) -> 13*
f0(12,2) -> 13*
f0(7,2) -> 13*
f0(2,2) -> 13*
f0(12,4) -> 13*
f0(7,4) -> 13*
f0(2,4) -> 13*
f0(12,6) -> 13*
f0(7,6) -> 13*
f0(2,6) -> 13*
f0(12,8) -> 13*
f0(7,8) -> 13*
f0(2,8) -> 13*
f0(12,10) -> 13*
f0(7,10) -> 13*
f0(2,10) -> 13*
f0(12,12) -> 13*
g0(7,12) -> 12*
g0(2,12) -> 12*
g0(8,1) -> 12*
g0(3,1) -> 12*
g0(8,3) -> 12*
g0(3,3) -> 12*
g0(8,5) -> 12*
g0(3,5) -> 12*
g0(8,7) -> 12*
g0(3,7) -> 12*
g0(8,9) -> 12*
g0(3,9) -> 12*
g0(8,11) -> 12*
g0(3,11) -> 12*
g0(9,2) -> 12*
g0(4,2) -> 12*
g0(9,4) -> 12*
g0(4,4) -> 12*
g0(9,6) -> 12*
g0(4,6) -> 12*
g0(9,8) -> 12*
g0(4,8) -> 12*
g0(9,10) -> 12*
g0(4,10) -> 12*
g0(9,12) -> 12*
g0(4,12) -> 12*
g0(10,1) -> 12*
g0(5,1) -> 12*
g0(10,3) -> 12*
g0(5,3) -> 12*
g0(10,5) -> 12*
g0(5,5) -> 12*
g0(10,7) -> 12*
g0(5,7) -> 12*
g0(10,9) -> 12*
g0(5,9) -> 12*
g0(10,11) -> 12*
g0(5,11) -> 12*
g0(11,2) -> 12*
g0(6,2) -> 12*
g0(1,2) -> 12*
g0(11,4) -> 12*
g0(6,4) -> 12*
g0(1,4) -> 12*
g0(11,6) -> 12*
g0(6,6) -> 12*
g0(1,6) -> 12*
g0(11,8) -> 12*
g0(6,8) -> 12*
g0(1,8) -> 12*
g0(11,10) -> 12*
g0(6,10) -> 12*
g0(1,10) -> 12*
g0(11,12) -> 12*
g0(6,12) -> 12*
g0(1,12) -> 12*
g0(12,1) -> 12*
g0(7,1) -> 12*
g0(2,1) -> 12*
g0(12,3) -> 12*
g0(7,3) -> 12*
g0(2,3) -> 12*
g0(12,5) -> 12*
g0(7,5) -> 12*
g0(2,5) -> 12*
g0(12,7) -> 12*
g0(7,7) -> 12*
g0(2,7) -> 12*
g0(12,9) -> 12*
g0(7,9) -> 12*
g0(2,9) -> 12*
g0(12,11) -> 12*
g0(7,11) -> 12*
g0(2,11) -> 12*
g0(8,2) -> 12*
g0(3,2) -> 12*
g0(8,4) -> 12*
g0(3,4) -> 12*
g0(8,6) -> 12*
g0(3,6) -> 12*
g0(8,8) -> 12*
g0(3,8) -> 12*
g0(8,10) -> 12*
g0(3,10) -> 12*
g0(8,12) -> 12*
g0(3,12) -> 12*
g0(9,1) -> 12*
g0(4,1) -> 12*
g0(9,3) -> 12*
g0(4,3) -> 12*
g0(9,5) -> 12*
g0(4,5) -> 12*
g0(9,7) -> 12*
g0(4,7) -> 12*
g0(9,9) -> 12*
g0(4,9) -> 12*
g0(9,11) -> 12*
g0(4,11) -> 12*
g0(10,2) -> 12*
g0(5,2) -> 12*
g0(10,4) -> 12*
g0(5,4) -> 12*
g0(10,6) -> 12*
g0(5,6) -> 12*
g0(10,8) -> 12*
g0(5,8) -> 12*
g0(10,10) -> 12*
g0(5,10) -> 12*
g0(10,12) -> 12*
g0(5,12) -> 12*
g0(11,1) -> 12*
g0(6,1) -> 12*
g0(1,1) -> 12*
g0(11,3) -> 12*
g0(6,3) -> 12*
g0(1,3) -> 12*
g0(11,5) -> 12*
g0(6,5) -> 12*
g0(1,5) -> 12*
g0(11,7) -> 12*
g0(6,7) -> 12*
g0(1,7) -> 12*
g0(11,9) -> 12*
g0(6,9) -> 12*
g0(1,9) -> 12*
g0(11,11) -> 12*
g0(6,11) -> 12*
g0(1,11) -> 12*
g0(12,2) -> 12*
g0(7,2) -> 12*
g0(2,2) -> 12*
g0(12,4) -> 12*
g0(7,4) -> 12*
g0(2,4) -> 12*
g0(12,6) -> 12*
g0(7,6) -> 12*
g0(2,6) -> 12*
g0(12,8) -> 12*
g0(7,8) -> 12*
g0(2,8) -> 12*
g0(12,10) -> 12*
g0(7,10) -> 12*
g0(2,10) -> 12*
g0(12,12) -> 12*
i0(5,2,1) -> 11*
i0(9,8,3) -> 11*
i0(2,7,8) -> 11*
i0(3,2,2) -> 11*
i0(12,9,8) -> 11*
i0(6,3,7) -> 11*
i0(10,9,9) -> 11*
i0(9,4,12) -> 11*
i0(4,8,3) -> 11*
i0(10,4,1) -> 11*
i0(7,9,8) -> 11*
i0(8,4,2) -> 11*
i0(1,3,7) -> 11*
i0(5,9,9) -> 11*
i0(11,5,7) -> 11*
i0(4,4,12) -> 11*
i0(5,4,1) -> 11*
i0(9,10,3) -> 11*
i0(2,9,8) -> 11*
i0(3,4,2) -> 11*
i0(12,11,8) -> 11*
i0(6,5,7) -> 11*
i0(10,11,9) -> 11*
i0(12,1,5) -> 11*
i0(9,6,12) -> 11*
i0(10,1,6) -> 11*
i0(4,10,3) -> 11*
i0(10,6,1) -> 11*
i0(7,11,8) -> 11*
i0(8,6,2) -> 11*
i0(1,5,7) -> 11*
i0(5,11,9) -> 11*
i0(7,1,5) -> 11*
i0(11,7,7) -> 11*
i0(4,6,12) -> 11*
i0(5,1,6) -> 11*
i0(8,2,11) -> 11*
i0(5,6,1) -> 11*
i0(9,12,3) -> 11*
i0(2,11,8) -> 11*
i0(3,6,2) -> 11*
i0(2,1,5) -> 11*
i0(6,7,7) -> 11*
i0(12,3,5) -> 11*
i0(9,8,12) -> 11*
i0(10,3,6) -> 11*
i0(3,2,11) -> 11*
i0(4,12,3) -> 11*
i0(10,8,1) -> 11*
i0(8,8,2) -> 11*
i0(1,7,7) -> 11*
i0(7,3,5) -> 11*
i0(11,9,7) -> 11*
i0(4,8,12) -> 11*
i0(5,3,6) -> 11*
i0(8,4,11) -> 11*
i0(5,8,1) -> 11*
i0(3,8,2) -> 11*
i0(2,3,5) -> 11*
i0(6,9,7) -> 11*
i0(12,5,5) -> 11*
i0(9,10,12) -> 11*
i0(10,5,6) -> 11*
i0(3,4,11) -> 11*
i0(10,10,1) -> 11*
i0(8,10,2) -> 11*
i0(1,9,7) -> 11*
i0(7,5,5) -> 11*
i0(11,11,7) -> 11*
i0(4,10,12) -> 11*
i0(5,5,6) -> 11*
i0(11,1,4) -> 11*
i0(8,6,11) -> 11*
i0(5,10,1) -> 11*
i0(12,2,10) -> 11*
i0(3,10,2) -> 11*
i0(2,5,5) -> 11*
i0(6,11,7) -> 11*
i0(12,7,5) -> 11*
i0(6,1,4) -> 11*
i0(9,12,12) -> 11*
i0(10,7,6) -> 11*
i0(3,6,11) -> 11*
i0(7,2,10) -> 11*
i0(10,12,1) -> 11*
i0(8,12,2) -> 11*
i0(1,11,7) -> 11*
i0(7,7,5) -> 11*
i0(1,1,4) -> 11*
i0(4,12,12) -> 11*
i0(5,7,6) -> 11*
i0(11,3,4) -> 11*
i0(8,8,11) -> 11*
i0(2,2,10) -> 11*
i0(5,12,1) -> 11*
i0(12,4,10) -> 11*
i0(3,12,2) -> 11*
i0(2,7,5) -> 11*
i0(12,9,5) -> 11*
i0(6,3,4) -> 11*
i0(10,9,6) -> 11*
i0(3,8,11) -> 11*
i0(7,4,10) -> 11*
i0(7,9,5) -> 11*
i0(1,3,4) -> 11*
i0(5,9,6) -> 11*
i0(11,5,4) -> 11*
i0(8,10,11) -> 11*
i0(2,4,10) -> 11*
i0(12,6,10) -> 11*
i0(2,9,5) -> 11*
i0(12,11,5) -> 11*
i0(6,5,4) -> 11*
i0(10,11,6) -> 11*
i0(3,10,11) -> 11*
i0(10,1,3) -> 11*
i0(7,6,10) -> 11*
i0(11,2,9) -> 11*
i0(7,11,5) -> 11*
i0(1,5,4) -> 11*
i0(5,11,6) -> 11*
i0(11,7,4) -> 11*
i0(5,1,3) -> 11*
i0(8,12,11) -> 11*
i0(2,6,10) -> 11*
i0(8,2,8) -> 11*
i0(12,8,10) -> 11*
i0(6,2,9) -> 11*
i0(2,11,5) -> 11*
i0(6,7,4) -> 11*
i0(3,12,11) -> 11*
i0(10,3,3) -> 11*
i0(3,2,8) -> 11*
i0(7,8,10) -> 11*
i0(1,2,9) -> 11*
i0(11,4,9) -> 11*
i0(1,7,4) -> 11*
i0(11,9,4) -> 11*
i0(5,3,3) -> 11*
i0(2,8,10) -> 11*
i0(8,4,8) -> 11*
i0(12,10,10) -> 11*
i0(6,4,9) -> 11*
i0(6,9,4) -> 11*
i0(10,5,3) -> 11*
i0(3,4,8) -> 11*
i0(7,10,10) -> 11*
i0(1,4,9) -> 11*
i0(11,6,9) -> 11*
i0(10,1,12) -> 11*
i0(1,9,4) -> 11*
i0(11,11,4) -> 11*
i0(5,5,3) -> 11*
i0(11,1,1) -> 11*
i0(2,10,10) -> 11*
i0(8,6,8) -> 11*
i0(9,1,2) -> 11*
i0(12,12,10) -> 11*
i0(6,6,9) -> 11*
i0(12,2,7) -> 11*
i0(5,1,12) -> 11*
i0(6,11,4) -> 11*
i0(6,1,1) -> 11*
i0(10,7,3) -> 11*
i0(3,6,8) -> 11*
i0(4,1,2) -> 11*
i0(7,12,10) -> 11*
i0(1,6,9) -> 11*
i0(7,2,7) -> 11*
i0(11,8,9) -> 11*
i0(10,3,12) -> 11*
i0(1,11,4) -> 11*
i0(1,1,1) -> 11*
i0(5,7,3) -> 11*
i0(11,3,1) -> 11*
i0(2,12,10) -> 11*
i0(8,8,8) -> 11*
i0(9,3,2) -> 11*
i0(2,2,7) -> 11*
i0(6,8,9) -> 11*
i0(12,4,7) -> 11*
i0(5,3,12) -> 11*
i0(6,3,1) -> 11*
i0(10,9,3) -> 11*
i0(3,8,8) -> 11*
i0(4,3,2) -> 11*
i0(1,8,9) -> 11*
i0(7,4,7) -> 11*
i0(11,10,9) -> 11*
i0(10,5,12) -> 11*
i0(1,3,1) -> 11*
i0(5,9,3) -> 11*
i0(11,5,1) -> 11*
i0(8,10,8) -> 11*
i0(9,5,2) -> 11*
i0(2,4,7) -> 11*
i0(6,10,9) -> 11*
i0(12,6,7) -> 11*
i0(5,5,12) -> 11*
i0(9,1,11) -> 11*
i0(6,5,1) -> 11*
i0(10,11,3) -> 11*
i0(3,10,8) -> 11*
i0(4,5,2) -> 11*
i0(1,10,9) -> 11*
i0(7,6,7) -> 11*
i0(11,12,9) -> 11*
i0(10,7,12) -> 11*
i0(11,2,6) -> 11*
i0(4,1,11) -> 11*
i0(1,5,1) -> 11*
i0(5,11,3) -> 11*
i0(11,7,1) -> 11*
i0(8,12,8) -> 11*
i0(9,7,2) -> 11*
i0(2,6,7) -> 11*
i0(6,12,9) -> 11*
i0(8,2,5) -> 11*
i0(12,8,7) -> 11*
i0(5,7,12) -> 11*
i0(6,2,6) -> 11*
i0(9,3,11) -> 11*
i0(6,7,1) -> 11*
i0(3,12,8) -> 11*
i0(4,7,2) -> 11*
i0(1,12,9) -> 11*
i0(3,2,5) -> 11*
i0(7,8,7) -> 11*
i0(1,2,6) -> 11*
i0(10,9,12) -> 11*
i0(11,4,6) -> 11*
i0(4,3,11) -> 11*
i0(1,7,1) -> 11*
i0(11,9,1) -> 11*
i0(9,9,2) -> 11*
i0(2,8,7) -> 11*
i0(8,4,5) -> 11*
i0(12,10,7) -> 11*
i0(5,9,12) -> 11*
i0(6,4,6) -> 11*
i0(9,5,11) -> 11*
i0(6,9,1) -> 11*
i0(4,9,2) -> 11*
i0(3,4,5) -> 11*
i0(7,10,7) -> 11*
i0(1,4,6) -> 11*
i0(10,11,12) -> 11*
i0(11,6,6) -> 11*
i0(4,5,11) -> 11*
i0(1,9,1) -> 11*
i0(8,1,10) -> 11*
i0(11,11,1) -> 11*
i0(9,11,2) -> 11*
i0(2,10,7) -> 11*
i0(8,6,5) -> 11*
i0(12,12,7) -> 11*
i0(5,11,12) -> 11*
i0(6,6,6) -> 11*
i0(12,2,4) -> 11*
i0(9,7,11) -> 11*
i0(3,1,10) -> 11*
i0(6,11,1) -> 11*
i0(4,11,2) -> 11*
i0(3,6,5) -> 11*
i0(7,12,7) -> 11*
i0(1,6,6) -> 11*
i0(7,2,4) -> 11*
i0(11,8,6) -> 11*
i0(4,7,11) -> 11*
i0(1,11,1) -> 11*
i0(8,3,10) -> 11*
i0(2,12,7) -> 11*
i0(8,8,5) -> 11*
i0(2,2,4) -> 11*
i0(6,8,6) -> 11*
i0(12,4,4) -> 11*
i0(9,9,11) -> 11*
i0(3,3,10) -> 11*
i0(3,8,5) -> 11*
i0(1,8,6) -> 11*
i0(7,4,4) -> 11*
i0(11,10,6) -> 11*
i0(4,9,11) -> 11*
i0(8,5,10) -> 11*
i0(12,1,9) -> 11*
i0(8,10,5) -> 11*
i0(2,4,4) -> 11*
i0(6,10,6) -> 11*
i0(12,6,4) -> 11*
i0(9,11,11) -> 11*
i0(3,5,10) -> 11*
i0(9,1,8) -> 11*
i0(7,1,9) -> 11*
i0(3,10,5) -> 11*
i0(1,10,6) -> 11*
i0(7,6,4) -> 11*
i0(11,12,6) -> 11*
i0(4,11,11) -> 11*
i0(11,2,3) -> 11*
i0(4,1,8) -> 11*
i0(8,7,10) -> 11*
i0(2,1,9) -> 11*
i0(12,3,9) -> 11*
i0(8,12,5) -> 11*
i0(2,6,4) -> 11*
i0(6,12,6) -> 11*
i0(12,8,4) -> 11*
i0(6,2,3) -> 11*
i0(3,7,10) -> 11*
i0(9,3,8) -> 11*
i0(7,3,9) -> 11*
i0(3,12,5) -> 11*
i0(1,12,6) -> 11*
i0(7,8,4) -> 11*
i0(1,2,3) -> 11*
i0(11,4,3) -> 11*
i0(4,3,8) -> 11*
i0(8,9,10) -> 11*
i0(2,3,9) -> 11*
i0(12,5,9) -> 11*
i0(2,8,4) -> 11*
i0(12,10,4) -> 11*
i0(6,4,3) -> 11*
i0(3,9,10) -> 11*
i0(9,5,8) -> 11*
i0(7,5,9) -> 11*
i0(7,10,4) -> 11*
i0(1,4,3) -> 11*
i0(11,6,3) -> 11*
i0(4,5,8) -> 11*
i0(8,11,10) -> 11*
i0(2,5,9) -> 11*
i0(8,1,7) -> 11*
i0(12,7,9) -> 11*
i0(11,2,12) -> 11*
i0(2,10,4) -> 11*
i0(12,12,4) -> 11*
i0(6,6,3) -> 11*
i0(12,2,1) -> 11*
i0(3,11,10) -> 11*
i0(9,7,8) -> 11*
i0(10,2,2) -> 11*
i0(3,1,7) -> 11*
i0(7,7,9) -> 11*
i0(6,2,12) -> 11*
i0(7,12,4) -> 11*
i0(1,6,3) -> 11*
i0(7,2,1) -> 11*
i0(11,8,3) -> 11*
i0(4,7,8) -> 11*
i0(5,2,2) -> 11*
i0(2,7,9) -> 11*
i0(8,3,7) -> 11*
i0(12,9,9) -> 11*
i0(1,2,12) -> 11*
i0(11,4,12) -> 11*
i0(2,12,4) -> 11*
i0(2,2,1) -> 11*
i0(6,8,3) -> 11*
i0(12,4,1) -> 11*
i0(9,9,8) -> 11*
i0(10,4,2) -> 11*
i0(3,3,7) -> 11*
i0(7,9,9) -> 11*
i0(6,4,12) -> 11*
i0(1,8,3) -> 11*
i0(7,4,1) -> 11*
i0(11,10,3) -> 11*
i0(4,9,8) -> 11*
i0(5,4,2) -> 11*
i0(2,9,9) -> 11*
i0(8,5,7) -> 11*
i0(12,11,9) -> 11*
i0(1,4,12) -> 11*
i0(11,6,12) -> 11*
i0(12,1,6) -> 11*
i0(2,4,1) -> 11*
i0(6,10,3) -> 11*
i0(12,6,1) -> 11*
i0(9,11,8) -> 11*
i0(10,6,2) -> 11*
i0(3,5,7) -> 11*
i0(7,11,9) -> 11*
i0(9,1,5) -> 11*
i0(6,6,12) -> 11*
i0(7,1,6) -> 11*
i0(10,2,11) -> 11*
i0(1,10,3) -> 11*
i0(7,6,1) -> 11*
i0(11,12,3) -> 11*
i0(4,11,8) -> 11*
i0(5,6,2) -> 11*
i0(2,11,9) -> 11*
i0(4,1,5) -> 11*
i0(8,7,7) -> 11*
i0(1,6,12) -> 11*
i0(2,1,6) -> 11*
i0(11,8,12) -> 11*
i0(12,3,6) -> 11*
i0(5,2,11) -> 11*
i0(2,6,1) -> 11*
i0(6,12,3) -> 11*
i0(12,8,1) -> 11*
i0(10,8,2) -> 11*
i0(3,7,7) -> 11*
i0(9,3,5) -> 11*
i0(6,8,12) -> 11*
i0(7,3,6) -> 11*
i0(10,4,11) -> 11*
i0(1,12,3) -> 11*
i0(7,8,1) -> 11*
i0(5,8,2) -> 11*
i0(4,3,5) -> 11*
i0(8,9,7) -> 11*
i0(1,8,12) -> 11*
i0(2,3,6) -> 11*
i0(11,10,12) -> 11*
i0(12,5,6) -> 11*
i0(5,4,11) -> 11*
i0(2,8,1) -> 11*
i0(12,10,1) -> 11*
i0(10,10,2) -> 11*
i0(3,9,7) -> 11*
i0(9,5,5) -> 11*
i0(6,10,12) -> 11*
i0(7,5,6) -> 11*
i0(10,6,11) -> 11*
i0(7,10,1) -> 11*
i0(5,10,2) -> 11*
i0(4,5,5) -> 11*
i0(8,11,7) -> 11*
i0(1,10,12) -> 11*
i0(2,5,6) -> 11*
i0(8,1,4) -> 11*
i0(11,12,12) -> 11*
i0(12,7,6) -> 11*
i0(5,6,11) -> 11*
i0(2,10,1) -> 11*
i0(9,2,10) -> 11*
i0(12,12,1) -> 11*
i0(10,12,2) -> 11*
i0(3,11,7) -> 11*
i0(9,7,5) -> 11*
i0(3,1,4) -> 11*
i0(6,12,12) -> 11*
i0(7,7,6) -> 11*
i0(10,8,11) -> 11*
i0(4,2,10) -> 11*
i0(7,12,1) -> 11*
i0(5,12,2) -> 11*
i0(4,7,5) -> 11*
i0(1,12,12) -> 11*
i0(2,7,6) -> 11*
i0(8,3,4) -> 11*
i0(12,9,6) -> 11*
i0(5,8,11) -> 11*
i0(2,12,1) -> 11*
i0(9,4,10) -> 11*
i0(9,9,5) -> 11*
i0(3,3,4) -> 11*
i0(7,9,6) -> 11*
i0(10,10,11) -> 11*
i0(4,4,10) -> 11*
i0(4,9,5) -> 11*
i0(2,9,6) -> 11*
i0(8,5,4) -> 11*
i0(12,11,6) -> 11*
i0(5,10,11) -> 11*
i0(12,1,3) -> 11*
i0(9,6,10) -> 11*
i0(9,11,5) -> 11*
i0(3,5,4) -> 11*
i0(7,11,6) -> 11*
i0(7,1,3) -> 11*
i0(10,12,11) -> 11*
i0(4,6,10) -> 11*
i0(10,2,8) -> 11*
i0(8,2,9) -> 11*
i0(4,11,5) -> 11*
i0(2,11,6) -> 11*
i0(8,7,4) -> 11*
i0(2,1,3) -> 11*
i0(5,12,11) -> 11*
i0(12,3,3) -> 11*
i0(5,2,8) -> 11*
i0(9,8,10) -> 11*
i0(3,2,9) -> 11*
i0(3,7,4) -> 11*
i0(7,3,3) -> 11*
i0(4,8,10) -> 11*
i0(10,4,8) -> 11*
i0(8,4,9) -> 11*
i0(8,9,4) -> 11*
i0(2,3,3) -> 11*
i0(12,5,3) -> 11*
i0(5,4,8) -> 11*
i0(9,10,10) -> 11*
i0(3,4,9) -> 11*
i0(12,1,12) -> 11*
i0(3,9,4) -> 11*
i0(7,5,3) -> 11*
i0(4,10,10) -> 11*
i0(10,6,8) -> 11*
i0(11,1,2) -> 11*
i0(8,6,9) -> 11*
i0(7,1,12) -> 11*
i0(8,11,4) -> 11*
i0(2,5,3) -> 11*
i0(8,1,1) -> 11*
i0(12,7,3) -> 11*
i0(5,6,8) -> 11*
i0(6,1,2) -> 11*
i0(9,12,10) -> 11*
i0(3,6,9) -> 11*
i0(9,2,7) -> 11*
i0(2,1,12) -> 11*
i0(12,3,12) -> 11*
i0(3,11,4) -> 11*
i0(3,1,1) -> 11*
i0(7,7,3) -> 11*
i0(1,1,2) -> 11*
i0(4,12,10) -> 11*
i0(10,8,8) -> 11*
i0(11,3,2) -> 11*
i0(4,2,7) -> 11*
i0(8,8,9) -> 11*
i0(7,3,12) -> 11*
i0(2,7,3) -> 11*
i0(8,3,1) -> 11*
i0(12,9,3) -> 11*
i0(5,8,8) -> 11*
i0(6,3,2) -> 11*
i0(3,8,9) -> 11*
i0(9,4,7) -> 11*
i0(2,3,12) -> 11*
i0(12,5,12) -> 11*
i0(3,3,1) -> 11*
i0(7,9,3) -> 11*
i0(1,3,2) -> 11*
i0(10,10,8) -> 11*
i0(11,5,2) -> 11*
i0(4,4,7) -> 11*
i0(8,10,9) -> 11*
i0(7,5,12) -> 11*
i0(11,1,11) -> 11*
i0(2,9,3) -> 11*
i0(8,5,1) -> 11*
i0(12,11,3) -> 11*
i0(5,10,8) -> 11*
i0(6,5,2) -> 11*
i0(3,10,9) -> 11*
i0(9,6,7) -> 11*
i0(2,5,12) -> 11*
i0(12,7,12) -> 11*
i0(6,1,11) -> 11*
i0(3,5,1) -> 11*
i0(7,11,3) -> 11*
i0(1,5,2) -> 11*
i0(10,12,8) -> 11*
i0(11,7,2) -> 11*
i0(4,6,7) -> 11*
i0(8,12,9) -> 11*
i0(10,2,5) -> 11*
i0(7,7,12) -> 11*
i0(8,2,6) -> 11*
i0(1,1,11) -> 11*
i0(11,3,11) -> 11*
i0(2,11,3) -> 11*
i0(8,7,1) -> 11*
i0(5,12,8) -> 11*
i0(6,7,2) -> 11*
i0(3,12,9) -> 11*
i0(5,2,5) -> 11*
i0(9,8,7) -> 11*
i0(2,7,12) -> 11*
i0(3,2,6) -> 11*
i0(12,9,12) -> 11*
i0(6,3,11) -> 11*
i0(3,7,1) -> 11*
i0(1,7,2) -> 11*
i0(11,9,2) -> 11*
i0(4,8,7) -> 11*
i0(10,4,5) -> 11*
i0(7,9,12) -> 11*
i0(8,4,6) -> 11*
i0(1,3,11) -> 11*
i0(11,5,11) -> 11*
i0(8,9,1) -> 11*
i0(6,9,2) -> 11*
i0(5,4,5) -> 11*
i0(9,10,7) -> 11*
i0(2,9,12) -> 11*
i0(3,4,6) -> 11*
i0(12,11,12) -> 11*
i0(6,5,11) -> 11*
i0(3,9,1) -> 11*
i0(10,1,10) -> 11*
i0(1,9,2) -> 11*
i0(11,11,2) -> 11*
i0(4,10,7) -> 11*
i0(10,6,5) -> 11*
i0(7,11,12) -> 11*
i0(8,6,6) -> 11*
i0(1,5,11) -> 11*
i0(11,7,11) -> 11*
i0(5,1,10) -> 11*
i0(8,11,1) -> 11*
i0(6,11,2) -> 11*
i0(5,6,5) -> 11*
i0(9,12,7) -> 11*
i0(2,11,12) -> 11*
i0(3,6,6) -> 11*
i0(9,2,4) -> 11*
i0(6,7,11) -> 11*
i0(3,11,1) -> 11*
i0(10,3,10) -> 11*
i0(1,11,2) -> 11*
i0(4,12,7) -> 11*
i0(10,8,5) -> 11*
i0(4,2,4) -> 11*
i0(8,8,6) -> 11*
i0(1,7,11) -> 11*
i0(11,9,11) -> 11*
i0(5,3,10) -> 11*
i0(5,8,5) -> 11*
i0(3,8,6) -> 11*
i0(9,4,4) -> 11*
i0(6,9,11) -> 11*
i0(10,5,10) -> 11*
i0(10,10,5) -> 11*
i0(4,4,4) -> 11*
i0(8,10,6) -> 11*
i0(1,9,11) -> 11*
i0(11,11,11) -> 11*
i0(5,5,10) -> 11*
i0(11,1,8) -> 11*
i0(9,1,9) -> 11*
i0(5,10,5) -> 11*
i0(3,10,6) -> 11*
i0(9,6,4) -> 11*
i0(6,11,11) -> 11*
i0(6,1,8) -> 11*
i0(10,7,10) -> 11*
i0(4,1,9) -> 11*
i0(10,12,5) -> 11*
i0(4,6,4) -> 11*
i0(8,12,6) -> 11*
i0(1,11,11) -> 11*
i0(8,2,3) -> 11*
i0(1,1,8) -> 11*
i0(5,7,10) -> 11*
i0(11,3,8) -> 11*
i0(9,3,9) -> 11*
i0(5,12,5) -> 11*
i0(3,12,6) -> 11*
i0(9,8,4) -> 11*
i0(3,2,3) -> 11*
i0(6,3,8) -> 11*
i0(10,9,10) -> 11*
i0(4,3,9) -> 11*
i0(4,8,4) -> 11*
i0(8,4,3) -> 11*
i0(1,3,8) -> 11*
i0(5,9,10) -> 11*
i0(11,5,8) -> 11*
i0(9,5,9) -> 11*
i0(9,10,4) -> 11*
i0(3,4,3) -> 11*
i0(6,5,8) -> 11*
i0(10,11,10) -> 11*
i0(4,5,9) -> 11*
i0(10,1,7) -> 11*
i0(4,10,4) -> 11*
i0(8,6,3) -> 11*
i0(1,5,8) -> 11*
i0(5,11,10) -> 11*
i0(11,7,8) -> 11*
i0(12,2,2) -> 11*
i0(5,1,7) -> 11*
i0(9,7,9) -> 11*
i0(8,2,12) -> 11*
i0(9,12,4) -> 11*
i0(3,6,3) -> 11*
i0(9,2,1) -> 11*
i0(6,7,8) -> 11*
i0(7,2,2) -> 11*
i0(4,7,9) -> 11*
i0(10,3,7) -> 11*
i0(3,2,12) -> 11*
i0(4,12,4) -> 11*
i0(4,2,1) -> 11*
i0(8,8,3) -> 11*
i0(1,7,8) -> 11*
i0(2,2,2) -> 11*
i0(11,9,8) -> 11*
i0(12,4,2) -> 11*
i0(5,3,7) -> 11*
i0(9,9,9) -> 11*
i0(8,4,12) -> 11*
i0(3,8,3) -> 11*
i0(9,4,1) -> 11*
i0(6,9,8) -> 11*
i0(7,4,2) -> 11*
i0(4,9,9) -> 11*
i0(10,5,7) -> 11*
i0(3,4,12) -> 11*
i0(4,4,1) -> 11*
i0(8,10,3) -> 11*
i0(1,9,8) -> 11*
i0(2,4,2) -> 11*
i0(11,11,8) -> 11*
i0(12,6,2) -> 11*
i0(5,5,7) -> 11*
i0(9,11,9) -> 11*
i0(11,1,5) -> 11*
i0(8,6,12) -> 11*
i0(9,1,6) -> 11*
i0(12,2,11) -> 11*
i0(3,10,3) -> 11*
i0(9,6,1) -> 11*
i0(6,11,8) -> 11*
i0(7,6,2) -> 11*
i0(4,11,9) -> 11*
i0(6,1,5) -> 11*
i0(10,7,7) -> 11*
i0(3,6,12) -> 11*
i0(4,1,6) -> 11*
i0(7,2,11) -> 11*
i0(4,6,1) -> 11*
i0(8,12,3) -> 11*
i0(1,11,8) -> 11*
i0(2,6,2) -> 11*
i0(12,8,2) -> 11*
i0(1,1,5) -> 11*
i0(5,7,7) -> 11*
i0(11,3,5) -> 11*
i0(8,8,12) -> 11*
i0(9,3,6) -> 11*
i0(2,2,11) -> 11*
i0(12,4,11) -> 11*
i0(3,12,3) -> 11*
i0(9,8,1) -> 11*
i0(7,8,2) -> 11*
i0(6,3,5) -> 11*
i0(10,9,7) -> 11*
i0(3,8,12) -> 11*
i0(4,3,6) -> 11*
i0(7,4,11) -> 11*
i0(4,8,1) -> 11*
i0(2,8,2) -> 11*
i0(12,10,2) -> 11*
i0(1,3,5) -> 11*
i0(5,9,7) -> 11*
i0(11,5,5) -> 11*
i0(8,10,12) -> 11*
i0(9,5,6) -> 11*
i0(2,4,11) -> 11*
i0(12,6,11) -> 11*
i0(9,10,1) -> 11*
i0(7,10,2) -> 11*
i0(6,5,5) -> 11*
i0(10,11,7) -> 11*
i0(3,10,12) -> 11*
i0(4,5,6) -> 11*
i0(10,1,4) -> 11*
i0(7,6,11) -> 11*
i0(4,10,1) -> 11*
i0(11,2,10) -> 11*
i0(2,10,2) -> 11*
i0(12,12,2) -> 11*
i0(1,5,5) -> 11*
i0(5,11,7) -> 11*
i0(11,7,5) -> 11*
i0(5,1,4) -> 11*
i0(8,12,12) -> 11*
i0(9,7,6) -> 11*
i0(2,6,11) -> 11*
i0(12,8,11) -> 11*
i0(6,2,10) -> 11*
i0(9,12,1) -> 11*
i0(7,12,2) -> 11*
i0(6,7,5) -> 11*
i0(3,12,12) -> 11*
i0(4,7,6) -> 11*
i0(10,3,4) -> 11*
i0(7,8,11) -> 11*
i0(1,2,10) -> 11*
i0(4,12,1) -> 11*
i0(11,4,10) -> 11*
i0(2,12,2) -> 11*
i0(1,7,5) -> 11*
i0(11,9,5) -> 11*
i0(5,3,4) -> 11*
i0(9,9,6) -> 11*
i0(2,8,11) -> 11*
i0(12,10,11) -> 11*
i0(6,4,10) -> 11*
i0(6,9,5) -> 11*
i0(4,9,6) -> 11*
i0(10,5,4) -> 11*
i0(7,10,11) -> 11*
i0(1,4,10) -> 11*
i0(11,6,10) -> 11*
i0(1,9,5) -> 11*
i0(11,11,5) -> 11*
i0(5,5,4) -> 11*
i0(9,11,6) -> 11*
i0(2,10,11) -> 11*
i0(9,1,3) -> 11*
i0(12,12,11) -> 11*
i0(6,6,10) -> 11*
i0(12,2,8) -> 11*
i0(10,2,9) -> 11*
i0(6,11,5) -> 11*
i0(4,11,6) -> 11*
i0(10,7,4) -> 11*
i0(4,1,3) -> 11*
i0(7,12,11) -> 11*
i0(1,6,10) -> 11*
i0(7,2,8) -> 11*
i0(11,8,10) -> 11*
i0(5,2,9) -> 11*
i0(1,11,5) -> 11*
i0(5,7,4) -> 11*
i0(2,12,11) -> 11*
i0(9,3,3) -> 11*
i0(2,2,8) -> 11*
i0(6,8,10) -> 11*
i0(12,4,8) -> 11*
i0(10,4,9) -> 11*
i0(10,9,4) -> 11*
i0(4,3,3) -> 11*
i0(1,8,10) -> 11*
i0(7,4,8) -> 11*
i0(11,10,10) -> 11*
i0(5,4,9) -> 11*
i0(5,9,4) -> 11*
i0(9,5,3) -> 11*
i0(2,4,8) -> 11*
i0(6,10,10) -> 11*
i0(12,6,8) -> 11*
i0(10,6,9) -> 11*
i0(9,1,12) -> 11*
i0(10,11,4) -> 11*
i0(4,5,3) -> 11*
i0(10,1,1) -> 11*
i0(1,10,10) -> 11*
i0(7,6,8) -> 11*
i0(8,1,2) -> 11*
i0(11,12,10) -> 11*
i0(5,6,9) -> 11*
i0(11,2,7) -> 11*
i0(4,1,12) -> 11*
i0(5,11,4) -> 11*
i0(5,1,1) -> 11*
i0(9,7,3) -> 11*
i0(2,6,8) -> 11*
i0(3,1,2) -> 11*
i0(6,12,10) -> 11*
i0(12,8,8) -> 11*
i0(6,2,7) -> 11*
i0(10,8,9) -> 11*
i0(9,3,12) -> 11*
i0(4,7,3) -> 11*
i0(10,3,1) -> 11*
i0(1,12,10) -> 11*
i0(7,8,8) -> 11*
i0(8,3,2) -> 11*
i0(1,2,7) -> 11*
i0(5,8,9) -> 11*
i0(11,4,7) -> 11*
i0(4,3,12) -> 11*
i0(5,3,1) -> 11*
i0(9,9,3) -> 11*
i0(2,8,8) -> 11*
i0(3,3,2) -> 11*
i0(12,10,8) -> 11*
i0(6,4,7) -> 11*
i0(10,10,9) -> 11*
i0(9,5,12) -> 11*
i0(4,9,3) -> 11*
i0(10,5,1) -> 11*
i0(7,10,8) -> 11*
i0(8,5,2) -> 11*
i0(1,4,7) -> 11*
i0(5,10,9) -> 11*
i0(11,6,7) -> 11*
i0(4,5,12) -> 11*
i0(8,1,11) -> 11*
i0(5,5,1) -> 11*
i0(9,11,3) -> 11*
i0(2,10,8) -> 11*
i0(3,5,2) -> 11*
i0(12,12,8) -> 11*
i0(6,6,7) -> 11*
i0(10,12,9) -> 11*
i0(12,2,5) -> 11*
i0(9,7,12) -> 11*
i0(10,2,6) -> 11*
i0(3,1,11) -> 11*
i0(4,11,3) -> 11*
i0(10,7,1) -> 11*
i0(7,12,8) -> 11*
i0(8,7,2) -> 11*
i0(1,6,7) -> 11*
i0(5,12,9) -> 11*
i0(7,2,5) -> 11*
i0(11,8,7) -> 11*
i0(4,7,12) -> 11*
i0(5,2,6) -> 11*
i0(8,3,11) -> 11*
i0(5,7,1) -> 11*
i0(2,12,8) -> 11*
i0(3,7,2) -> 11*
i0(2,2,5) -> 11*
i0(6,8,7) -> 11*
i0(12,4,5) -> 11*
i0(9,9,12) -> 11*
i0(10,4,6) -> 11*
i0(3,3,11) -> 11*
i0(10,9,1) -> 11*
i0(8,9,2) -> 11*
i0(1,8,7) -> 11*
i0(7,4,5) -> 11*
i0(11,10,7) -> 11*
i0(4,9,12) -> 11*
i0(5,4,6) -> 11*
i0(8,5,11) -> 11*
i0(5,9,1) -> 11*
i0(12,1,10) -> 11*
i0(3,9,2) -> 11*
i0(2,4,5) -> 11*
i0(6,10,7) -> 11*
i0(12,6,5) -> 11*
i0(9,11,12) -> 11*
i0(10,6,6) -> 11*
i0(3,5,11) -> 11*
i0(7,1,10) -> 11*
i0(10,11,1) -> 11*
i0(8,11,2) -> 11*
i0(1,10,7) -> 11*
i0(7,6,5) -> 11*
i0(11,12,7) -> 11*
i0(4,11,12) -> 11*
i0(5,6,6) -> 11*
i0(11,2,4) -> 11*
i0(8,7,11) -> 11*
i0(2,1,10) -> 11*
i0(5,11,1) -> 11*
i0(12,3,10) -> 11*
i0(3,11,2) -> 11*
i0(2,6,5) -> 11*
i0(6,12,7) -> 11*
i0(12,8,5) -> 11*
i0(6,2,4) -> 11*
i0(10,8,6) -> 11*
i0(3,7,11) -> 11*
i0(7,3,10) -> 11*
i0(1,12,7) -> 11*
i0(7,8,5) -> 11*
i0(1,2,4) -> 11*
i0(5,8,6) -> 11*
i0(11,4,4) -> 11*
i0(8,9,11) -> 11*
i0(2,3,10) -> 11*
i0(12,5,10) -> 11*
i0(2,8,5) -> 11*
i0(12,10,5) -> 11*
i0(6,4,4) -> 11*
i0(10,10,6) -> 11*
i0(3,9,11) -> 11*
i0(7,5,10) -> 11*
i0(11,1,9) -> 11*
i0(7,10,5) -> 11*
i0(1,4,4) -> 11*
i0(5,10,6) -> 11*
i0(11,6,4) -> 11*
i0(8,11,11) -> 11*
i0(2,5,10) -> 11*
i0(8,1,8) -> 11*
i0(12,7,10) -> 11*
i0(6,1,9) -> 11*
i0(2,10,5) -> 11*
i0(12,12,5) -> 11*
i0(6,6,4) -> 11*
i0(10,12,6) -> 11*
i0(3,11,11) -> 11*
i0(10,2,3) -> 11*
i0(3,1,8) -> 11*
i0(7,7,10) -> 11*
i0(1,1,9) -> 11*
i0(11,3,9) -> 11*
i0(7,12,5) -> 11*
i0(1,6,4) -> 11*
i0(5,12,6) -> 11*
i0(11,8,4) -> 11*
i0(5,2,3) -> 11*
i0(2,7,10) -> 11*
i0(8,3,8) -> 11*
i0(12,9,10) -> 11*
i0(6,3,9) -> 11*
i0(2,12,5) -> 11*
i0(6,8,4) -> 11*
i0(10,4,3) -> 11*
i0(3,3,8) -> 11*
i0(7,9,10) -> 11*
i0(1,3,9) -> 11*
i0(11,5,9) -> 11*
i0(1,8,4) -> 11*
i0(11,10,4) -> 11*
i0(5,4,3) -> 11*
i0(2,9,10) -> 11*
i0(8,5,8) -> 11*
i0(12,11,10) -> 11*
i0(6,5,9) -> 11*
i0(12,1,7) -> 11*
i0(6,10,4) -> 11*
i0(10,6,3) -> 11*
i0(3,5,8) -> 11*
i0(7,11,10) -> 11*
i0(1,5,9) -> 11*
i0(7,1,7) -> 11*
i0(11,7,9) -> 11*
i0(10,2,12) -> 11*
i0(1,10,4) -> 11*
i0(11,12,4) -> 11*
i0(5,6,3) -> 11*
i0(11,2,1) -> 11*
i0(2,11,10) -> 11*
i0(8,7,8) -> 11*
i0(9,2,2) -> 11*
i0(2,1,7) -> 11*
i0(6,7,9) -> 11*
i0(12,3,7) -> 11*
i0(5,2,12) -> 11*
i0(6,12,4) -> 11*
i0(6,2,1) -> 11*
i0(10,8,3) -> 11*
i0(3,7,8) -> 11*
i0(4,2,2) -> 11*
i0(1,7,9) -> 11*
i0(7,3,7) -> 11*
i0(11,9,9) -> 11*
i0(10,4,12) -> 11*
i0(1,12,4) -> 11*
i0(1,2,1) -> 11*
i0(5,8,3) -> 11*
i0(11,4,1) -> 11*
i0(8,9,8) -> 11*
i0(9,4,2) -> 11*
i0(2,3,7) -> 11*
i0(6,9,9) -> 11*
i0(12,5,7) -> 11*
i0(5,4,12) -> 11*
i0(6,4,1) -> 11*
i0(10,10,3) -> 11*
i0(3,9,8) -> 11*
i0(4,4,2) -> 11*
i0(1,9,9) -> 11*
i0(7,5,7) -> 11*
i0(11,11,9) -> 11*
i0(10,6,12) -> 11*
i0(11,1,6) -> 11*
i0(1,4,1) -> 11*
i0(5,10,3) -> 11*
i0(11,6,1) -> 11*
i0(8,11,8) -> 11*
i0(9,6,2) -> 11*
i0(2,5,7) -> 11*
i0(6,11,9) -> 11*
i0(8,1,5) -> 11*
i0(12,7,7) -> 11*
i0(5,6,12) -> 11*
i0(6,1,6) -> 11*
i0(9,2,11) -> 11*
i0(6,6,1) -> 11*
i0(10,12,3) -> 11*
i0(3,11,8) -> 11*
i0(4,6,2) -> 11*
i0(1,11,9) -> 11*
i0(3,1,5) -> 11*
i0(7,7,7) -> 11*
i0(1,1,6) -> 11*
i0(10,8,12) -> 11*
i0(11,3,6) -> 11*
i0(4,2,11) -> 11*
i0(1,6,1) -> 11*
i0(5,12,3) -> 11*
i0(11,8,1) -> 11*
i0(9,8,2) -> 11*
i0(2,7,7) -> 11*
i0(8,3,5) -> 11*
i0(12,9,7) -> 11*
i0(5,8,12) -> 11*
i0(6,3,6) -> 11*
i0(9,4,11) -> 11*
i0(6,8,1) -> 11*
i0(4,8,2) -> 11*
i0(3,3,5) -> 11*
i0(7,9,7) -> 11*
i0(1,3,6) -> 11*
i0(10,10,12) -> 11*
i0(11,5,6) -> 11*
i0(4,4,11) -> 11*
i0(1,8,1) -> 11*
i0(11,10,1) -> 11*
i0(9,10,2) -> 11*
i0(2,9,7) -> 11*
i0(8,5,5) -> 11*
i0(12,11,7) -> 11*
i0(5,10,12) -> 11*
i0(6,5,6) -> 11*
i0(12,1,4) -> 11*
i0(9,6,11) -> 11*
i0(6,10,1) -> 11*
i0(4,10,2) -> 11*
i0(3,5,5) -> 11*
i0(7,11,7) -> 11*
i0(1,5,6) -> 11*
i0(7,1,4) -> 11*
i0(10,12,12) -> 11*
i0(11,7,6) -> 11*
i0(4,6,11) -> 11*
i0(1,10,1) -> 11*
i0(8,2,10) -> 11*
i0(11,12,1) -> 11*
i0(9,12,2) -> 11*
i0(2,11,7) -> 11*
i0(8,7,5) -> 11*
i0(2,1,4) -> 11*
i0(5,12,12) -> 11*
i0(6,7,6) -> 11*
i0(12,3,4) -> 11*
i0(9,8,11) -> 11*
i0(3,2,10) -> 11*
i0(6,12,1) -> 11*
i0(4,12,2) -> 11*
i0(3,7,5) -> 11*
i0(1,7,6) -> 11*
i0(7,3,4) -> 11*
i0(11,9,6) -> 11*
i0(4,8,11) -> 11*
i0(1,12,1) -> 11*
i0(8,4,10) -> 11*
i0(8,9,5) -> 11*
i0(2,3,4) -> 11*
i0(6,9,6) -> 11*
i0(12,5,4) -> 11*
i0(9,10,11) -> 11*
i0(3,4,10) -> 11*
i0(3,9,5) -> 11*
i0(1,9,6) -> 11*
i0(7,5,4) -> 11*
i0(11,11,6) -> 11*
i0(4,10,11) -> 11*
i0(11,1,3) -> 11*
i0(8,6,10) -> 11*
i0(12,2,9) -> 11*
i0(8,11,5) -> 11*
i0(2,5,4) -> 11*
i0(6,11,6) -> 11*
i0(12,7,4) -> 11*
i0(6,1,3) -> 11*
i0(9,12,11) -> 11*
i0(3,6,10) -> 11*
i0(9,2,8) -> 11*
i0(7,2,9) -> 11*
i0(3,11,5) -> 11*
i0(1,11,6) -> 11*
i0(7,7,4) -> 11*
i0(1,1,3) -> 11*
i0(4,12,11) -> 11*
i0(11,3,3) -> 11*
i0(4,2,8) -> 11*
i0(8,8,10) -> 11*
i0(2,2,9) -> 11*
i0(12,4,9) -> 11*
i0(2,7,4) -> 11*
i0(12,9,4) -> 11*
i0(6,3,3) -> 11*
i0(3,8,10) -> 11*
i0(9,4,8) -> 11*
i0(7,4,9) -> 11*
i0(7,9,4) -> 11*
i0(1,3,3) -> 11*
i0(11,5,3) -> 11*
i0(4,4,8) -> 11*
i0(8,10,10) -> 11*
i0(2,4,9) -> 11*
i0(12,6,9) -> 11*
i0(11,1,12) -> 11*
i0(2,9,4) -> 11*
i0(12,11,4) -> 11*
i0(6,5,3) -> 11*
i0(12,1,1) -> 11*
i0(3,10,10) -> 11*
i0(9,6,8) -> 11*
i0(10,1,2) -> 11*
i0(7,6,9) -> 11*
i0(6,1,12) -> 11*
i0(7,11,4) -> 11*
i0(1,5,3) -> 11*
i0(7,1,1) -> 11*
i0(11,7,3) -> 11*
i0(4,6,8) -> 11*
i0(5,1,2) -> 11*
i0(8,12,10) -> 11*
i0(2,6,9) -> 11*
i0(8,2,7) -> 11*
i0(12,8,9) -> 11*
i0(1,1,12) -> 11*
i0(11,3,12) -> 11*
i0(2,11,4) -> 11*
i0(2,1,1) -> 11*
i0(6,7,3) -> 11*
i0(12,3,1) -> 11*
i0(3,12,10) -> 11*
i0(9,8,8) -> 11*
i0(10,3,2) -> 11*
i0(3,2,7) -> 11*
i0(7,8,9) -> 11*
i0(6,3,12) -> 11*
i0(1,7,3) -> 11*
i0(7,3,1) -> 11*
i0(11,9,3) -> 11*
i0(4,8,8) -> 11*
i0(5,3,2) -> 11*
i0(2,8,9) -> 11*
i0(8,4,7) -> 11*
i0(12,10,9) -> 11*
i0(1,3,12) -> 11*
i0(11,5,12) -> 11*
i0(2,3,1) -> 11*
i0(6,9,3) -> 11*
i0(12,5,1) -> 11*
i0(9,10,8) -> 11*
i0(10,5,2) -> 11*
i0(3,4,7) -> 11*
i0(7,10,9) -> 11*
i0(6,5,12) -> 11*
i0(10,1,11) -> 11*
i0(1,9,3) -> 11*
i0(7,5,1) -> 11*
i0(11,11,3) -> 11*
i0(4,10,8) -> 11*
i0(5,5,2) -> 11*
i0(2,10,9) -> 11*
i0(8,6,7) -> 11*
i0(12,12,9) -> 11*
i0(1,5,12) -> 11*
i0(11,7,12) -> 11*
i0(12,2,6) -> 11*
i0(5,1,11) -> 11*
i0(2,5,1) -> 11*
i0(6,11,3) -> 11*
i0(12,7,1) -> 11*
i0(9,12,8) -> 11*
i0(10,7,2) -> 11*
i0(3,6,7) -> 11*
i0(7,12,9) -> 11*
i0(9,2,5) -> 11*
i0(6,7,12) -> 11*
i0(7,2,6) -> 11*
i0(10,3,11) -> 11*
i0(1,11,3) -> 11*
i0(7,7,1) -> 11*
i0(4,12,8) -> 11*
i0(5,7,2) -> 11*
i0(2,12,9) -> 11*
i0(4,2,5) -> 11*
i0(8,8,7) -> 11*
i0(1,7,12) -> 11*
i0(2,2,6) -> 11*
i0(11,9,12) -> 11*
i0(12,4,6) -> 11*
i0(5,3,11) -> 11*
i0(2,7,1) -> 11*
i0(12,9,1) -> 11*
i0(10,9,2) -> 11*
i0(3,8,7) -> 11*
i0(9,4,5) -> 11*
i0(6,9,12) -> 11*
i0(7,4,6) -> 11*
i0(10,5,11) -> 11*
i0(7,9,1) -> 11*
i0(5,9,2) -> 11*
i0(4,4,5) -> 11*
i0(8,10,7) -> 11*
i0(1,9,12) -> 11*
i0(2,4,6) -> 11*
i0(11,11,12) -> 11*
i0(12,6,6) -> 11*
i0(5,5,11) -> 11*
i0(2,9,1) -> 11*
i0(9,1,10) -> 11*
i0(12,11,1) -> 11*
i0(10,11,2) -> 11*
i0(3,10,7) -> 11*
i0(9,6,5) -> 11*
i0(6,11,12) -> 11*
i0(7,6,6) -> 11*
i0(10,7,11) -> 11*
i0(4,1,10) -> 11*
i0(7,11,1) -> 11*
i0(5,11,2) -> 11*
i0(4,6,5) -> 11*
i0(8,12,7) -> 11*
i0(1,11,12) -> 11*
i0(2,6,6) -> 11*
i0(8,2,4) -> 11*
i0(12,8,6) -> 11*
i0(5,7,11) -> 11*
i0(2,11,1) -> 11*
i0(9,3,10) -> 11*
i0(3,12,7) -> 11*
i0(9,8,5) -> 11*
i0(3,2,4) -> 11*
i0(7,8,6) -> 11*
i0(10,9,11) -> 11*
i0(4,3,10) -> 11*
i0(4,8,5) -> 11*
i0(2,8,6) -> 11*
i0(8,4,4) -> 11*
i0(12,10,6) -> 11*
i0(5,9,11) -> 11*
i0(9,5,10) -> 11*
i0(9,10,5) -> 11*
i0(3,4,4) -> 11*
i0(7,10,6) -> 11*
i0(10,11,11) -> 11*
i0(4,5,10) -> 11*
i0(10,1,8) -> 11*
i0(8,1,9) -> 11*
i0(4,10,5) -> 11*
i0(2,10,6) -> 11*
i0(8,6,4) -> 11*
i0(12,12,6) -> 11*
i0(5,11,11) -> 11*
i0(12,2,3) -> 11*
i0(5,1,8) -> 11*
i0(9,7,10) -> 11*
i0(3,1,9) -> 11*
i0(9,12,5) -> 11*
i0(3,6,4) -> 11*
i0(7,12,6) -> 11*
i0(7,2,3) -> 11*
i0(4,7,10) -> 11*
i0(10,3,8) -> 11*
i0(8,3,9) -> 11*
i0(4,12,5) -> 11*
i0(2,12,6) -> 11*
i0(8,8,4) -> 11*
i0(2,2,3) -> 11*
i0(12,4,3) -> 11*
i0(5,3,8) -> 11*
i0(9,9,10) -> 11*
i0(3,3,9) -> 11*
i0(3,8,4) -> 11*
i0(7,4,3) -> 11*
i0(4,9,10) -> 11*
i0(10,5,8) -> 11*
i0(8,5,9) -> 11*
i0(8,10,4) -> 11*
i0(2,4,3) -> 11*
i0(12,6,3) -> 11*
i0(5,5,8) -> 11*
i0(9,11,10) -> 11*
i0(3,5,9) -> 11*
i0(9,1,7) -> 11*
i0(12,2,12) -> 11*
i0(3,10,4) -> 11*
i0(7,6,3) -> 11*
i0(4,11,10) -> 11*
i0(10,7,8) -> 11*
i0(11,2,2) -> 11*
i0(4,1,7) -> 11*
i0(8,7,9) -> 11*
i0(7,2,12) -> 11*
i0(8,12,4) -> 11*
i0(2,6,3) -> 11*
i0(8,2,1) -> 11*
i0(12,8,3) -> 11*
i0(5,7,8) -> 11*
i0(6,2,2) -> 11*
i0(3,7,9) -> 11*
i0(9,3,7) -> 11*
i0(2,2,12) -> 11*
i0(12,4,12) -> 11*
i0(3,12,4) -> 11*
i0(3,2,1) -> 11*
i0(7,8,3) -> 11*
i0(1,2,2) -> 11*
i0(10,9,8) -> 11*
i0(11,4,2) -> 11*
i0(4,3,7) -> 11*
i0(8,9,9) -> 11*
i0(7,4,12) -> 11*
i0(2,8,3) -> 11*
i0(8,4,1) -> 11*
i0(12,10,3) -> 11*
i0(5,9,8) -> 11*
i0(6,4,2) -> 11*
i0(3,9,9) -> 11*
i0(9,5,7) -> 11*
i0(2,4,12) -> 11*
i0(12,6,12) -> 11*
i0(3,4,1) -> 11*
i0(7,10,3) -> 11*
i0(1,4,2) -> 11*
i0(10,11,8) -> 11*
i0(11,6,2) -> 11*
i0(4,5,7) -> 11*
i0(8,11,9) -> 11*
i0(10,1,5) -> 11*
i0(7,6,12) -> 11*
i0(8,1,6) -> 11*
i0(11,2,11) -> 11*
i0(2,10,3) -> 11*
i0(8,6,1) -> 11*
i0(12,12,3) -> 11*
i0(5,11,8) -> 11*
i0(6,6,2) -> 11*
i0(3,11,9) -> 11*
i0(5,1,5) -> 11*
i0(9,7,7) -> 11*
i0(2,6,12) -> 11*
i0(3,1,6) -> 11*
i0(12,8,12) -> 11*
i0(6,2,11) -> 11*
i0(3,6,1) -> 11*
i0(7,12,3) -> 11*
i0(1,6,2) -> 11*
i0(11,8,2) -> 11*
i0(4,7,7) -> 11*
i0(10,3,5) -> 11*
i0(7,8,12) -> 11*
i0(8,3,6) -> 11*
i0(1,2,11) -> 11*
i0(11,4,11) -> 11*
i0(2,12,3) -> 11*
i0(8,8,1) -> 11*
i0(6,8,2) -> 11*
i0(5,3,5) -> 11*
i0(9,9,7) -> 11*
i0(2,8,12) -> 11*
i0(3,3,6) -> 11*
i0(12,10,12) -> 11*
i0(6,4,11) -> 11*
i0(3,8,1) -> 11*
i0(1,8,2) -> 11*
i0(11,10,2) -> 11*
i0(4,9,7) -> 11*
i0(10,5,5) -> 11*
i0(7,10,12) -> 11*
i0(8,5,6) -> 11*
i0(1,4,11) -> 11*
i0(11,6,11) -> 11*
i0(8,10,1) -> 11*
i0(6,10,2) -> 11*
i0(5,5,5) -> 11*
i0(9,11,7) -> 11*
i0(2,10,12) -> 11*
i0(3,5,6) -> 11*
i0(9,1,4) -> 11*
i0(12,12,12) -> 11*
i0(6,6,11) -> 11*
i0(3,10,1) -> 11*
i0(10,2,10) -> 11*
i0(1,10,2) -> 11*
i0(11,12,2) -> 11*
i0(4,11,7) -> 11*
i0(10,7,5) -> 11*
i0(4,1,4) -> 11*
i0(7,12,12) -> 11*
i0(8,7,6) -> 11*
i0(1,6,11) -> 11*
i0(11,8,11) -> 11*
i0(5,2,10) -> 11*
i0(8,12,1) -> 11*
i0(6,12,2) -> 11*
i0(5,7,5) -> 11*
i0(2,12,12) -> 11*
i0(3,7,6) -> 11*
i0(9,3,4) -> 11*
i0(6,8,11) -> 11*
i0(3,12,1) -> 11*
i0(10,4,10) -> 11*
i0(1,12,2) -> 11*
i0(10,9,5) -> 11*
i0(4,3,4) -> 11*
i0(8,9,6) -> 11*
i0(1,8,11) -> 11*
i0(11,10,11) -> 11*
i0(5,4,10) -> 11*
i0(5,9,5) -> 11*
i0(3,9,6) -> 11*
i0(9,5,4) -> 11*
i0(6,10,11) -> 11*
i0(10,6,10) -> 11*
i0(10,11,5) -> 11*
i0(4,5,4) -> 11*
i0(8,11,6) -> 11*
i0(1,10,11) -> 11*
i0(8,1,3) -> 11*
i0(11,12,11) -> 11*
i0(5,6,10) -> 11*
i0(11,2,8) -> 11*
i0(9,2,9) -> 11*
i0(5,11,5) -> 11*
i0(3,11,6) -> 11*
i0(9,7,4) -> 11*
i0(3,1,3) -> 11*
i0(6,12,11) -> 11*
i0(6,2,8) -> 11*
i0(10,8,10) -> 11*
i0(4,2,9) -> 11*
i0(4,7,4) -> 11*
i0(1,12,11) -> 11*
i0(8,3,3) -> 11*
i0(1,2,8) -> 11*
i0(5,8,10) -> 11*
i0(11,4,8) -> 11*
i0(9,4,9) -> 11*
i0(9,9,4) -> 11*
i0(3,3,3) -> 11*
i0(6,4,8) -> 11*
i0(10,10,10) -> 11*
i0(4,4,9) -> 11*
i0(4,9,4) -> 11*
i0(8,5,3) -> 11*
i0(1,4,8) -> 11*
i0(5,10,10) -> 11*
i0(11,6,8) -> 11*
i0(12,1,2) -> 11*
i0(9,6,9) -> 11*
i0(8,1,12) -> 11*
i0(9,11,4) -> 11*
i0(3,5,3) -> 11*
i0(9,1,1) -> 11*
i0(6,6,8) -> 11*
i0(7,1,2) -> 11*
i0(10,12,10) -> 11*
i0(4,6,9) -> 11*
i0(10,2,7) -> 11*
i0(3,1,12) -> 11*
i0(4,11,4) -> 11*
i0(4,1,1) -> 11*
i0(8,7,3) -> 11*
i0(1,6,8) -> 11*
i0(2,1,2) -> 11*
i0(5,12,10) -> 11*
i0(11,8,8) -> 11*
i0(12,3,2) -> 11*
i0(5,2,7) -> 11*
i0(9,8,9) -> 11*
i0(8,3,12) -> 11*
i0(3,7,3) -> 11*
i0(9,3,1) -> 11*
i0(6,8,8) -> 11*
i0(7,3,2) -> 11*
i0(4,8,9) -> 11*
i0(10,4,7) -> 11*
i0(3,3,12) -> 11*
i0(4,3,1) -> 11*
i0(8,9,3) -> 11*
i0(1,8,8) -> 11*
i0(2,3,2) -> 11*
i0(11,10,8) -> 11*
i0(12,5,2) -> 11*
i0(5,4,7) -> 11*
i0(9,10,9) -> 11*
i0(8,5,12) -> 11*
i0(12,1,11) -> 11*
i0(3,9,3) -> 11*
i0(9,5,1) -> 11*
i0(6,10,8) -> 11*
i0(7,5,2) -> 11*
i0(4,10,9) -> 11*
i0(10,6,7) -> 11*
i0(3,5,12) -> 11*
i0(7,1,11) -> 11*
i0(4,5,1) -> 11*
i0(8,11,3) -> 11*
i0(1,10,8) -> 11*
i0(2,5,2) -> 11*
i0(11,12,8) -> 11*
i0(12,7,2) -> 11*
i0(5,6,7) -> 11*
i0(9,12,9) -> 11*
i0(11,2,5) -> 11*
i0(8,7,12) -> 11*
i0(9,2,6) -> 11*
i0(2,1,11) -> 11*
i0(12,3,11) -> 11*
i0(3,11,3) -> 11*
i0(9,7,1) -> 11*
i0(6,12,8) -> 11*
i0(7,7,2) -> 11*
i0(4,12,9) -> 11*
i0(6,2,5) -> 11*
i0(10,8,7) -> 11*
i0(3,7,12) -> 11*
i0(4,2,6) -> 11*
i0(7,3,11) -> 11*
i0(4,7,1) -> 11*
i0(1,12,8) -> 11*
i0(2,7,2) -> 11*
i0(12,9,2) -> 11*
i0(1,2,5) -> 11*
i0(5,8,7) -> 11*
i0(11,4,5) -> 11*
i0(8,9,12) -> 11*
i0(9,4,6) -> 11*
i0(2,3,11) -> 11*
i0(12,5,11) -> 11*
i0(9,9,1) -> 11*
i0(7,9,2) -> 11*
i0(6,4,5) -> 11*
i0(10,10,7) -> 11*
i0(3,9,12) -> 11*
i0(4,4,6) -> 11*
i0(7,5,11) -> 11*
i0(4,9,1) -> 11*
i0(11,1,10) -> 11*
i0(2,9,2) -> 11*
i0(12,11,2) -> 11*
i0(1,4,5) -> 11*
i0(5,10,7) -> 11*
i0(11,6,5) -> 11*
i0(8,11,12) -> 11*
i0(9,6,6) -> 11*
i0(2,5,11) -> 11*
i0(12,7,11) -> 11*
i0(6,1,10) -> 11*
i0(9,11,1) -> 11*
i0(7,11,2) -> 11*
i0(6,6,5) -> 11*
i0(10,12,7) -> 11*
i0(3,11,12) -> 11*
i0(4,6,6) -> 11*
i0(10,2,4) -> 11*
i0(7,7,11) -> 11*
i0(1,1,10) -> 11*
i0(4,11,1) -> 11*
i0(11,3,10) -> 11*
i0(2,11,2) -> 11*
i0(1,6,5) -> 11*
i0(5,12,7) -> 11*
i0(11,8,5) -> 11*
i0(5,2,4) -> 11*
i0(9,8,6) -> 11*
i0(2,7,11) -> 11*
i0(12,9,11) -> 11*
i0(6,3,10) -> 11*
i0(6,8,5) -> 11*
i0(4,8,6) -> 11*
i0(10,4,4) -> 11*
i0(7,9,11) -> 11*
i0(1,3,10) -> 11*
i0(11,5,10) -> 11*
i0(1,8,5) -> 11*
i0(11,10,5) -> 11*
i0(5,4,4) -> 11*
i0(9,10,6) -> 11*
i0(2,9,11) -> 11*
i0(12,11,11) -> 11*
i0(6,5,10) -> 11*
i0(12,1,8) -> 11*
i0(10,1,9) -> 11*
i0(6,10,5) -> 11*
i0(4,10,6) -> 11*
i0(10,6,4) -> 11*
i0(7,11,11) -> 11*
i0(1,5,10) -> 11*
i0(7,1,8) -> 11*
i0(11,7,10) -> 11*
i0(5,1,9) -> 11*
i0(1,10,5) -> 11*
i0(11,12,5) -> 11*
i0(5,6,4) -> 11*
i0(9,12,6) -> 11*
i0(2,11,11) -> 11*
i0(9,2,3) -> 11*
i0(2,1,8) -> 11*
i0(6,7,10) -> 11*
i0(12,3,8) -> 11*
i0(10,3,9) -> 11*
i0(6,12,5) -> 11*
i0(4,12,6) -> 11*
i0(10,8,4) -> 11*
i0(4,2,3) -> 11*
i0(1,7,10) -> 11*
i0(7,3,8) -> 11*
i0(11,9,10) -> 11*
i0(5,3,9) -> 11*
i0(1,12,5) -> 11*
i0(5,8,4) -> 11*
i0(9,4,3) -> 11*
i0(2,3,8) -> 11*
i0(6,9,10) -> 11*
i0(12,5,8) -> 11*
i0(10,5,9) -> 11*
i0(10,10,4) -> 11*
i0(4,4,3) -> 11*
i0(1,9,10) -> 11*
i0(7,5,8) -> 11*
i0(11,11,10) -> 11*
i0(5,5,9) -> 11*
i0(11,1,7) -> 11*
i0(5,10,4) -> 11*
i0(9,6,3) -> 11*
i0(2,5,8) -> 11*
i0(6,11,10) -> 11*
i0(12,7,8) -> 11*
i0(6,1,7) -> 11*
i0(10,7,9) -> 11*
i0(9,2,12) -> 11*
i0(10,12,4) -> 11*
i0(4,6,3) -> 11*
i0(10,2,1) -> 11*
i0(1,11,10) -> 11*
i0(7,7,8) -> 11*
i0(8,2,2) -> 11*
i0(1,1,7) -> 11*
i0(5,7,9) -> 11*
i0(11,3,7) -> 11*
i0(4,2,12) -> 11*
i0(5,12,4) -> 11*
a0() -> 10*
b0() -> 9*
b'0() -> 8*
c0() -> 7*
d0() -> 6*
if0(10,12,4) -> 5*
if0(4,6,3) -> 5*
if0(10,2,1) -> 5*
if0(1,11,10) -> 5*
if0(7,7,8) -> 5*
if0(8,2,2) -> 5*
if0(1,1,7) -> 5*
if0(5,7,9) -> 5*
if0(11,3,7) -> 5*
if0(4,2,12) -> 5*
if0(5,12,4) -> 5*
if0(5,2,1) -> 5*
if0(9,8,3) -> 5*
if0(2,7,8) -> 5*
if0(3,2,2) -> 5*
if0(12,9,8) -> 5*
if0(6,3,7) -> 5*
if0(10,9,9) -> 5*
if0(9,4,12) -> 5*
if0(4,8,3) -> 5*
if0(10,4,1) -> 5*
if0(7,9,8) -> 5*
if0(8,4,2) -> 5*
if0(1,3,7) -> 5*
if0(5,9,9) -> 5*
if0(11,5,7) -> 5*
if0(4,4,12) -> 5*
if0(5,4,1) -> 5*
if0(9,10,3) -> 5*
if0(2,9,8) -> 5*
if0(3,4,2) -> 5*
if0(12,11,8) -> 5*
if0(6,5,7) -> 5*
if0(10,11,9) -> 5*
if0(12,1,5) -> 5*
if0(9,6,12) -> 5*
if0(10,1,6) -> 5*
if0(4,10,3) -> 5*
if0(10,6,1) -> 5*
if0(7,11,8) -> 5*
if0(8,6,2) -> 5*
if0(1,5,7) -> 5*
if0(5,11,9) -> 5*
if0(7,1,5) -> 5*
if0(11,7,7) -> 5*
if0(4,6,12) -> 5*
if0(5,1,6) -> 5*
if0(8,2,11) -> 5*
if0(5,6,1) -> 5*
if0(9,12,3) -> 5*
if0(2,11,8) -> 5*
if0(3,6,2) -> 5*
if0(2,1,5) -> 5*
if0(6,7,7) -> 5*
if0(12,3,5) -> 5*
if0(9,8,12) -> 5*
if0(10,3,6) -> 5*
if0(3,2,11) -> 5*
if0(4,12,3) -> 5*
if0(10,8,1) -> 5*
if0(8,8,2) -> 5*
if0(1,7,7) -> 5*
if0(7,3,5) -> 5*
if0(11,9,7) -> 5*
if0(4,8,12) -> 5*
if0(5,3,6) -> 5*
if0(8,4,11) -> 5*
if0(5,8,1) -> 5*
if0(3,8,2) -> 5*
if0(2,3,5) -> 5*
if0(6,9,7) -> 5*
if0(12,5,5) -> 5*
if0(9,10,12) -> 5*
if0(10,5,6) -> 5*
if0(3,4,11) -> 5*
if0(10,10,1) -> 5*
if0(8,10,2) -> 5*
if0(1,9,7) -> 5*
if0(7,5,5) -> 5*
if0(11,11,7) -> 5*
if0(4,10,12) -> 5*
if0(5,5,6) -> 5*
if0(11,1,4) -> 5*
if0(8,6,11) -> 5*
if0(5,10,1) -> 5*
if0(12,2,10) -> 5*
if0(3,10,2) -> 5*
if0(2,5,5) -> 5*
if0(6,11,7) -> 5*
if0(12,7,5) -> 5*
if0(6,1,4) -> 5*
if0(9,12,12) -> 5*
if0(10,7,6) -> 5*
if0(3,6,11) -> 5*
if0(7,2,10) -> 5*
if0(10,12,1) -> 5*
if0(8,12,2) -> 5*
if0(1,11,7) -> 5*
if0(7,7,5) -> 5*
if0(1,1,4) -> 5*
if0(4,12,12) -> 5*
if0(5,7,6) -> 5*
if0(11,3,4) -> 5*
if0(8,8,11) -> 5*
if0(2,2,10) -> 5*
if0(5,12,1) -> 5*
if0(12,4,10) -> 5*
if0(3,12,2) -> 5*
if0(2,7,5) -> 5*
if0(12,9,5) -> 5*
if0(6,3,4) -> 5*
if0(10,9,6) -> 5*
if0(3,8,11) -> 5*
if0(7,4,10) -> 5*
if0(7,9,5) -> 5*
if0(1,3,4) -> 5*
if0(5,9,6) -> 5*
if0(11,5,4) -> 5*
if0(8,10,11) -> 5*
if0(2,4,10) -> 5*
if0(12,6,10) -> 5*
if0(2,9,5) -> 5*
if0(12,11,5) -> 5*
if0(6,5,4) -> 5*
if0(10,11,6) -> 5*
if0(3,10,11) -> 5*
if0(10,1,3) -> 5*
if0(7,6,10) -> 5*
if0(11,2,9) -> 5*
if0(7,11,5) -> 5*
if0(1,5,4) -> 5*
if0(5,11,6) -> 5*
if0(11,7,4) -> 5*
if0(5,1,3) -> 5*
if0(8,12,11) -> 5*
if0(2,6,10) -> 5*
if0(8,2,8) -> 5*
if0(12,8,10) -> 5*
if0(6,2,9) -> 5*
if0(2,11,5) -> 5*
if0(6,7,4) -> 5*
if0(3,12,11) -> 5*
if0(10,3,3) -> 5*
if0(3,2,8) -> 5*
if0(7,8,10) -> 5*
if0(1,2,9) -> 5*
if0(11,4,9) -> 5*
if0(1,7,4) -> 5*
if0(11,9,4) -> 5*
if0(5,3,3) -> 5*
if0(2,8,10) -> 5*
if0(8,4,8) -> 5*
if0(12,10,10) -> 5*
if0(6,4,9) -> 5*
if0(6,9,4) -> 5*
if0(10,5,3) -> 5*
if0(3,4,8) -> 5*
if0(7,10,10) -> 5*
if0(1,4,9) -> 5*
if0(11,6,9) -> 5*
if0(10,1,12) -> 5*
if0(1,9,4) -> 5*
if0(11,11,4) -> 5*
if0(5,5,3) -> 5*
if0(11,1,1) -> 5*
if0(2,10,10) -> 5*
if0(8,6,8) -> 5*
if0(9,1,2) -> 5*
if0(12,12,10) -> 5*
if0(6,6,9) -> 5*
if0(12,2,7) -> 5*
if0(5,1,12) -> 5*
if0(6,11,4) -> 5*
if0(6,1,1) -> 5*
if0(10,7,3) -> 5*
if0(3,6,8) -> 5*
if0(4,1,2) -> 5*
if0(7,12,10) -> 5*
if0(1,6,9) -> 5*
if0(7,2,7) -> 5*
if0(11,8,9) -> 5*
if0(10,3,12) -> 5*
if0(1,11,4) -> 5*
if0(1,1,1) -> 5*
if0(5,7,3) -> 5*
if0(11,3,1) -> 5*
if0(2,12,10) -> 5*
if0(8,8,8) -> 5*
if0(9,3,2) -> 5*
if0(2,2,7) -> 5*
if0(6,8,9) -> 5*
if0(12,4,7) -> 5*
if0(5,3,12) -> 5*
if0(6,3,1) -> 5*
if0(10,9,3) -> 5*
if0(3,8,8) -> 5*
if0(4,3,2) -> 5*
if0(1,8,9) -> 5*
if0(7,4,7) -> 5*
if0(11,10,9) -> 5*
if0(10,5,12) -> 5*
if0(1,3,1) -> 5*
if0(5,9,3) -> 5*
if0(11,5,1) -> 5*
if0(8,10,8) -> 5*
if0(9,5,2) -> 5*
if0(2,4,7) -> 5*
if0(6,10,9) -> 5*
if0(12,6,7) -> 5*
if0(5,5,12) -> 5*
if0(9,1,11) -> 5*
if0(6,5,1) -> 5*
if0(10,11,3) -> 5*
if0(3,10,8) -> 5*
if0(4,5,2) -> 5*
if0(1,10,9) -> 5*
if0(7,6,7) -> 5*
if0(11,12,9) -> 5*
if0(10,7,12) -> 5*
if0(11,2,6) -> 5*
if0(4,1,11) -> 5*
if0(1,5,1) -> 5*
if0(5,11,3) -> 5*
if0(11,7,1) -> 5*
if0(8,12,8) -> 5*
if0(9,7,2) -> 5*
if0(2,6,7) -> 5*
if0(6,12,9) -> 5*
if0(8,2,5) -> 5*
if0(12,8,7) -> 5*
if0(5,7,12) -> 5*
if0(6,2,6) -> 5*
if0(9,3,11) -> 5*
if0(6,7,1) -> 5*
if0(3,12,8) -> 5*
if0(4,7,2) -> 5*
if0(1,12,9) -> 5*
if0(3,2,5) -> 5*
if0(7,8,7) -> 5*
if0(1,2,6) -> 5*
if0(10,9,12) -> 5*
if0(11,4,6) -> 5*
if0(4,3,11) -> 5*
if0(1,7,1) -> 5*
if0(11,9,1) -> 5*
if0(9,9,2) -> 5*
if0(2,8,7) -> 5*
if0(8,4,5) -> 5*
if0(12,10,7) -> 5*
if0(5,9,12) -> 5*
if0(6,4,6) -> 5*
if0(9,5,11) -> 5*
if0(6,9,1) -> 5*
if0(4,9,2) -> 5*
if0(3,4,5) -> 5*
if0(7,10,7) -> 5*
if0(1,4,6) -> 5*
if0(10,11,12) -> 5*
if0(11,6,6) -> 5*
if0(4,5,11) -> 5*
if0(1,9,1) -> 5*
if0(8,1,10) -> 5*
if0(11,11,1) -> 5*
if0(9,11,2) -> 5*
if0(2,10,7) -> 5*
if0(8,6,5) -> 5*
if0(12,12,7) -> 5*
if0(5,11,12) -> 5*
if0(6,6,6) -> 5*
if0(12,2,4) -> 5*
if0(9,7,11) -> 5*
if0(3,1,10) -> 5*
if0(6,11,1) -> 5*
if0(4,11,2) -> 5*
if0(3,6,5) -> 5*
if0(7,12,7) -> 5*
if0(1,6,6) -> 5*
if0(7,2,4) -> 5*
if0(11,8,6) -> 5*
if0(4,7,11) -> 5*
if0(1,11,1) -> 5*
if0(8,3,10) -> 5*
if0(2,12,7) -> 5*
if0(8,8,5) -> 5*
if0(2,2,4) -> 5*
if0(6,8,6) -> 5*
if0(12,4,4) -> 5*
if0(9,9,11) -> 5*
if0(3,3,10) -> 5*
if0(3,8,5) -> 5*
if0(1,8,6) -> 5*
if0(7,4,4) -> 5*
if0(11,10,6) -> 5*
if0(4,9,11) -> 5*
if0(8,5,10) -> 5*
if0(12,1,9) -> 5*
if0(8,10,5) -> 5*
if0(2,4,4) -> 5*
if0(6,10,6) -> 5*
if0(12,6,4) -> 5*
if0(9,11,11) -> 5*
if0(3,5,10) -> 5*
if0(9,1,8) -> 5*
if0(7,1,9) -> 5*
if0(3,10,5) -> 5*
if0(1,10,6) -> 5*
if0(7,6,4) -> 5*
if0(11,12,6) -> 5*
if0(4,11,11) -> 5*
if0(11,2,3) -> 5*
if0(4,1,8) -> 5*
if0(8,7,10) -> 5*
if0(2,1,9) -> 5*
if0(12,3,9) -> 5*
if0(8,12,5) -> 5*
if0(2,6,4) -> 5*
if0(6,12,6) -> 5*
if0(12,8,4) -> 5*
if0(6,2,3) -> 5*
if0(3,7,10) -> 5*
if0(9,3,8) -> 5*
if0(7,3,9) -> 5*
if0(3,12,5) -> 5*
if0(1,12,6) -> 5*
if0(7,8,4) -> 5*
if0(1,2,3) -> 5*
if0(11,4,3) -> 5*
if0(4,3,8) -> 5*
if0(8,9,10) -> 5*
if0(2,3,9) -> 5*
if0(12,5,9) -> 5*
if0(2,8,4) -> 5*
if0(12,10,4) -> 5*
if0(6,4,3) -> 5*
if0(3,9,10) -> 5*
if0(9,5,8) -> 5*
if0(7,5,9) -> 5*
if0(7,10,4) -> 5*
if0(1,4,3) -> 5*
if0(11,6,3) -> 5*
if0(4,5,8) -> 5*
if0(8,11,10) -> 5*
if0(2,5,9) -> 5*
if0(8,1,7) -> 5*
if0(12,7,9) -> 5*
if0(11,2,12) -> 5*
if0(2,10,4) -> 5*
if0(12,12,4) -> 5*
if0(6,6,3) -> 5*
if0(12,2,1) -> 5*
if0(3,11,10) -> 5*
if0(9,7,8) -> 5*
if0(10,2,2) -> 5*
if0(3,1,7) -> 5*
if0(7,7,9) -> 5*
if0(6,2,12) -> 5*
if0(7,12,4) -> 5*
if0(1,6,3) -> 5*
if0(7,2,1) -> 5*
if0(11,8,3) -> 5*
if0(4,7,8) -> 5*
if0(5,2,2) -> 5*
if0(2,7,9) -> 5*
if0(8,3,7) -> 5*
if0(12,9,9) -> 5*
if0(1,2,12) -> 5*
if0(11,4,12) -> 5*
if0(2,12,4) -> 5*
if0(2,2,1) -> 5*
if0(6,8,3) -> 5*
if0(12,4,1) -> 5*
if0(9,9,8) -> 5*
if0(10,4,2) -> 5*
if0(3,3,7) -> 5*
if0(7,9,9) -> 5*
if0(6,4,12) -> 5*
if0(1,8,3) -> 5*
if0(7,4,1) -> 5*
if0(11,10,3) -> 5*
if0(4,9,8) -> 5*
if0(5,4,2) -> 5*
if0(2,9,9) -> 5*
if0(8,5,7) -> 5*
if0(12,11,9) -> 5*
if0(1,4,12) -> 5*
if0(11,6,12) -> 5*
if0(12,1,6) -> 5*
if0(2,4,1) -> 5*
if0(6,10,3) -> 5*
if0(12,6,1) -> 5*
if0(9,11,8) -> 5*
if0(10,6,2) -> 5*
if0(3,5,7) -> 5*
if0(7,11,9) -> 5*
if0(9,1,5) -> 5*
if0(6,6,12) -> 5*
if0(7,1,6) -> 5*
if0(10,2,11) -> 5*
if0(1,10,3) -> 5*
if0(7,6,1) -> 5*
if0(11,12,3) -> 5*
if0(4,11,8) -> 5*
if0(5,6,2) -> 5*
if0(2,11,9) -> 5*
if0(4,1,5) -> 5*
if0(8,7,7) -> 5*
if0(1,6,12) -> 5*
if0(2,1,6) -> 5*
if0(11,8,12) -> 5*
if0(12,3,6) -> 5*
if0(5,2,11) -> 5*
if0(2,6,1) -> 5*
if0(6,12,3) -> 5*
if0(12,8,1) -> 5*
if0(10,8,2) -> 5*
if0(3,7,7) -> 5*
if0(9,3,5) -> 5*
if0(6,8,12) -> 5*
if0(7,3,6) -> 5*
if0(10,4,11) -> 5*
if0(1,12,3) -> 5*
if0(7,8,1) -> 5*
if0(5,8,2) -> 5*
if0(4,3,5) -> 5*
if0(8,9,7) -> 5*
if0(1,8,12) -> 5*
if0(2,3,6) -> 5*
if0(11,10,12) -> 5*
if0(12,5,6) -> 5*
if0(5,4,11) -> 5*
if0(2,8,1) -> 5*
if0(12,10,1) -> 5*
if0(10,10,2) -> 5*
if0(3,9,7) -> 5*
if0(9,5,5) -> 5*
if0(6,10,12) -> 5*
if0(7,5,6) -> 5*
if0(10,6,11) -> 5*
if0(7,10,1) -> 5*
if0(5,10,2) -> 5*
if0(4,5,5) -> 5*
if0(8,11,7) -> 5*
if0(1,10,12) -> 5*
if0(2,5,6) -> 5*
if0(8,1,4) -> 5*
if0(11,12,12) -> 5*
if0(12,7,6) -> 5*
if0(5,6,11) -> 5*
if0(2,10,1) -> 5*
if0(9,2,10) -> 5*
if0(12,12,1) -> 5*
if0(10,12,2) -> 5*
if0(3,11,7) -> 5*
if0(9,7,5) -> 5*
if0(3,1,4) -> 5*
if0(6,12,12) -> 5*
if0(7,7,6) -> 5*
if0(10,8,11) -> 5*
if0(4,2,10) -> 5*
if0(7,12,1) -> 5*
if0(5,12,2) -> 5*
if0(4,7,5) -> 5*
if0(1,12,12) -> 5*
if0(2,7,6) -> 5*
if0(8,3,4) -> 5*
if0(12,9,6) -> 5*
if0(5,8,11) -> 5*
if0(2,12,1) -> 5*
if0(9,4,10) -> 5*
if0(9,9,5) -> 5*
if0(3,3,4) -> 5*
if0(7,9,6) -> 5*
if0(10,10,11) -> 5*
if0(4,4,10) -> 5*
if0(4,9,5) -> 5*
if0(2,9,6) -> 5*
if0(8,5,4) -> 5*
if0(12,11,6) -> 5*
if0(5,10,11) -> 5*
if0(12,1,3) -> 5*
if0(9,6,10) -> 5*
if0(9,11,5) -> 5*
if0(3,5,4) -> 5*
if0(7,11,6) -> 5*
if0(7,1,3) -> 5*
if0(10,12,11) -> 5*
if0(4,6,10) -> 5*
if0(10,2,8) -> 5*
if0(8,2,9) -> 5*
if0(4,11,5) -> 5*
if0(2,11,6) -> 5*
if0(8,7,4) -> 5*
if0(2,1,3) -> 5*
if0(5,12,11) -> 5*
if0(12,3,3) -> 5*
if0(5,2,8) -> 5*
if0(9,8,10) -> 5*
if0(3,2,9) -> 5*
if0(3,7,4) -> 5*
if0(7,3,3) -> 5*
if0(4,8,10) -> 5*
if0(10,4,8) -> 5*
if0(8,4,9) -> 5*
if0(8,9,4) -> 5*
if0(2,3,3) -> 5*
if0(12,5,3) -> 5*
if0(5,4,8) -> 5*
if0(9,10,10) -> 5*
if0(3,4,9) -> 5*
if0(12,1,12) -> 5*
if0(3,9,4) -> 5*
if0(7,5,3) -> 5*
if0(4,10,10) -> 5*
if0(10,6,8) -> 5*
if0(11,1,2) -> 5*
if0(8,6,9) -> 5*
if0(7,1,12) -> 5*
if0(8,11,4) -> 5*
if0(2,5,3) -> 5*
if0(8,1,1) -> 5*
if0(12,7,3) -> 5*
if0(5,6,8) -> 5*
if0(6,1,2) -> 5*
if0(9,12,10) -> 5*
if0(3,6,9) -> 5*
if0(9,2,7) -> 5*
if0(2,1,12) -> 5*
if0(12,3,12) -> 5*
if0(3,11,4) -> 5*
if0(3,1,1) -> 5*
if0(7,7,3) -> 5*
if0(1,1,2) -> 5*
if0(4,12,10) -> 5*
if0(10,8,8) -> 5*
if0(11,3,2) -> 5*
if0(4,2,7) -> 5*
if0(8,8,9) -> 5*
if0(7,3,12) -> 5*
if0(2,7,3) -> 5*
if0(8,3,1) -> 5*
if0(12,9,3) -> 5*
if0(5,8,8) -> 5*
if0(6,3,2) -> 5*
if0(3,8,9) -> 5*
if0(9,4,7) -> 5*
if0(2,3,12) -> 5*
if0(12,5,12) -> 5*
if0(3,3,1) -> 5*
if0(7,9,3) -> 5*
if0(1,3,2) -> 5*
if0(10,10,8) -> 5*
if0(11,5,2) -> 5*
if0(4,4,7) -> 5*
if0(8,10,9) -> 5*
if0(7,5,12) -> 5*
if0(11,1,11) -> 5*
if0(2,9,3) -> 5*
if0(8,5,1) -> 5*
if0(12,11,3) -> 5*
if0(5,10,8) -> 5*
if0(6,5,2) -> 5*
if0(3,10,9) -> 5*
if0(9,6,7) -> 5*
if0(2,5,12) -> 5*
if0(12,7,12) -> 5*
if0(6,1,11) -> 5*
if0(3,5,1) -> 5*
if0(7,11,3) -> 5*
if0(1,5,2) -> 5*
if0(10,12,8) -> 5*
if0(11,7,2) -> 5*
if0(4,6,7) -> 5*
if0(8,12,9) -> 5*
if0(10,2,5) -> 5*
if0(7,7,12) -> 5*
if0(8,2,6) -> 5*
if0(1,1,11) -> 5*
if0(11,3,11) -> 5*
if0(2,11,3) -> 5*
if0(8,7,1) -> 5*
if0(5,12,8) -> 5*
if0(6,7,2) -> 5*
if0(3,12,9) -> 5*
if0(5,2,5) -> 5*
if0(9,8,7) -> 5*
if0(2,7,12) -> 5*
if0(3,2,6) -> 5*
if0(12,9,12) -> 5*
if0(6,3,11) -> 5*
if0(3,7,1) -> 5*
if0(1,7,2) -> 5*
if0(11,9,2) -> 5*
if0(4,8,7) -> 5*
if0(10,4,5) -> 5*
if0(7,9,12) -> 5*
if0(8,4,6) -> 5*
if0(1,3,11) -> 5*
if0(11,5,11) -> 5*
if0(8,9,1) -> 5*
if0(6,9,2) -> 5*
if0(5,4,5) -> 5*
if0(9,10,7) -> 5*
if0(2,9,12) -> 5*
if0(3,4,6) -> 5*
if0(12,11,12) -> 5*
if0(6,5,11) -> 5*
if0(3,9,1) -> 5*
if0(10,1,10) -> 5*
if0(1,9,2) -> 5*
if0(11,11,2) -> 5*
if0(4,10,7) -> 5*
if0(10,6,5) -> 5*
if0(7,11,12) -> 5*
if0(8,6,6) -> 5*
if0(1,5,11) -> 5*
if0(11,7,11) -> 5*
if0(5,1,10) -> 5*
if0(8,11,1) -> 5*
if0(6,11,2) -> 5*
if0(5,6,5) -> 5*
if0(9,12,7) -> 5*
if0(2,11,12) -> 5*
if0(3,6,6) -> 5*
if0(9,2,4) -> 5*
if0(6,7,11) -> 5*
if0(3,11,1) -> 5*
if0(10,3,10) -> 5*
if0(1,11,2) -> 5*
if0(4,12,7) -> 5*
if0(10,8,5) -> 5*
if0(4,2,4) -> 5*
if0(8,8,6) -> 5*
if0(1,7,11) -> 5*
if0(11,9,11) -> 5*
if0(5,3,10) -> 5*
if0(5,8,5) -> 5*
if0(3,8,6) -> 5*
if0(9,4,4) -> 5*
if0(6,9,11) -> 5*
if0(10,5,10) -> 5*
if0(10,10,5) -> 5*
if0(4,4,4) -> 5*
if0(8,10,6) -> 5*
if0(1,9,11) -> 5*
if0(11,11,11) -> 5*
if0(5,5,10) -> 5*
if0(11,1,8) -> 5*
if0(9,1,9) -> 5*
if0(5,10,5) -> 5*
if0(3,10,6) -> 5*
if0(9,6,4) -> 5*
if0(6,11,11) -> 5*
if0(6,1,8) -> 5*
if0(10,7,10) -> 5*
if0(4,1,9) -> 5*
if0(10,12,5) -> 5*
if0(4,6,4) -> 5*
if0(8,12,6) -> 5*
if0(1,11,11) -> 5*
if0(8,2,3) -> 5*
if0(1,1,8) -> 5*
if0(5,7,10) -> 5*
if0(11,3,8) -> 5*
if0(9,3,9) -> 5*
if0(5,12,5) -> 5*
if0(3,12,6) -> 5*
if0(9,8,4) -> 5*
if0(3,2,3) -> 5*
if0(6,3,8) -> 5*
if0(10,9,10) -> 5*
if0(4,3,9) -> 5*
if0(4,8,4) -> 5*
if0(8,4,3) -> 5*
if0(1,3,8) -> 5*
if0(5,9,10) -> 5*
if0(11,5,8) -> 5*
if0(9,5,9) -> 5*
if0(9,10,4) -> 5*
if0(3,4,3) -> 5*
if0(6,5,8) -> 5*
if0(10,11,10) -> 5*
if0(4,5,9) -> 5*
if0(10,1,7) -> 5*
if0(4,10,4) -> 5*
if0(8,6,3) -> 5*
if0(1,5,8) -> 5*
if0(5,11,10) -> 5*
if0(11,7,8) -> 5*
if0(12,2,2) -> 5*
if0(5,1,7) -> 5*
if0(9,7,9) -> 5*
if0(8,2,12) -> 5*
if0(9,12,4) -> 5*
if0(3,6,3) -> 5*
if0(9,2,1) -> 5*
if0(6,7,8) -> 5*
if0(7,2,2) -> 5*
if0(4,7,9) -> 5*
if0(10,3,7) -> 5*
if0(3,2,12) -> 5*
if0(4,12,4) -> 5*
if0(4,2,1) -> 5*
if0(8,8,3) -> 5*
if0(1,7,8) -> 5*
if0(2,2,2) -> 5*
if0(11,9,8) -> 5*
if0(12,4,2) -> 5*
if0(5,3,7) -> 5*
if0(9,9,9) -> 5*
if0(8,4,12) -> 5*
if0(3,8,3) -> 5*
if0(9,4,1) -> 5*
if0(6,9,8) -> 5*
if0(7,4,2) -> 5*
if0(4,9,9) -> 5*
if0(10,5,7) -> 5*
if0(3,4,12) -> 5*
if0(4,4,1) -> 5*
if0(8,10,3) -> 5*
if0(1,9,8) -> 5*
if0(2,4,2) -> 5*
if0(11,11,8) -> 5*
if0(12,6,2) -> 5*
if0(5,5,7) -> 5*
if0(9,11,9) -> 5*
if0(11,1,5) -> 5*
if0(8,6,12) -> 5*
if0(9,1,6) -> 5*
if0(12,2,11) -> 5*
if0(3,10,3) -> 5*
if0(9,6,1) -> 5*
if0(6,11,8) -> 5*
if0(7,6,2) -> 5*
if0(4,11,9) -> 5*
if0(6,1,5) -> 5*
if0(10,7,7) -> 5*
if0(3,6,12) -> 5*
if0(4,1,6) -> 5*
if0(7,2,11) -> 5*
if0(4,6,1) -> 5*
if0(8,12,3) -> 5*
if0(1,11,8) -> 5*
if0(2,6,2) -> 5*
if0(12,8,2) -> 5*
if0(1,1,5) -> 5*
if0(5,7,7) -> 5*
if0(11,3,5) -> 5*
if0(8,8,12) -> 5*
if0(9,3,6) -> 5*
if0(2,2,11) -> 5*
if0(12,4,11) -> 5*
if0(3,12,3) -> 5*
if0(9,8,1) -> 5*
if0(7,8,2) -> 5*
if0(6,3,5) -> 5*
if0(10,9,7) -> 5*
if0(3,8,12) -> 5*
if0(4,3,6) -> 5*
if0(7,4,11) -> 5*
if0(4,8,1) -> 5*
if0(2,8,2) -> 5*
if0(12,10,2) -> 5*
if0(1,3,5) -> 5*
if0(5,9,7) -> 5*
if0(11,5,5) -> 5*
if0(8,10,12) -> 5*
if0(9,5,6) -> 5*
if0(2,4,11) -> 5*
if0(12,6,11) -> 5*
if0(9,10,1) -> 5*
if0(7,10,2) -> 5*
if0(6,5,5) -> 5*
if0(10,11,7) -> 5*
if0(3,10,12) -> 5*
if0(4,5,6) -> 5*
if0(10,1,4) -> 5*
if0(7,6,11) -> 5*
if0(4,10,1) -> 5*
if0(11,2,10) -> 5*
if0(2,10,2) -> 5*
if0(12,12,2) -> 5*
if0(1,5,5) -> 5*
if0(5,11,7) -> 5*
if0(11,7,5) -> 5*
if0(5,1,4) -> 5*
if0(8,12,12) -> 5*
if0(9,7,6) -> 5*
if0(2,6,11) -> 5*
if0(12,8,11) -> 5*
if0(6,2,10) -> 5*
if0(9,12,1) -> 5*
if0(7,12,2) -> 5*
if0(6,7,5) -> 5*
if0(3,12,12) -> 5*
if0(4,7,6) -> 5*
if0(10,3,4) -> 5*
if0(7,8,11) -> 5*
if0(1,2,10) -> 5*
if0(4,12,1) -> 5*
if0(11,4,10) -> 5*
if0(2,12,2) -> 5*
if0(1,7,5) -> 5*
if0(11,9,5) -> 5*
if0(5,3,4) -> 5*
if0(9,9,6) -> 5*
if0(2,8,11) -> 5*
if0(12,10,11) -> 5*
if0(6,4,10) -> 5*
if0(6,9,5) -> 5*
if0(4,9,6) -> 5*
if0(10,5,4) -> 5*
if0(7,10,11) -> 5*
if0(1,4,10) -> 5*
if0(11,6,10) -> 5*
if0(1,9,5) -> 5*
if0(11,11,5) -> 5*
if0(5,5,4) -> 5*
if0(9,11,6) -> 5*
if0(2,10,11) -> 5*
if0(9,1,3) -> 5*
if0(12,12,11) -> 5*
if0(6,6,10) -> 5*
if0(12,2,8) -> 5*
if0(10,2,9) -> 5*
if0(6,11,5) -> 5*
if0(4,11,6) -> 5*
if0(10,7,4) -> 5*
if0(4,1,3) -> 5*
if0(7,12,11) -> 5*
if0(1,6,10) -> 5*
if0(7,2,8) -> 5*
if0(11,8,10) -> 5*
if0(5,2,9) -> 5*
if0(1,11,5) -> 5*
if0(5,7,4) -> 5*
if0(2,12,11) -> 5*
if0(9,3,3) -> 5*
if0(2,2,8) -> 5*
if0(6,8,10) -> 5*
if0(12,4,8) -> 5*
if0(10,4,9) -> 5*
if0(10,9,4) -> 5*
if0(4,3,3) -> 5*
if0(1,8,10) -> 5*
if0(7,4,8) -> 5*
if0(11,10,10) -> 5*
if0(5,4,9) -> 5*
if0(5,9,4) -> 5*
if0(9,5,3) -> 5*
if0(2,4,8) -> 5*
if0(6,10,10) -> 5*
if0(12,6,8) -> 5*
if0(10,6,9) -> 5*
if0(9,1,12) -> 5*
if0(10,11,4) -> 5*
if0(4,5,3) -> 5*
if0(10,1,1) -> 5*
if0(1,10,10) -> 5*
if0(7,6,8) -> 5*
if0(8,1,2) -> 5*
if0(11,12,10) -> 5*
if0(5,6,9) -> 5*
if0(11,2,7) -> 5*
if0(4,1,12) -> 5*
if0(5,11,4) -> 5*
if0(5,1,1) -> 5*
if0(9,7,3) -> 5*
if0(2,6,8) -> 5*
if0(3,1,2) -> 5*
if0(6,12,10) -> 5*
if0(12,8,8) -> 5*
if0(6,2,7) -> 5*
if0(10,8,9) -> 5*
if0(9,3,12) -> 5*
if0(4,7,3) -> 5*
if0(10,3,1) -> 5*
if0(1,12,10) -> 5*
if0(7,8,8) -> 5*
if0(8,3,2) -> 5*
if0(1,2,7) -> 5*
if0(5,8,9) -> 5*
if0(11,4,7) -> 5*
if0(4,3,12) -> 5*
if0(5,3,1) -> 5*
if0(9,9,3) -> 5*
if0(2,8,8) -> 5*
if0(3,3,2) -> 5*
if0(12,10,8) -> 5*
if0(6,4,7) -> 5*
if0(10,10,9) -> 5*
if0(9,5,12) -> 5*
if0(4,9,3) -> 5*
if0(10,5,1) -> 5*
if0(7,10,8) -> 5*
if0(8,5,2) -> 5*
if0(1,4,7) -> 5*
if0(5,10,9) -> 5*
if0(11,6,7) -> 5*
if0(4,5,12) -> 5*
if0(8,1,11) -> 5*
if0(5,5,1) -> 5*
if0(9,11,3) -> 5*
if0(2,10,8) -> 5*
if0(3,5,2) -> 5*
if0(12,12,8) -> 5*
if0(6,6,7) -> 5*
if0(10,12,9) -> 5*
if0(12,2,5) -> 5*
if0(9,7,12) -> 5*
if0(10,2,6) -> 5*
if0(3,1,11) -> 5*
if0(4,11,3) -> 5*
if0(10,7,1) -> 5*
if0(7,12,8) -> 5*
if0(8,7,2) -> 5*
if0(1,6,7) -> 5*
if0(5,12,9) -> 5*
if0(7,2,5) -> 5*
if0(11,8,7) -> 5*
if0(4,7,12) -> 5*
if0(5,2,6) -> 5*
if0(8,3,11) -> 5*
if0(5,7,1) -> 5*
if0(2,12,8) -> 5*
if0(3,7,2) -> 5*
if0(2,2,5) -> 5*
if0(6,8,7) -> 5*
if0(12,4,5) -> 5*
if0(9,9,12) -> 5*
if0(10,4,6) -> 5*
if0(3,3,11) -> 5*
if0(10,9,1) -> 5*
if0(8,9,2) -> 5*
if0(1,8,7) -> 5*
if0(7,4,5) -> 5*
if0(11,10,7) -> 5*
if0(4,9,12) -> 5*
if0(5,4,6) -> 5*
if0(8,5,11) -> 5*
if0(5,9,1) -> 5*
if0(12,1,10) -> 5*
if0(3,9,2) -> 5*
if0(2,4,5) -> 5*
if0(6,10,7) -> 5*
if0(12,6,5) -> 5*
if0(9,11,12) -> 5*
if0(10,6,6) -> 5*
if0(3,5,11) -> 5*
if0(7,1,10) -> 5*
if0(10,11,1) -> 5*
if0(8,11,2) -> 5*
if0(1,10,7) -> 5*
if0(7,6,5) -> 5*
if0(11,12,7) -> 5*
if0(4,11,12) -> 5*
if0(5,6,6) -> 5*
if0(11,2,4) -> 5*
if0(8,7,11) -> 5*
if0(2,1,10) -> 5*
if0(5,11,1) -> 5*
if0(12,3,10) -> 5*
if0(3,11,2) -> 5*
if0(2,6,5) -> 5*
if0(6,12,7) -> 5*
if0(12,8,5) -> 5*
if0(6,2,4) -> 5*
if0(10,8,6) -> 5*
if0(3,7,11) -> 5*
if0(7,3,10) -> 5*
if0(1,12,7) -> 5*
if0(7,8,5) -> 5*
if0(1,2,4) -> 5*
if0(5,8,6) -> 5*
if0(11,4,4) -> 5*
if0(8,9,11) -> 5*
if0(2,3,10) -> 5*
if0(12,5,10) -> 5*
if0(2,8,5) -> 5*
if0(12,10,5) -> 5*
if0(6,4,4) -> 5*
if0(10,10,6) -> 5*
if0(3,9,11) -> 5*
if0(7,5,10) -> 5*
if0(11,1,9) -> 5*
if0(7,10,5) -> 5*
if0(1,4,4) -> 5*
if0(5,10,6) -> 5*
if0(11,6,4) -> 5*
if0(8,11,11) -> 5*
if0(2,5,10) -> 5*
if0(8,1,8) -> 5*
if0(12,7,10) -> 5*
if0(6,1,9) -> 5*
if0(2,10,5) -> 5*
if0(12,12,5) -> 5*
if0(6,6,4) -> 5*
if0(10,12,6) -> 5*
if0(3,11,11) -> 5*
if0(10,2,3) -> 5*
if0(3,1,8) -> 5*
if0(7,7,10) -> 5*
if0(1,1,9) -> 5*
if0(11,3,9) -> 5*
if0(7,12,5) -> 5*
if0(1,6,4) -> 5*
if0(5,12,6) -> 5*
if0(11,8,4) -> 5*
if0(5,2,3) -> 5*
if0(2,7,10) -> 5*
if0(8,3,8) -> 5*
if0(12,9,10) -> 5*
if0(6,3,9) -> 5*
if0(2,12,5) -> 5*
if0(6,8,4) -> 5*
if0(10,4,3) -> 5*
if0(3,3,8) -> 5*
if0(7,9,10) -> 5*
if0(1,3,9) -> 5*
if0(11,5,9) -> 5*
if0(1,8,4) -> 5*
if0(11,10,4) -> 5*
if0(5,4,3) -> 5*
if0(2,9,10) -> 5*
if0(8,5,8) -> 5*
if0(12,11,10) -> 5*
if0(6,5,9) -> 5*
if0(12,1,7) -> 5*
if0(6,10,4) -> 5*
if0(10,6,3) -> 5*
if0(3,5,8) -> 5*
if0(7,11,10) -> 5*
if0(1,5,9) -> 5*
if0(7,1,7) -> 5*
if0(11,7,9) -> 5*
if0(10,2,12) -> 5*
if0(1,10,4) -> 5*
if0(11,12,4) -> 5*
if0(5,6,3) -> 5*
if0(11,2,1) -> 5*
if0(2,11,10) -> 5*
if0(8,7,8) -> 5*
if0(9,2,2) -> 5*
if0(2,1,7) -> 5*
if0(6,7,9) -> 5*
if0(12,3,7) -> 5*
if0(5,2,12) -> 5*
if0(6,12,4) -> 5*
if0(6,2,1) -> 5*
if0(10,8,3) -> 5*
if0(3,7,8) -> 5*
if0(4,2,2) -> 5*
if0(1,7,9) -> 5*
if0(7,3,7) -> 5*
if0(11,9,9) -> 5*
if0(10,4,12) -> 5*
if0(1,12,4) -> 5*
if0(1,2,1) -> 5*
if0(5,8,3) -> 5*
if0(11,4,1) -> 5*
if0(8,9,8) -> 5*
if0(9,4,2) -> 5*
if0(2,3,7) -> 5*
if0(6,9,9) -> 5*
if0(12,5,7) -> 5*
if0(5,4,12) -> 5*
if0(6,4,1) -> 5*
if0(10,10,3) -> 5*
if0(3,9,8) -> 5*
if0(4,4,2) -> 5*
if0(1,9,9) -> 5*
if0(7,5,7) -> 5*
if0(11,11,9) -> 5*
if0(10,6,12) -> 5*
if0(11,1,6) -> 5*
if0(1,4,1) -> 5*
if0(5,10,3) -> 5*
if0(11,6,1) -> 5*
if0(8,11,8) -> 5*
if0(9,6,2) -> 5*
if0(2,5,7) -> 5*
if0(6,11,9) -> 5*
if0(8,1,5) -> 5*
if0(12,7,7) -> 5*
if0(5,6,12) -> 5*
if0(6,1,6) -> 5*
if0(9,2,11) -> 5*
if0(6,6,1) -> 5*
if0(10,12,3) -> 5*
if0(3,11,8) -> 5*
if0(4,6,2) -> 5*
if0(1,11,9) -> 5*
if0(3,1,5) -> 5*
if0(7,7,7) -> 5*
if0(1,1,6) -> 5*
if0(10,8,12) -> 5*
if0(11,3,6) -> 5*
if0(4,2,11) -> 5*
if0(1,6,1) -> 5*
if0(5,12,3) -> 5*
if0(11,8,1) -> 5*
if0(9,8,2) -> 5*
if0(2,7,7) -> 5*
if0(8,3,5) -> 5*
if0(12,9,7) -> 5*
if0(5,8,12) -> 5*
if0(6,3,6) -> 5*
if0(9,4,11) -> 5*
if0(6,8,1) -> 5*
if0(4,8,2) -> 5*
if0(3,3,5) -> 5*
if0(7,9,7) -> 5*
if0(1,3,6) -> 5*
if0(10,10,12) -> 5*
if0(11,5,6) -> 5*
if0(4,4,11) -> 5*
if0(1,8,1) -> 5*
if0(11,10,1) -> 5*
if0(9,10,2) -> 5*
if0(2,9,7) -> 5*
if0(8,5,5) -> 5*
if0(12,11,7) -> 5*
if0(5,10,12) -> 5*
if0(6,5,6) -> 5*
if0(12,1,4) -> 5*
if0(9,6,11) -> 5*
if0(6,10,1) -> 5*
if0(4,10,2) -> 5*
if0(3,5,5) -> 5*
if0(7,11,7) -> 5*
if0(1,5,6) -> 5*
if0(7,1,4) -> 5*
if0(10,12,12) -> 5*
if0(11,7,6) -> 5*
if0(4,6,11) -> 5*
if0(1,10,1) -> 5*
if0(8,2,10) -> 5*
if0(11,12,1) -> 5*
if0(9,12,2) -> 5*
if0(2,11,7) -> 5*
if0(8,7,5) -> 5*
if0(2,1,4) -> 5*
if0(5,12,12) -> 5*
if0(6,7,6) -> 5*
if0(12,3,4) -> 5*
if0(9,8,11) -> 5*
if0(3,2,10) -> 5*
if0(6,12,1) -> 5*
if0(4,12,2) -> 5*
if0(3,7,5) -> 5*
if0(1,7,6) -> 5*
if0(7,3,4) -> 5*
if0(11,9,6) -> 5*
if0(4,8,11) -> 5*
if0(1,12,1) -> 5*
if0(8,4,10) -> 5*
if0(8,9,5) -> 5*
if0(2,3,4) -> 5*
if0(6,9,6) -> 5*
if0(12,5,4) -> 5*
if0(9,10,11) -> 5*
if0(3,4,10) -> 5*
if0(3,9,5) -> 5*
if0(1,9,6) -> 5*
if0(7,5,4) -> 5*
if0(11,11,6) -> 5*
if0(4,10,11) -> 5*
if0(11,1,3) -> 5*
if0(8,6,10) -> 5*
if0(12,2,9) -> 5*
if0(8,11,5) -> 5*
if0(2,5,4) -> 5*
if0(6,11,6) -> 5*
if0(12,7,4) -> 5*
if0(6,1,3) -> 5*
if0(9,12,11) -> 5*
if0(3,6,10) -> 5*
if0(9,2,8) -> 5*
if0(7,2,9) -> 5*
if0(3,11,5) -> 5*
if0(1,11,6) -> 5*
if0(7,7,4) -> 5*
if0(1,1,3) -> 5*
if0(4,12,11) -> 5*
if0(11,3,3) -> 5*
if0(4,2,8) -> 5*
if0(8,8,10) -> 5*
if0(2,2,9) -> 5*
if0(12,4,9) -> 5*
if0(2,7,4) -> 5*
if0(12,9,4) -> 5*
if0(6,3,3) -> 5*
if0(3,8,10) -> 5*
if0(9,4,8) -> 5*
if0(7,4,9) -> 5*
if0(7,9,4) -> 5*
if0(1,3,3) -> 5*
if0(11,5,3) -> 5*
if0(4,4,8) -> 5*
if0(8,10,10) -> 5*
if0(2,4,9) -> 5*
if0(12,6,9) -> 5*
if0(11,1,12) -> 5*
if0(2,9,4) -> 5*
if0(12,11,4) -> 5*
if0(6,5,3) -> 5*
if0(12,1,1) -> 5*
if0(3,10,10) -> 5*
if0(9,6,8) -> 5*
if0(10,1,2) -> 5*
if0(7,6,9) -> 5*
if0(6,1,12) -> 5*
if0(7,11,4) -> 5*
if0(1,5,3) -> 5*
if0(7,1,1) -> 5*
if0(11,7,3) -> 5*
if0(4,6,8) -> 5*
if0(5,1,2) -> 5*
if0(8,12,10) -> 5*
if0(2,6,9) -> 5*
if0(8,2,7) -> 5*
if0(12,8,9) -> 5*
if0(1,1,12) -> 5*
if0(11,3,12) -> 5*
if0(2,11,4) -> 5*
if0(2,1,1) -> 5*
if0(6,7,3) -> 5*
if0(12,3,1) -> 5*
if0(3,12,10) -> 5*
if0(9,8,8) -> 5*
if0(10,3,2) -> 5*
if0(3,2,7) -> 5*
if0(7,8,9) -> 5*
if0(6,3,12) -> 5*
if0(1,7,3) -> 5*
if0(7,3,1) -> 5*
if0(11,9,3) -> 5*
if0(4,8,8) -> 5*
if0(5,3,2) -> 5*
if0(2,8,9) -> 5*
if0(8,4,7) -> 5*
if0(12,10,9) -> 5*
if0(1,3,12) -> 5*
if0(11,5,12) -> 5*
if0(2,3,1) -> 5*
if0(6,9,3) -> 5*
if0(12,5,1) -> 5*
if0(9,10,8) -> 5*
if0(10,5,2) -> 5*
if0(3,4,7) -> 5*
if0(7,10,9) -> 5*
if0(6,5,12) -> 5*
if0(10,1,11) -> 5*
if0(1,9,3) -> 5*
if0(7,5,1) -> 5*
if0(11,11,3) -> 5*
if0(4,10,8) -> 5*
if0(5,5,2) -> 5*
if0(2,10,9) -> 5*
if0(8,6,7) -> 5*
if0(12,12,9) -> 5*
if0(1,5,12) -> 5*
if0(11,7,12) -> 5*
if0(12,2,6) -> 5*
if0(5,1,11) -> 5*
if0(2,5,1) -> 5*
if0(6,11,3) -> 5*
if0(12,7,1) -> 5*
if0(9,12,8) -> 5*
if0(10,7,2) -> 5*
if0(3,6,7) -> 5*
if0(7,12,9) -> 5*
if0(9,2,5) -> 5*
if0(6,7,12) -> 5*
if0(7,2,6) -> 5*
if0(10,3,11) -> 5*
if0(1,11,3) -> 5*
if0(7,7,1) -> 5*
if0(4,12,8) -> 5*
if0(5,7,2) -> 5*
if0(2,12,9) -> 5*
if0(4,2,5) -> 5*
if0(8,8,7) -> 5*
if0(1,7,12) -> 5*
if0(2,2,6) -> 5*
if0(11,9,12) -> 5*
if0(12,4,6) -> 5*
if0(5,3,11) -> 5*
if0(2,7,1) -> 5*
if0(12,9,1) -> 5*
if0(10,9,2) -> 5*
if0(3,8,7) -> 5*
if0(9,4,5) -> 5*
if0(6,9,12) -> 5*
if0(7,4,6) -> 5*
if0(10,5,11) -> 5*
if0(7,9,1) -> 5*
if0(5,9,2) -> 5*
if0(4,4,5) -> 5*
if0(8,10,7) -> 5*
if0(1,9,12) -> 5*
if0(2,4,6) -> 5*
if0(11,11,12) -> 5*
if0(12,6,6) -> 5*
if0(5,5,11) -> 5*
if0(2,9,1) -> 5*
if0(9,1,10) -> 5*
if0(12,11,1) -> 5*
if0(10,11,2) -> 5*
if0(3,10,7) -> 5*
if0(9,6,5) -> 5*
if0(6,11,12) -> 5*
if0(7,6,6) -> 5*
if0(10,7,11) -> 5*
if0(4,1,10) -> 5*
if0(7,11,1) -> 5*
if0(5,11,2) -> 5*
if0(4,6,5) -> 5*
if0(8,12,7) -> 5*
if0(1,11,12) -> 5*
if0(2,6,6) -> 5*
if0(8,2,4) -> 5*
if0(12,8,6) -> 5*
if0(5,7,11) -> 5*
if0(2,11,1) -> 5*
if0(9,3,10) -> 5*
if0(3,12,7) -> 5*
if0(9,8,5) -> 5*
if0(3,2,4) -> 5*
if0(7,8,6) -> 5*
if0(10,9,11) -> 5*
if0(4,3,10) -> 5*
if0(4,8,5) -> 5*
if0(2,8,6) -> 5*
if0(8,4,4) -> 5*
if0(12,10,6) -> 5*
if0(5,9,11) -> 5*
if0(9,5,10) -> 5*
if0(9,10,5) -> 5*
if0(3,4,4) -> 5*
if0(7,10,6) -> 5*
if0(10,11,11) -> 5*
if0(4,5,10) -> 5*
if0(10,1,8) -> 5*
if0(8,1,9) -> 5*
if0(4,10,5) -> 5*
if0(2,10,6) -> 5*
if0(8,6,4) -> 5*
if0(12,12,6) -> 5*
if0(5,11,11) -> 5*
if0(12,2,3) -> 5*
if0(5,1,8) -> 5*
if0(9,7,10) -> 5*
if0(3,1,9) -> 5*
if0(9,12,5) -> 5*
if0(3,6,4) -> 5*
if0(7,12,6) -> 5*
if0(7,2,3) -> 5*
if0(4,7,10) -> 5*
if0(10,3,8) -> 5*
if0(8,3,9) -> 5*
if0(4,12,5) -> 5*
if0(2,12,6) -> 5*
if0(8,8,4) -> 5*
if0(2,2,3) -> 5*
if0(12,4,3) -> 5*
if0(5,3,8) -> 5*
if0(9,9,10) -> 5*
if0(3,3,9) -> 5*
if0(3,8,4) -> 5*
if0(7,4,3) -> 5*
if0(4,9,10) -> 5*
if0(10,5,8) -> 5*
if0(8,5,9) -> 5*
if0(8,10,4) -> 5*
if0(2,4,3) -> 5*
if0(12,6,3) -> 5*
if0(5,5,8) -> 5*
if0(9,11,10) -> 5*
if0(3,5,9) -> 5*
if0(9,1,7) -> 5*
if0(12,2,12) -> 5*
if0(3,10,4) -> 5*
if0(7,6,3) -> 5*
if0(4,11,10) -> 5*
if0(10,7,8) -> 5*
if0(11,2,2) -> 5*
if0(4,1,7) -> 5*
if0(8,7,9) -> 5*
if0(7,2,12) -> 5*
if0(8,12,4) -> 5*
if0(2,6,3) -> 5*
if0(8,2,1) -> 5*
if0(12,8,3) -> 5*
if0(5,7,8) -> 5*
if0(6,2,2) -> 5*
if0(3,7,9) -> 5*
if0(9,3,7) -> 5*
if0(2,2,12) -> 5*
if0(12,4,12) -> 5*
if0(3,12,4) -> 5*
if0(3,2,1) -> 5*
if0(7,8,3) -> 5*
if0(1,2,2) -> 5*
if0(10,9,8) -> 5*
if0(11,4,2) -> 5*
if0(4,3,7) -> 5*
if0(8,9,9) -> 5*
if0(7,4,12) -> 5*
if0(2,8,3) -> 5*
if0(8,4,1) -> 5*
if0(12,10,3) -> 5*
if0(5,9,8) -> 5*
if0(6,4,2) -> 5*
if0(3,9,9) -> 5*
if0(9,5,7) -> 5*
if0(2,4,12) -> 5*
if0(12,6,12) -> 5*
if0(3,4,1) -> 5*
if0(7,10,3) -> 5*
if0(1,4,2) -> 5*
if0(10,11,8) -> 5*
if0(11,6,2) -> 5*
if0(4,5,7) -> 5*
if0(8,11,9) -> 5*
if0(10,1,5) -> 5*
if0(7,6,12) -> 5*
if0(8,1,6) -> 5*
if0(11,2,11) -> 5*
if0(2,10,3) -> 5*
if0(8,6,1) -> 5*
if0(12,12,3) -> 5*
if0(5,11,8) -> 5*
if0(6,6,2) -> 5*
if0(3,11,9) -> 5*
if0(5,1,5) -> 5*
if0(9,7,7) -> 5*
if0(2,6,12) -> 5*
if0(3,1,6) -> 5*
if0(12,8,12) -> 5*
if0(6,2,11) -> 5*
if0(3,6,1) -> 5*
if0(7,12,3) -> 5*
if0(1,6,2) -> 5*
if0(11,8,2) -> 5*
if0(4,7,7) -> 5*
if0(10,3,5) -> 5*
if0(7,8,12) -> 5*
if0(8,3,6) -> 5*
if0(1,2,11) -> 5*
if0(11,4,11) -> 5*
if0(2,12,3) -> 5*
if0(8,8,1) -> 5*
if0(6,8,2) -> 5*
if0(5,3,5) -> 5*
if0(9,9,7) -> 5*
if0(2,8,12) -> 5*
if0(3,3,6) -> 5*
if0(12,10,12) -> 5*
if0(6,4,11) -> 5*
if0(3,8,1) -> 5*
if0(1,8,2) -> 5*
if0(11,10,2) -> 5*
if0(4,9,7) -> 5*
if0(10,5,5) -> 5*
if0(7,10,12) -> 5*
if0(8,5,6) -> 5*
if0(1,4,11) -> 5*
if0(11,6,11) -> 5*
if0(8,10,1) -> 5*
if0(6,10,2) -> 5*
if0(5,5,5) -> 5*
if0(9,11,7) -> 5*
if0(2,10,12) -> 5*
if0(3,5,6) -> 5*
if0(9,1,4) -> 5*
if0(12,12,12) -> 5*
if0(6,6,11) -> 5*
if0(3,10,1) -> 5*
if0(10,2,10) -> 5*
if0(1,10,2) -> 5*
if0(11,12,2) -> 5*
if0(4,11,7) -> 5*
if0(10,7,5) -> 5*
if0(4,1,4) -> 5*
if0(7,12,12) -> 5*
if0(8,7,6) -> 5*
if0(1,6,11) -> 5*
if0(11,8,11) -> 5*
if0(5,2,10) -> 5*
if0(8,12,1) -> 5*
if0(6,12,2) -> 5*
if0(5,7,5) -> 5*
if0(2,12,12) -> 5*
if0(3,7,6) -> 5*
if0(9,3,4) -> 5*
if0(6,8,11) -> 5*
if0(3,12,1) -> 5*
if0(10,4,10) -> 5*
if0(1,12,2) -> 5*
if0(10,9,5) -> 5*
if0(4,3,4) -> 5*
if0(8,9,6) -> 5*
if0(1,8,11) -> 5*
if0(11,10,11) -> 5*
if0(5,4,10) -> 5*
if0(5,9,5) -> 5*
if0(3,9,6) -> 5*
if0(9,5,4) -> 5*
if0(6,10,11) -> 5*
if0(10,6,10) -> 5*
if0(10,11,5) -> 5*
if0(4,5,4) -> 5*
if0(8,11,6) -> 5*
if0(1,10,11) -> 5*
if0(8,1,3) -> 5*
if0(11,12,11) -> 5*
if0(5,6,10) -> 5*
if0(11,2,8) -> 5*
if0(9,2,9) -> 5*
if0(5,11,5) -> 5*
if0(3,11,6) -> 5*
if0(9,7,4) -> 5*
if0(3,1,3) -> 5*
if0(6,12,11) -> 5*
if0(6,2,8) -> 5*
if0(10,8,10) -> 5*
if0(4,2,9) -> 5*
if0(4,7,4) -> 5*
if0(1,12,11) -> 5*
if0(8,3,3) -> 5*
if0(1,2,8) -> 5*
if0(5,8,10) -> 5*
if0(11,4,8) -> 5*
if0(9,4,9) -> 5*
if0(9,9,4) -> 5*
if0(3,3,3) -> 5*
if0(6,4,8) -> 5*
if0(10,10,10) -> 5*
if0(4,4,9) -> 5*
if0(4,9,4) -> 5*
if0(8,5,3) -> 5*
if0(1,4,8) -> 5*
if0(5,10,10) -> 5*
if0(11,6,8) -> 5*
if0(12,1,2) -> 5*
if0(9,6,9) -> 5*
if0(8,1,12) -> 5*
if0(9,11,4) -> 5*
if0(3,5,3) -> 5*
if0(9,1,1) -> 5*
if0(6,6,8) -> 5*
if0(7,1,2) -> 5*
if0(10,12,10) -> 5*
if0(4,6,9) -> 5*
if0(10,2,7) -> 5*
if0(3,1,12) -> 5*
if0(4,11,4) -> 5*
if0(4,1,1) -> 5*
if0(8,7,3) -> 5*
if0(1,6,8) -> 5*
if0(2,1,2) -> 5*
if0(5,12,10) -> 5*
if0(11,8,8) -> 5*
if0(12,3,2) -> 5*
if0(5,2,7) -> 5*
if0(9,8,9) -> 5*
if0(8,3,12) -> 5*
if0(3,7,3) -> 5*
if0(9,3,1) -> 5*
if0(6,8,8) -> 5*
if0(7,3,2) -> 5*
if0(4,8,9) -> 5*
if0(10,4,7) -> 5*
if0(3,3,12) -> 5*
if0(4,3,1) -> 5*
if0(8,9,3) -> 5*
if0(1,8,8) -> 5*
if0(2,3,2) -> 5*
if0(11,10,8) -> 5*
if0(12,5,2) -> 5*
if0(5,4,7) -> 5*
if0(9,10,9) -> 5*
if0(8,5,12) -> 5*
if0(12,1,11) -> 5*
if0(3,9,3) -> 5*
if0(9,5,1) -> 5*
if0(6,10,8) -> 5*
if0(7,5,2) -> 5*
if0(4,10,9) -> 5*
if0(10,6,7) -> 5*
if0(3,5,12) -> 5*
if0(7,1,11) -> 5*
if0(4,5,1) -> 5*
if0(8,11,3) -> 5*
if0(1,10,8) -> 5*
if0(2,5,2) -> 5*
if0(11,12,8) -> 5*
if0(12,7,2) -> 5*
if0(5,6,7) -> 5*
if0(9,12,9) -> 5*
if0(11,2,5) -> 5*
if0(8,7,12) -> 5*
if0(9,2,6) -> 5*
if0(2,1,11) -> 5*
if0(12,3,11) -> 5*
if0(3,11,3) -> 5*
if0(9,7,1) -> 5*
if0(6,12,8) -> 5*
if0(7,7,2) -> 5*
if0(4,12,9) -> 5*
if0(6,2,5) -> 5*
if0(10,8,7) -> 5*
if0(3,7,12) -> 5*
if0(4,2,6) -> 5*
if0(7,3,11) -> 5*
if0(4,7,1) -> 5*
if0(1,12,8) -> 5*
if0(2,7,2) -> 5*
if0(12,9,2) -> 5*
if0(1,2,5) -> 5*
if0(5,8,7) -> 5*
if0(11,4,5) -> 5*
if0(8,9,12) -> 5*
if0(9,4,6) -> 5*
if0(2,3,11) -> 5*
if0(12,5,11) -> 5*
if0(9,9,1) -> 5*
if0(7,9,2) -> 5*
if0(6,4,5) -> 5*
if0(10,10,7) -> 5*
if0(3,9,12) -> 5*
if0(4,4,6) -> 5*
if0(7,5,11) -> 5*
if0(4,9,1) -> 5*
if0(11,1,10) -> 5*
if0(2,9,2) -> 5*
if0(12,11,2) -> 5*
if0(1,4,5) -> 5*
if0(5,10,7) -> 5*
if0(11,6,5) -> 5*
if0(8,11,12) -> 5*
if0(9,6,6) -> 5*
if0(2,5,11) -> 5*
if0(12,7,11) -> 5*
if0(6,1,10) -> 5*
if0(9,11,1) -> 5*
if0(7,11,2) -> 5*
if0(6,6,5) -> 5*
if0(10,12,7) -> 5*
if0(3,11,12) -> 5*
if0(4,6,6) -> 5*
if0(10,2,4) -> 5*
if0(7,7,11) -> 5*
if0(1,1,10) -> 5*
if0(4,11,1) -> 5*
if0(11,3,10) -> 5*
if0(2,11,2) -> 5*
if0(1,6,5) -> 5*
if0(5,12,7) -> 5*
if0(11,8,5) -> 5*
if0(5,2,4) -> 5*
if0(9,8,6) -> 5*
if0(2,7,11) -> 5*
if0(12,9,11) -> 5*
if0(6,3,10) -> 5*
if0(6,8,5) -> 5*
if0(4,8,6) -> 5*
if0(10,4,4) -> 5*
if0(7,9,11) -> 5*
if0(1,3,10) -> 5*
if0(11,5,10) -> 5*
if0(1,8,5) -> 5*
if0(11,10,5) -> 5*
if0(5,4,4) -> 5*
if0(9,10,6) -> 5*
if0(2,9,11) -> 5*
if0(12,11,11) -> 5*
if0(6,5,10) -> 5*
if0(12,1,8) -> 5*
if0(10,1,9) -> 5*
if0(6,10,5) -> 5*
if0(4,10,6) -> 5*
if0(10,6,4) -> 5*
if0(7,11,11) -> 5*
if0(1,5,10) -> 5*
if0(7,1,8) -> 5*
if0(11,7,10) -> 5*
if0(5,1,9) -> 5*
if0(1,10,5) -> 5*
if0(11,12,5) -> 5*
if0(5,6,4) -> 5*
if0(9,12,6) -> 5*
if0(2,11,11) -> 5*
if0(9,2,3) -> 5*
if0(2,1,8) -> 5*
if0(6,7,10) -> 5*
if0(12,3,8) -> 5*
if0(10,3,9) -> 5*
if0(6,12,5) -> 5*
if0(4,12,6) -> 5*
if0(10,8,4) -> 5*
if0(4,2,3) -> 5*
if0(1,7,10) -> 5*
if0(7,3,8) -> 5*
if0(11,9,10) -> 5*
if0(5,3,9) -> 5*
if0(1,12,5) -> 5*
if0(5,8,4) -> 5*
if0(9,4,3) -> 5*
if0(2,3,8) -> 5*
if0(6,9,10) -> 5*
if0(12,5,8) -> 5*
if0(10,5,9) -> 5*
if0(10,10,4) -> 5*
if0(4,4,3) -> 5*
if0(1,9,10) -> 5*
if0(7,5,8) -> 5*
if0(11,11,10) -> 5*
if0(5,5,9) -> 5*
if0(11,1,7) -> 5*
if0(5,10,4) -> 5*
if0(9,6,3) -> 5*
if0(2,5,8) -> 5*
if0(6,11,10) -> 5*
if0(12,7,8) -> 5*
if0(6,1,7) -> 5*
if0(10,7,9) -> 5*
if0(9,2,12) -> 5*
e0() -> 4*
.0(7,10) -> 3*
.0(2,10) -> 3*
.0(12,12) -> 3*
.0(7,12) -> 3*
.0(2,12) -> 3*
.0(8,1) -> 3*
.0(3,1) -> 3*
.0(8,3) -> 3*
.0(3,3) -> 3*
.0(8,5) -> 3*
.0(3,5) -> 3*
.0(8,7) -> 3*
.0(3,7) -> 3*
.0(8,9) -> 3*
.0(3,9) -> 3*
.0(8,11) -> 3*
.0(3,11) -> 3*
.0(9,2) -> 3*
.0(4,2) -> 3*
.0(9,4) -> 3*
.0(4,4) -> 3*
.0(9,6) -> 3*
.0(4,6) -> 3*
.0(9,8) -> 3*
.0(4,8) -> 3*
.0(9,10) -> 3*
.0(4,10) -> 3*
.0(9,12) -> 3*
.0(4,12) -> 3*
.0(10,1) -> 3*
.0(5,1) -> 3*
.0(10,3) -> 3*
.0(5,3) -> 3*
.0(10,5) -> 3*
.0(5,5) -> 3*
.0(10,7) -> 3*
.0(5,7) -> 3*
.0(10,9) -> 3*
.0(5,9) -> 3*
.0(10,11) -> 3*
.0(5,11) -> 3*
.0(11,2) -> 3*
.0(6,2) -> 3*
.0(1,2) -> 3*
.0(11,4) -> 3*
.0(6,4) -> 3*
.0(1,4) -> 3*
.0(11,6) -> 3*
.0(6,6) -> 3*
.0(1,6) -> 3*
.0(11,8) -> 3*
.0(6,8) -> 3*
.0(1,8) -> 3*
.0(11,10) -> 3*
.0(6,10) -> 3*
.0(1,10) -> 3*
.0(11,12) -> 3*
.0(6,12) -> 3*
.0(1,12) -> 3*
.0(12,1) -> 3*
.0(7,1) -> 3*
.0(2,1) -> 3*
.0(12,3) -> 3*
.0(7,3) -> 3*
.0(2,3) -> 3*
.0(12,5) -> 3*
.0(7,5) -> 3*
.0(2,5) -> 3*
.0(12,7) -> 3*
.0(7,7) -> 3*
.0(2,7) -> 3*
.0(12,9) -> 3*
.0(7,9) -> 3*
.0(2,9) -> 3*
.0(12,11) -> 3*
.0(7,11) -> 3*
.0(2,11) -> 3*
.0(8,2) -> 3*
.0(3,2) -> 3*
.0(8,4) -> 3*
.0(3,4) -> 3*
.0(8,6) -> 3*
.0(3,6) -> 3*
.0(8,8) -> 3*
.0(3,8) -> 3*
.0(8,10) -> 3*
.0(3,10) -> 3*
.0(8,12) -> 3*
.0(3,12) -> 3*
.0(9,1) -> 3*
.0(4,1) -> 3*
.0(9,3) -> 3*
.0(4,3) -> 3*
.0(9,5) -> 3*
.0(4,5) -> 3*
.0(9,7) -> 3*
.0(4,7) -> 3*
.0(9,9) -> 3*
.0(4,9) -> 3*
.0(9,11) -> 3*
.0(4,11) -> 3*
.0(10,2) -> 3*
.0(5,2) -> 3*
.0(10,4) -> 3*
.0(5,4) -> 3*
.0(10,6) -> 3*
.0(5,6) -> 3*
.0(10,8) -> 3*
.0(5,8) -> 3*
.0(10,10) -> 3*
.0(5,10) -> 3*
.0(10,12) -> 3*
.0(5,12) -> 3*
.0(11,1) -> 3*
.0(6,1) -> 3*
.0(1,1) -> 3*
.0(11,3) -> 3*
.0(6,3) -> 3*
.0(1,3) -> 3*
.0(11,5) -> 3*
.0(6,5) -> 3*
.0(1,5) -> 3*
.0(11,7) -> 3*
.0(6,7) -> 3*
.0(1,7) -> 3*
.0(11,9) -> 3*
.0(6,9) -> 3*
.0(1,9) -> 3*
.0(11,11) -> 3*
.0(6,11) -> 3*
.0(1,11) -> 3*
.0(12,2) -> 3*
.0(7,2) -> 3*
.0(2,2) -> 3*
.0(12,4) -> 3*
.0(7,4) -> 3*
.0(2,4) -> 3*
.0(12,6) -> 3*
.0(7,6) -> 3*
.0(2,6) -> 3*
.0(12,8) -> 3*
.0(7,8) -> 3*
.0(2,8) -> 3*
.0(12,10) -> 3*
d'0() -> 2*
h0(2,8) -> 1*
h0(12,10) -> 1*
h0(7,10) -> 1*
h0(2,10) -> 1*
h0(12,12) -> 1*
h0(7,12) -> 1*
h0(2,12) -> 1*
h0(8,1) -> 1*
h0(3,1) -> 1*
h0(8,3) -> 1*
h0(3,3) -> 1*
h0(8,5) -> 1*
h0(3,5) -> 1*
h0(8,7) -> 1*
h0(3,7) -> 1*
h0(8,9) -> 1*
h0(3,9) -> 1*
h0(8,11) -> 1*
h0(3,11) -> 1*
h0(9,2) -> 1*
h0(4,2) -> 1*
h0(9,4) -> 1*
h0(4,4) -> 1*
h0(9,6) -> 1*
h0(4,6) -> 1*
h0(9,8) -> 1*
h0(4,8) -> 1*
h0(9,10) -> 1*
h0(4,10) -> 1*
h0(9,12) -> 1*
h0(4,12) -> 1*
h0(10,1) -> 1*
h0(5,1) -> 1*
h0(10,3) -> 1*
h0(5,3) -> 1*
h0(10,5) -> 1*
h0(5,5) -> 1*
h0(10,7) -> 1*
h0(5,7) -> 1*
h0(10,9) -> 1*
h0(5,9) -> 1*
h0(10,11) -> 1*
h0(5,11) -> 1*
h0(11,2) -> 1*
h0(6,2) -> 1*
h0(1,2) -> 1*
h0(11,4) -> 1*
h0(6,4) -> 1*
h0(1,4) -> 1*
h0(11,6) -> 1*
h0(6,6) -> 1*
h0(1,6) -> 1*
h0(11,8) -> 1*
h0(6,8) -> 1*
h0(1,8) -> 1*
h0(11,10) -> 1*
h0(6,10) -> 1*
h0(1,10) -> 1*
h0(11,12) -> 1*
h0(6,12) -> 1*
h0(1,12) -> 1*
h0(12,1) -> 1*
h0(7,1) -> 1*
h0(2,1) -> 1*
h0(12,3) -> 1*
h0(7,3) -> 1*
h0(2,3) -> 1*
h0(12,5) -> 1*
h0(7,5) -> 1*
h0(2,5) -> 1*
h0(12,7) -> 1*
h0(7,7) -> 1*
h0(2,7) -> 1*
h0(12,9) -> 1*
h0(7,9) -> 1*
h0(2,9) -> 1*
h0(12,11) -> 1*
h0(7,11) -> 1*
h0(2,11) -> 1*
h0(8,2) -> 1*
h0(3,2) -> 1*
h0(8,4) -> 1*
h0(3,4) -> 1*
h0(8,6) -> 1*
h0(3,6) -> 1*
h0(8,8) -> 1*
h0(3,8) -> 1*
h0(8,10) -> 1*
h0(3,10) -> 1*
h0(8,12) -> 1*
h0(3,12) -> 1*
h0(9,1) -> 1*
h0(4,1) -> 1*
h0(9,3) -> 1*
h0(4,3) -> 1*
h0(9,5) -> 1*
h0(4,5) -> 1*
h0(9,7) -> 1*
h0(4,7) -> 1*
h0(9,9) -> 1*
h0(4,9) -> 1*
h0(9,11) -> 1*
h0(4,11) -> 1*
h0(10,2) -> 1*
h0(5,2) -> 1*
h0(10,4) -> 1*
h0(5,4) -> 1*
h0(10,6) -> 1*
h0(5,6) -> 1*
h0(10,8) -> 1*
h0(5,8) -> 1*
h0(10,10) -> 1*
h0(5,10) -> 1*
h0(10,12) -> 1*
h0(5,12) -> 1*
h0(11,1) -> 1*
h0(6,1) -> 1*
h0(1,1) -> 1*
h0(11,3) -> 1*
h0(6,3) -> 1*
h0(1,3) -> 1*
h0(11,5) -> 1*
h0(6,5) -> 1*
h0(1,5) -> 1*
h0(11,7) -> 1*
h0(6,7) -> 1*
h0(1,7) -> 1*
h0(11,9) -> 1*
h0(6,9) -> 1*
h0(1,9) -> 1*
h0(11,11) -> 1*
h0(6,11) -> 1*
h0(1,11) -> 1*
h0(12,2) -> 1*
h0(7,2) -> 1*
h0(2,2) -> 1*
h0(12,4) -> 1*
h0(7,4) -> 1*
h0(2,4) -> 1*
h0(12,6) -> 1*
h0(7,6) -> 1*
h0(2,6) -> 1*
h0(12,8) -> 1*
h0(7,8) -> 1*
problem:
QedTool IRC1
| Execution Time | Unknown |
|---|
| Answer | YES(?,O(1)) |
|---|
| Input | SK90 4.47 |
|---|
stdout:
YES(?,O(1))
Tool IRC2
| Execution Time | Unknown |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | SK90 4.47 |
|---|
stdout:
YES(?,O(n^1))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
Proof Output:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with minimal-enrichment and initial automaton 'match''
--------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
Proof Output:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ f_0(2, 2) -> 1
, f_1(6, 7) -> 4
, f_1(8, 9) -> 5
, f_1(13, 9) -> 5
, g_0(2, 2) -> 2
, g_1(14, 13) -> 11
, i_0(2, 2, 2) -> 2
, a_0() -> 2
, a_1() -> 15
, b_0() -> 2
, b_1() -> 10
, b'_0() -> 2
, b'_1() -> 12
, c_0() -> 2
, c_1() -> 11
, c_1() -> 13
, d_0() -> 2
, d_1() -> 7
, if_0(2, 2, 2) -> 2
, if_1(3, 4, 5) -> 1
, e_0() -> 2
, e_1() -> 3
, ._0(2, 2) -> 2
, ._1(10, 11) -> 6
, ._1(12, 13) -> 8
, d'_0() -> 2
, d'_1() -> 7
, d'_1() -> 9
, h_0(2, 2) -> 2
, h_1(15, 10) -> 14}Tool RC1
| Execution Time | Unknown |
|---|
| Answer | YES(?,O(1)) |
|---|
| Input | SK90 4.47 |
|---|
stdout:
YES(?,O(1))
Tool RC2
| Execution Time | Unknown |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | SK90 4.47 |
|---|
stdout:
YES(?,O(n^1))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
Proof Output:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with minimal-enrichment and initial automaton 'match''
--------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
Proof Output:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ f_0(2, 2) -> 1
, f_1(6, 7) -> 4
, f_1(8, 9) -> 5
, f_1(13, 9) -> 5
, g_0(2, 2) -> 2
, g_1(14, 13) -> 11
, i_0(2, 2, 2) -> 2
, a_0() -> 2
, a_1() -> 15
, b_0() -> 2
, b_1() -> 10
, b'_0() -> 2
, b'_1() -> 12
, c_0() -> 2
, c_1() -> 11
, c_1() -> 13
, d_0() -> 2
, d_1() -> 7
, if_0(2, 2, 2) -> 2
, if_1(3, 4, 5) -> 1
, e_0() -> 2
, e_1() -> 3
, ._0(2, 2) -> 2
, ._1(10, 11) -> 6
, ._1(12, 13) -> 8
, d'_0() -> 2
, d'_1() -> 7
, d'_1() -> 9
, h_0(2, 2) -> 2
, h_1(15, 10) -> 14}Tool pair1rc
| Execution Time | Unknown |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | SK90 4.47 |
|---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
Application of 'pair1 (timeout of 60.0 seconds)':
-------------------------------------------------
The processor is not applicable, reason is:
Input problem is not restricted to innermost rewriting
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: none
1) 'Fastest' proved the goal fastest:
'Fastest' proved the goal fastest:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the goal fastest:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ f_0(2, 2) -> 1
, f_1(6, 7) -> 4
, f_1(8, 9) -> 5
, f_1(13, 9) -> 5
, g_0(2, 2) -> 2
, g_1(14, 13) -> 11
, i_0(2, 2, 2) -> 2
, a_0() -> 2
, a_1() -> 15
, b_0() -> 2
, b_1() -> 10
, b'_0() -> 2
, b'_1() -> 12
, c_0() -> 2
, c_1() -> 11
, c_1() -> 13
, d_0() -> 2
, d_1() -> 7
, if_0(2, 2, 2) -> 2
, if_1(3, 4, 5) -> 1
, e_0() -> 2
, e_1() -> 3
, ._0(2, 2) -> 2
, ._1(10, 11) -> 6
, ._1(12, 13) -> 8
, d'_0() -> 2
, d'_1() -> 7
, d'_1() -> 9
, h_0(2, 2) -> 2
, h_1(15, 10) -> 14}
Hurray, we answered YES(?,O(n^1))Tool pair2rc
| Execution Time | Unknown |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | SK90 4.47 |
|---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
Application of 'pair2 (timeout of 60.0 seconds)':
-------------------------------------------------
The processor is not applicable, reason is:
Input problem is not restricted to innermost rewriting
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: none
1) 'Fastest' proved the goal fastest:
'Fastest' proved the goal fastest:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the goal fastest:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ f_0(2, 2) -> 1
, f_1(6, 7) -> 4
, f_1(8, 9) -> 5
, f_1(13, 9) -> 5
, g_0(2, 2) -> 2
, g_1(14, 13) -> 11
, i_0(2, 2, 2) -> 2
, a_0() -> 2
, a_1() -> 15
, b_0() -> 2
, b_1() -> 10
, b'_0() -> 2
, b'_1() -> 12
, c_0() -> 2
, c_1() -> 11
, c_1() -> 13
, d_0() -> 2
, d_1() -> 7
, if_0(2, 2, 2) -> 2
, if_1(3, 4, 5) -> 1
, e_0() -> 2
, e_1() -> 3
, ._0(2, 2) -> 2
, ._1(10, 11) -> 6
, ._1(12, 13) -> 8
, d'_0() -> 2
, d'_1() -> 7
, d'_1() -> 9
, h_0(2, 2) -> 2
, h_1(15, 10) -> 14}
Hurray, we answered YES(?,O(n^1))Tool pair3irc
| Execution Time | Unknown |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | SK90 4.47 |
|---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
The input problem contains no overlaps that give rise to inapplicable rules.
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: innermost
1) 'Fastest' proved the goal fastest:
'Fastest' proved the goal fastest:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the goal fastest:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ f_0(2, 2) -> 1
, f_1(6, 7) -> 4
, f_1(8, 9) -> 5
, f_1(13, 9) -> 5
, g_0(2, 2) -> 2
, g_1(14, 13) -> 11
, i_0(2, 2, 2) -> 2
, a_0() -> 2
, a_1() -> 15
, b_0() -> 2
, b_1() -> 10
, b'_0() -> 2
, b'_1() -> 12
, c_0() -> 2
, c_1() -> 11
, c_1() -> 13
, d_0() -> 2
, d_1() -> 7
, if_0(2, 2, 2) -> 2
, if_1(3, 4, 5) -> 1
, e_0() -> 2
, e_1() -> 3
, ._0(2, 2) -> 2
, ._1(10, 11) -> 6
, ._1(12, 13) -> 8
, d'_0() -> 2
, d'_1() -> 7
, d'_1() -> 9
, h_0(2, 2) -> 2
, h_1(15, 10) -> 14}
Hurray, we answered YES(?,O(n^1))Tool pair3rc
| Execution Time | Unknown |
|---|
| Answer | YES(?,O(n^1)) |
|---|
| Input | SK90 4.47 |
|---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
The processor is not applicable, reason is:
Input problem is not restricted to innermost rewriting
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: none
1) 'Fastest' proved the goal fastest:
'Fastest' proved the goal fastest:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the goal fastest:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ f_0(2, 2) -> 1
, f_1(6, 7) -> 4
, f_1(8, 9) -> 5
, f_1(13, 9) -> 5
, g_0(2, 2) -> 2
, g_1(14, 13) -> 11
, i_0(2, 2, 2) -> 2
, a_0() -> 2
, a_1() -> 15
, b_0() -> 2
, b_1() -> 10
, b'_0() -> 2
, b'_1() -> 12
, c_0() -> 2
, c_1() -> 11
, c_1() -> 13
, d_0() -> 2
, d_1() -> 7
, if_0(2, 2, 2) -> 2
, if_1(3, 4, 5) -> 1
, e_0() -> 2
, e_1() -> 3
, ._0(2, 2) -> 2
, ._1(10, 11) -> 6
, ._1(12, 13) -> 8
, d'_0() -> 2
, d'_1() -> 7
, d'_1() -> 9
, h_0(2, 2) -> 2
, h_1(15, 10) -> 14}
Hurray, we answered YES(?,O(n^1))Tool rc
| Execution Time | Unknown |
|---|
| Answer | YES(O(1),O(1)) |
|---|
| Input | SK90 4.47 |
|---|
stdout:
YES(O(1),O(1))
We consider the following Problem:
Strict Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: none
Certificate: YES(O(1),O(1))
Application of 'rc (timeout of 60.0 seconds)':
----------------------------------------------
'dp' proved the goal fastest:
We have computed the following dependency pairs
Strict Dependency Pairs:
{ f^#(g(i(a(), b(), b'()), c()), d()) ->
c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'()))
, f^#(g(h(a(), b()), c()), d()) ->
c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'()))}
We consider the following Problem:
Strict DPs:
{ f^#(g(i(a(), b(), b'()), c()), d()) ->
c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'()))
, f^#(g(h(a(), b()), c()), d()) ->
c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'()))}
Strict Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: none
Certificate: YES(O(1),O(1))
Application of 'usablerules':
-----------------------------
No rule is usable.
We consider the following Problem:
Strict DPs:
{ f^#(g(i(a(), b(), b'()), c()), d()) ->
c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'()))
, f^#(g(h(a(), b()), c()), d()) ->
c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'()))}
StartTerms: basic terms
Strategy: none
Certificate: YES(O(1),O(1))
Application of 'Fastest':
-------------------------
'removetails >>> ... >>> ... >>> ...' proved the goal fastest:
We consider the the dependency-graph
1: f^#(g(i(a(), b(), b'()), c()), d()) ->
c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'()))
2: f^#(g(h(a(), b()), c()), d()) ->
c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'()))
together with the congruence-graph
->{1} Noncyclic, trivial, SCC
->{2} Noncyclic, trivial, SCC
Here rules are as follows:
{ 1: f^#(g(i(a(), b(), b'()), c()), d()) ->
c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'()))
, 2: f^#(g(h(a(), b()), c()), d()) ->
c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'()))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: f^#(g(h(a(), b()), c()), d()) ->
c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'()))
, 1: f^#(g(i(a(), b(), b'()), c()), d()) ->
c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'()))}
We consider the following Problem:
StartTerms: basic terms
Strategy: none
Certificate: YES(O(1),O(1))
Application of 'simpDPRHS >>> ...':
-----------------------------------
No rule was simplified
We apply the transformation 'usablerules' on the resulting sub-problems:
Sub-problem 1:
--------------
We consider the problem
StartTerms: basic terms
Strategy: none
The input problem is not a DP-problem.
We abort the transformation and continue with the subprocessor on the problem
StartTerms: basic terms
Strategy: none
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
All strict components are empty, nothing to further orient
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
StartTerms: basic terms
Strategy: none
We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
All strict components are empty, nothing to further orient
We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
StartTerms: basic terms
Strategy: none
All strict components are empty, nothing to further orient
We abort the transformation and continue with the subprocessor on the problem
StartTerms: basic terms
Strategy: none
1) No dependency-pair could be removed
We apply the transformation 'weightgap of dimension Nat 2, maximal degree 1, cbits 4 <> ...' on the resulting sub-problems:
Sub-problem 1:
--------------
We consider the problem
StartTerms: basic terms
Strategy: none
We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
All strict components are empty, nothing to further orient
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
StartTerms: basic terms
Strategy: none
We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
All strict components are empty, nothing to further orient
We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
StartTerms: basic terms
Strategy: none
All strict components are empty, nothing to further orient
We abort the transformation and continue with the subprocessor on the problem
StartTerms: basic terms
Strategy: none
1) 'Sequentially' proved the goal fastest:
'empty' succeeded:
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(1))Tool tup3irc
| Execution Time | 5.27291ms |
|---|
| Answer | YES(O(1),O(1)) |
|---|
| Input | SK90 4.47 |
|---|
stdout:
YES(O(1),O(1))
We consider the following Problem:
Strict Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Application of 'tup3 (timeout of 60.0 seconds)':
------------------------------------------------
The input problem contains no overlaps that give rise to inapplicable rules.
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: innermost
1) 'dp' proved the goal fastest:
We have computed the following dependency pairs
Strict Dependency Pairs:
{ f^#(g(i(a(), b(), b'()), c()), d()) ->
c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'()))
, f^#(g(h(a(), b()), c()), d()) ->
c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'()))}
We consider the following Problem:
Strict DPs:
{ f^#(g(i(a(), b(), b'()), c()), d()) ->
c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'()))
, f^#(g(h(a(), b()), c()), d()) ->
c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'()))}
Weak Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Application of 'Fastest':
-------------------------
'compose (statically using 'split all congruence from CWD except leafs', multiplication)' proved the goal fastest:
Compose is inapplicable since some weak rule is size increasing
We abort the transformation and continue with the subprocessor on the problem
Strict DPs:
{ f^#(g(i(a(), b(), b'()), c()), d()) ->
c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'()))
, f^#(g(h(a(), b()), c()), d()) ->
c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'()))}
Weak Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: innermost
1) We consider the the dependency-graph
1: f^#(g(i(a(), b(), b'()), c()), d()) ->
c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'()))
2: f^#(g(h(a(), b()), c()), d()) ->
c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'()))
together with the congruence-graph
->{1} Noncyclic, trivial, SCC
->{2} Noncyclic, trivial, SCC
Here rules are as follows:
{ 1: f^#(g(i(a(), b(), b'()), c()), d()) ->
c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'()))
, 2: f^#(g(h(a(), b()), c()), d()) ->
c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'()))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: f^#(g(h(a(), b()), c()), d()) ->
c_2(f^#(.(b(), g(h(a(), b()), c())), d()), f^#(c(), d'()))
, 1: f^#(g(i(a(), b(), b'()), c()), d()) ->
c_1(f^#(.(b(), c()), d'()), f^#(.(b'(), c()), d'()))}
We consider the following Problem:
Weak Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Application of 'simpDPRHS >>> ...':
-----------------------------------
No rule was simplified
We apply the transformation 'usablerules' on the resulting sub-problems:
Sub-problem 1:
--------------
We consider the problem
Weak Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: innermost
The input problem is not a DP-problem.
We abort the transformation and continue with the subprocessor on the problem
Weak Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: innermost
1) We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
All strict components are empty, nothing to further orient
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Weak Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: innermost
We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
All strict components are empty, nothing to further orient
We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
Weak Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: innermost
All strict components are empty, nothing to further orient
We abort the transformation and continue with the subprocessor on the problem
Weak Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: innermost
1) No dependency-pair could be removed
We apply the transformation 'weightgap of dimension Nat 2, maximal degree 1, cbits 4 <> ...' on the resulting sub-problems:
Sub-problem 1:
--------------
We consider the problem
Weak Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: innermost
We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
All strict components are empty, nothing to further orient
We try instead 'weightgap of dimension Nat 3, maximal degree 3, cbits 4 <> ...' on the problem
Weak Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: innermost
We fail transforming the problem using 'weightgap of dimension Nat 3, maximal degree 3, cbits 4'
All strict components are empty, nothing to further orient
We try instead 'weightgap of dimension Nat 4, maximal degree 3, cbits 4' on the problem
Weak Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: innermost
All strict components are empty, nothing to further orient
We abort the transformation and continue with the subprocessor on the problem
Weak Trs:
{ f(g(i(a(), b(), b'()), c()), d()) ->
if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'()))
, f(g(h(a(), b()), c()), d()) ->
if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'()))}
StartTerms: basic terms
Strategy: innermost
1) 'empty' succeeded:
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(1))