Inference procedure has parameters:
Ice fuel: 200
Timeout: 60s
Convolution: right


Learning problem is:

env: {
elt -> {a, b}  ;  elt_bin_tree -> {leaf, node}  ;  nat -> {s, z}
}
definition:
{
(leq, P:
{() -> leq([z, n2])
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)])
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2])
(leq([s(nn1), z])) -> BOT}
)
(plus, F:
{() -> plus([n, z, n])
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)])}
(plus([_mi, _ni, _oi]) /\ plus([_mi, _ni, _pi])) -> eq_nat([_oi, _pi])
)
(numnodes, F:
{() -> numnodes([leaf, z])
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)])}
(numnodes([_ti, _ui]) /\ numnodes([_ti, _vi])) -> eq_nat([_ui, _vi])
)
(member, P:
{() -> member([e2, node(e2, t1, t2)])
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)])
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)])
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2])
(member([e, leaf])) -> BOT}
)
}

properties:
{(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi])}


over-approximation: {member, numnodes, plus}
under-approximation: {leq}

Clause system for inference is:

{
() -> leq([z, n2]) -> 0
() -> member([e2, node(e2, t1, t2)]) -> 0
() -> numnodes([leaf, z]) -> 0
() -> plus([n, z, n]) -> 0
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 0
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 0
(leq([s(nn1), z])) -> BOT -> 0
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 0
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 0
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 0
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 0
(member([e, leaf])) -> BOT -> 0
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 0
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 0
}


Solving took 60.000870 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
leq -> 
{{{
Q={q_gen_1911, q_gen_1926, q_gen_1933, q_gen_1934, q_gen_1948, q_gen_1949, q_gen_1950},
Q_f={},
Delta=
{
<z>() -> q_gen_1934
<s>(q_gen_1934) -> q_gen_1950
<z, z>() -> q_gen_1911
<s, s>(q_gen_1911) -> q_gen_1926
<z, s>(q_gen_1934) -> q_gen_1933
<s, s>(q_gen_1949) -> q_gen_1948
<z, s>(q_gen_1950) -> q_gen_1949
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1917, q_gen_1918, q_gen_1919, q_gen_1920, q_gen_1921, q_gen_1922, q_gen_1923, q_gen_1924, q_gen_1925, q_gen_1927, q_gen_1928, q_gen_1929, q_gen_1932, q_gen_1941, q_gen_1942, q_gen_1943, q_gen_1944, q_gen_1945, q_gen_1951, q_gen_1952, q_gen_1958, q_gen_1959, q_gen_1960, q_gen_1961, q_gen_1962, q_gen_1963, q_gen_1964, q_gen_1972, q_gen_1973, q_gen_1974, q_gen_1975, q_gen_1976, q_gen_1977, q_gen_1978, q_gen_1979, q_gen_1980, q_gen_1981, q_gen_1982, q_gen_1985, q_gen_1986, q_gen_1987},
Q_f={},
Delta=
{
<leaf>() -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1922, q_gen_1920, q_gen_1919) -> q_gen_1918
<node>(q_gen_1910, q_gen_1909, q_gen_1920) -> q_gen_1919
<node>(q_gen_1910, q_gen_1921, q_gen_1909) -> q_gen_1920
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1921
<a>() -> q_gen_1922
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1924
<node>(q_gen_1910, q_gen_1919, q_gen_1918) -> q_gen_1925
<node>(q_gen_1922, q_gen_1921, q_gen_1909) -> q_gen_1943
<node>(q_gen_1910, q_gen_1909, q_gen_1921) -> q_gen_1945
<node>(q_gen_1910, q_gen_1921, q_gen_1945) -> q_gen_1960
<node>(q_gen_1922, q_gen_1924, q_gen_1909) -> q_gen_1963
<node>(q_gen_1910, q_gen_1921, q_gen_1921) -> q_gen_1973
<node>(q_gen_1910, q_gen_1973, q_gen_1973) -> q_gen_1975
<node>(q_gen_1910, q_gen_1973, q_gen_1921) -> q_gen_1977
<node>(q_gen_1922, q_gen_1945, q_gen_1945) -> q_gen_1981
<node>(q_gen_1910, q_gen_1945, q_gen_1921) -> q_gen_1987
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1919, q_gen_1918) -> q_gen_1917
<b, node>(q_gen_1922, q_gen_1925, q_gen_1924) -> q_gen_1923
<b, leaf>() -> q_gen_1927
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1928
<b, node>(q_gen_1922, q_gen_1924, q_gen_1909) -> q_gen_1929
<a, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1932
<b, node>(q_gen_1922, q_gen_1921, q_gen_1909) -> q_gen_1941
<b, node>(q_gen_1922, q_gen_1909, q_gen_1943) -> q_gen_1942
<b, node>(q_gen_1922, q_gen_1909, q_gen_1945) -> q_gen_1944
<b, node>(q_gen_1922, q_gen_1924, q_gen_1924) -> q_gen_1951
<b, node>(q_gen_1910, q_gen_1924, q_gen_1924) -> q_gen_1952
<b, node>(q_gen_1922, q_gen_1909, q_gen_1924) -> q_gen_1958
<b, node>(q_gen_1922, q_gen_1960, q_gen_1921) -> q_gen_1959
<b, node>(q_gen_1910, q_gen_1921, q_gen_1945) -> q_gen_1961
<b, node>(q_gen_1922, q_gen_1963, q_gen_1909) -> q_gen_1962
<b, node>(q_gen_1910, q_gen_1909, q_gen_1924) -> q_gen_1964
<b, node>(q_gen_1910, q_gen_1973, q_gen_1973) -> q_gen_1972
<b, node>(q_gen_1922, q_gen_1921, q_gen_1975) -> q_gen_1974
<b, node>(q_gen_1922, q_gen_1977, q_gen_1977) -> q_gen_1976
<b, node>(q_gen_1910, q_gen_1973, q_gen_1921) -> q_gen_1978
<b, node>(q_gen_1922, q_gen_1945, q_gen_1945) -> q_gen_1979
<b, node>(q_gen_1922, q_gen_1981, q_gen_1909) -> q_gen_1980
<b, node>(q_gen_1910, q_gen_1924, q_gen_1909) -> q_gen_1982
<b, node>(q_gen_1910, q_gen_1945, q_gen_1921) -> q_gen_1985
<b, node>(q_gen_1922, q_gen_1921, q_gen_1987) -> q_gen_1986
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1914, q_gen_1915, q_gen_1916, q_gen_1939, q_gen_1940, q_gen_1946, q_gen_1947, q_gen_1955, q_gen_1956, q_gen_1957, q_gen_1969, q_gen_1970, q_gen_1971, q_gen_1983, q_gen_1984},
Q_f={},
Delta=
{
<leaf>() -> q_gen_1915
<b>() -> q_gen_1916
<a>() -> q_gen_1940
<z>() -> q_gen_1957
<s>(q_gen_1957) -> q_gen_1971
<node>(q_gen_1916, q_gen_1915, q_gen_1915) -> q_gen_1984
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1914
<node, s>(q_gen_1940, q_gen_1915, q_gen_1907) -> q_gen_1939
<node, s>(q_gen_1940, q_gen_1915, q_gen_1947) -> q_gen_1946
<node, s>(q_gen_1916, q_gen_1915, q_gen_1939) -> q_gen_1947
<node, s>(q_gen_1916, q_gen_1915, q_gen_1956) -> q_gen_1955
<leaf, s>(q_gen_1957) -> q_gen_1956
<node, s>(q_gen_1916, q_gen_1915, q_gen_1970) -> q_gen_1969
<leaf, s>(q_gen_1971) -> q_gen_1970
<node, s>(q_gen_1916, q_gen_1984, q_gen_1956) -> q_gen_1983
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1912, q_gen_1913, q_gen_1930, q_gen_1931, q_gen_1935, q_gen_1936, q_gen_1937, q_gen_1938, q_gen_1953, q_gen_1954, q_gen_1965, q_gen_1966, q_gen_1967, q_gen_1968},
Q_f={},
Delta=
{
<z>() -> q_gen_1938
<s>(q_gen_1938) -> q_gen_1968
<z, z>() -> q_gen_1913
<s, s>(q_gen_1913) -> q_gen_1931
<z, s>(q_gen_1938) -> q_gen_1954
<z, z, z>() -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1912
<s, z, s>(q_gen_1931) -> q_gen_1930
<s, z, s>(q_gen_1913) -> q_gen_1935
<s, s, s>(q_gen_1937) -> q_gen_1936
<z, z, s>(q_gen_1938) -> q_gen_1937
<z, s, s>(q_gen_1954) -> q_gen_1953
<s, z, s>(q_gen_1954) -> q_gen_1965
<s, s, s>(q_gen_1967) -> q_gen_1966
<z, z, s>(q_gen_1968) -> q_gen_1967
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004991 s (model generation: 0.004581,  model checking: 0.000410):

Model:
|_
{
leq -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 0
() -> member([e2, node(e2, t1, t2)]) -> 0
() -> numnodes([leaf, z]) -> 0
() -> plus([n, z, n]) -> 3
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 1
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 1
(member([e, leaf])) -> BOT -> 1
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 1
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 1
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.003986 s (model generation: 0.003859,  model checking: 0.000127):

Model:
|_
{
leq -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906},
Q_f={q_gen_1906},
Delta=
{
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 0
() -> member([e2, node(e2, t1, t2)]) -> 0
() -> numnodes([leaf, z]) -> 3
() -> plus([n, z, n]) -> 3
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 1
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 1
(member([e, leaf])) -> BOT -> 1
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 1
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 1
}
Sat witness: Found: (() -> numnodes([leaf, z]), {

})

-------------------------------------------
Step 2, which took 0.004327 s (model generation: 0.004261,  model checking: 0.000066):

Model:
|_
{
leq -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907},
Q_f={q_gen_1907},
Delta=
{
<leaf, z>() -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906},
Q_f={q_gen_1906},
Delta=
{
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 0
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> numnodes([leaf, z]) -> 3
() -> plus([n, z, n]) -> 3
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 1
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 1
(member([e, leaf])) -> BOT -> 1
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 1
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 1
}
Sat witness: Found: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 3, which took 0.003857 s (model generation: 0.003806,  model checking: 0.000051):

Model:
|_
{
leq -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<b>() -> q_gen_1910
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907},
Q_f={q_gen_1907},
Delta=
{
<leaf, z>() -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906},
Q_f={q_gen_1906},
Delta=
{
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 3
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> numnodes([leaf, z]) -> 3
() -> plus([n, z, n]) -> 3
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 1
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 1
(member([e, leaf])) -> BOT -> 1
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 1
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 1
}
Sat witness: Found: (() -> leq([z, n2]), {
n2 -> z
})

-------------------------------------------
Step 4, which took 0.005498 s (model generation: 0.005396,  model checking: 0.000102):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911},
Q_f={q_gen_1911},
Delta=
{
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<b>() -> q_gen_1910
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907},
Q_f={q_gen_1907},
Delta=
{
<leaf, z>() -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906},
Q_f={q_gen_1906},
Delta=
{
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 3
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> numnodes([leaf, z]) -> 3
() -> plus([n, z, n]) -> 3
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 1
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 1
(member([e, leaf])) -> BOT -> 1
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 1
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 4
}
Sat witness: Found: ((plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]), {
_li -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 5, which took 0.007738 s (model generation: 0.007536,  model checking: 0.000202):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911},
Q_f={q_gen_1911},
Delta=
{
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<b>() -> q_gen_1910
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907},
Q_f={q_gen_1907},
Delta=
{
<leaf, z>() -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913},
Q_f={q_gen_1906},
Delta=
{
<z, z>() -> q_gen_1913
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 3
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> numnodes([leaf, z]) -> 3
() -> plus([n, z, n]) -> 3
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 1
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 1
(member([e, leaf])) -> BOT -> 1
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 4
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 4
}
Sat witness: Found: ((numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]), {
_qi -> z  ;  _ri -> z  ;  _si -> z  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 6, which took 0.117915 s (model generation: 0.010604,  model checking: 0.107311):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911},
Q_f={q_gen_1911},
Delta=
{
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<b>() -> q_gen_1910
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<b>() -> q_gen_1916
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913},
Q_f={q_gen_1906},
Delta=
{
<z, z>() -> q_gen_1913
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 3
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> numnodes([leaf, z]) -> 3
() -> plus([n, z, n]) -> 3
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 1
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 1
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 4
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 2
(member([e, leaf])) -> BOT -> 2
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 4
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 4
}
Sat witness: Found: ((not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> b  ;  e2 -> a  ;  t1 -> node(b, node(b, leaf, node(b, node(a, leaf, leaf), leaf)), node(a, node(b, node(a, leaf, leaf), leaf), node(b, leaf, node(b, node(a, leaf, leaf), leaf))))  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 7, which took 0.006987 s (model generation: 0.006576,  model checking: 0.000411):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911},
Q_f={q_gen_1911},
Delta=
{
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1909
<a>() -> q_gen_1910
<b>() -> q_gen_1910
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<b>() -> q_gen_1916
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913},
Q_f={q_gen_1906},
Delta=
{
<z, z>() -> q_gen_1913
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 3
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> numnodes([leaf, z]) -> 3
() -> plus([n, z, n]) -> 3
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 4
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 2
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 4
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 2
(member([e, leaf])) -> BOT -> 2
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 4
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 4
}
Sat witness: Found: ((member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]), {
_wi -> s(z)  ;  e -> b  ;  t1 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 8, which took 0.006950 s (model generation: 0.006392,  model checking: 0.000558):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911},
Q_f={q_gen_1911},
Delta=
{
<s, s>(q_gen_1911) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1909
<a>() -> q_gen_1910
<b>() -> q_gen_1910
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<b>() -> q_gen_1916
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913},
Q_f={q_gen_1906},
Delta=
{
<z, z>() -> q_gen_1913
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 3
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> numnodes([leaf, z]) -> 3
() -> plus([n, z, n]) -> 3
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 2
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2
(leq([s(nn1), z])) -> BOT -> 2
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 4
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 2
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 4
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 5
(member([e, leaf])) -> BOT -> 3
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 4
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 4
}
Sat witness: Found: ((not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]), {
e -> b  ;  e2 -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 9, which took 0.006969 s (model generation: 0.006763,  model checking: 0.000206):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911},
Q_f={q_gen_1911},
Delta=
{
<s, s>(q_gen_1911) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1909
<a>() -> q_gen_1910
<b>() -> q_gen_1910
<b, leaf>() -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<b>() -> q_gen_1916
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913},
Q_f={q_gen_1906},
Delta=
{
<z, z>() -> q_gen_1913
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 3
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> numnodes([leaf, z]) -> 3
() -> plus([n, z, n]) -> 3
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 3
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 3
(leq([s(nn1), z])) -> BOT -> 3
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 4
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 3
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 4
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 5
(member([e, leaf])) -> BOT -> 6
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 4
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 4
}
Sat witness: Found: ((member([e, leaf])) -> BOT, {
e -> b
})

-------------------------------------------
Step 10, which took 0.010098 s (model generation: 0.009490,  model checking: 0.000608):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911},
Q_f={q_gen_1911},
Delta=
{
<s, s>(q_gen_1911) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1922, q_gen_1923},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1909
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1909
<b>() -> q_gen_1910
<a>() -> q_gen_1922
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, leaf>() -> q_gen_1923
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1923
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<b>() -> q_gen_1916
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913},
Q_f={q_gen_1906},
Delta=
{
<z, z>() -> q_gen_1913
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 3
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> numnodes([leaf, z]) -> 3
() -> plus([n, z, n]) -> 3
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 3
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 3
(leq([s(nn1), z])) -> BOT -> 3
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 4
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 6
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 4
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 5
(member([e, leaf])) -> BOT -> 6
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 4
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 4
}
Sat witness: Found: ((member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> b  ;  e2 -> a  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 11, which took 0.014145 s (model generation: 0.013500,  model checking: 0.000645):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911},
Q_f={q_gen_1911},
Delta=
{
<s, s>(q_gen_1911) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1918, q_gen_1922, q_gen_1927},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1918
<node>(q_gen_1910, q_gen_1909, q_gen_1918) -> q_gen_1918
<node>(q_gen_1910, q_gen_1918, q_gen_1909) -> q_gen_1918
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1918
<node>(q_gen_1922, q_gen_1918, q_gen_1918) -> q_gen_1918
<a>() -> q_gen_1922
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1909, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1918, q_gen_1909) -> q_gen_1908
<b, leaf>() -> q_gen_1927
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1927
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<b>() -> q_gen_1916
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913},
Q_f={q_gen_1906},
Delta=
{
<z, z>() -> q_gen_1913
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 3
() -> member([e2, node(e2, t1, t2)]) -> 3
() -> numnodes([leaf, z]) -> 3
() -> plus([n, z, n]) -> 6
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4
(leq([s(nn1), z])) -> BOT -> 4
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 4
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 6
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 4
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 5
(member([e, leaf])) -> BOT -> 6
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 4
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 4
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 12, which took 0.015431 s (model generation: 0.013445,  model checking: 0.001986):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911},
Q_f={q_gen_1911},
Delta=
{
<s, s>(q_gen_1911) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1918, q_gen_1922, q_gen_1927},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1918
<node>(q_gen_1910, q_gen_1909, q_gen_1918) -> q_gen_1918
<node>(q_gen_1910, q_gen_1918, q_gen_1909) -> q_gen_1918
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1918
<node>(q_gen_1922, q_gen_1918, q_gen_1918) -> q_gen_1918
<a>() -> q_gen_1922
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1909, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1918, q_gen_1909) -> q_gen_1908
<b, leaf>() -> q_gen_1927
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1927
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<b>() -> q_gen_1916
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913},
Q_f={q_gen_1906},
Delta=
{
<s, s>(q_gen_1913) -> q_gen_1913
<z, z>() -> q_gen_1913
<s, z, s>(q_gen_1913) -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 3
() -> member([e2, node(e2, t1, t2)]) -> 6
() -> numnodes([leaf, z]) -> 4
() -> plus([n, z, n]) -> 6
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4
(leq([s(nn1), z])) -> BOT -> 4
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 4
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 6
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 4
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 5
(member([e, leaf])) -> BOT -> 6
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 4
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 4
}
Sat witness: Found: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 13, which took 0.018006 s (model generation: 0.017869,  model checking: 0.000137):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911},
Q_f={q_gen_1911},
Delta=
{
<s, s>(q_gen_1911) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1918, q_gen_1922, q_gen_1927},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1918
<node>(q_gen_1910, q_gen_1909, q_gen_1918) -> q_gen_1918
<node>(q_gen_1910, q_gen_1918, q_gen_1909) -> q_gen_1918
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1918
<node>(q_gen_1922, q_gen_1918, q_gen_1918) -> q_gen_1918
<a>() -> q_gen_1922
<a, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1909, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1918, q_gen_1909) -> q_gen_1908
<b, leaf>() -> q_gen_1927
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1927
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<b>() -> q_gen_1916
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913},
Q_f={q_gen_1906},
Delta=
{
<s, s>(q_gen_1913) -> q_gen_1913
<z, z>() -> q_gen_1913
<s, z, s>(q_gen_1913) -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 6
() -> member([e2, node(e2, t1, t2)]) -> 6
() -> numnodes([leaf, z]) -> 4
() -> plus([n, z, n]) -> 6
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4
(leq([s(nn1), z])) -> BOT -> 4
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 4
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 6
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 4
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 5
(member([e, leaf])) -> BOT -> 6
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 4
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 4
}
Sat witness: Found: (() -> leq([z, n2]), {
n2 -> s(z)
})

-------------------------------------------
Step 14, which took 0.017833 s (model generation: 0.017522,  model checking: 0.000311):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911, q_gen_1934},
Q_f={q_gen_1911},
Delta=
{
<z>() -> q_gen_1934
<s, s>(q_gen_1911) -> q_gen_1911
<z, s>(q_gen_1934) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1918, q_gen_1922, q_gen_1927},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1918
<node>(q_gen_1910, q_gen_1909, q_gen_1918) -> q_gen_1918
<node>(q_gen_1910, q_gen_1918, q_gen_1909) -> q_gen_1918
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1918
<node>(q_gen_1922, q_gen_1918, q_gen_1918) -> q_gen_1918
<a>() -> q_gen_1922
<a, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1909, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1918, q_gen_1909) -> q_gen_1908
<b, leaf>() -> q_gen_1927
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1927
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<b>() -> q_gen_1916
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913},
Q_f={q_gen_1906},
Delta=
{
<s, s>(q_gen_1913) -> q_gen_1913
<z, z>() -> q_gen_1913
<s, z, s>(q_gen_1913) -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 6
() -> member([e2, node(e2, t1, t2)]) -> 6
() -> numnodes([leaf, z]) -> 4
() -> plus([n, z, n]) -> 6
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4
(leq([s(nn1), z])) -> BOT -> 4
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 4
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 6
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 4
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 5
(member([e, leaf])) -> BOT -> 6
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 4
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 7
}
Sat witness: Found: ((plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]), {
_li -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 15, which took 0.020924 s (model generation: 0.018915,  model checking: 0.002009):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911, q_gen_1934},
Q_f={q_gen_1911},
Delta=
{
<z>() -> q_gen_1934
<s, s>(q_gen_1911) -> q_gen_1911
<z, s>(q_gen_1934) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1920, q_gen_1922, q_gen_1927},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1909, q_gen_1920) -> q_gen_1909
<node>(q_gen_1922, q_gen_1920, q_gen_1909) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1920
<node>(q_gen_1910, q_gen_1920, q_gen_1909) -> q_gen_1920
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1920
<a>() -> q_gen_1922
<a, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1920, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1920, q_gen_1920) -> q_gen_1908
<b, leaf>() -> q_gen_1927
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1927
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<b>() -> q_gen_1916
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913, q_gen_1938},
Q_f={q_gen_1906},
Delta=
{
<z>() -> q_gen_1938
<s, s>(q_gen_1913) -> q_gen_1913
<z, z>() -> q_gen_1913
<s, s, s>(q_gen_1906) -> q_gen_1906
<s, z, s>(q_gen_1913) -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, s>(q_gen_1938) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 6
() -> member([e2, node(e2, t1, t2)]) -> 6
() -> numnodes([leaf, z]) -> 4
() -> plus([n, z, n]) -> 6
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4
(leq([s(nn1), z])) -> BOT -> 4
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 4
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 6
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 4
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 5
(member([e, leaf])) -> BOT -> 6
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 7
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 7
}
Sat witness: Found: ((numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]), {
_qi -> z  ;  _ri -> z  ;  _si -> z  ;  e -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 16, which took 0.039258 s (model generation: 0.019413,  model checking: 0.019845):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911, q_gen_1934},
Q_f={q_gen_1911},
Delta=
{
<z>() -> q_gen_1934
<s, s>(q_gen_1911) -> q_gen_1911
<z, s>(q_gen_1934) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1920, q_gen_1922, q_gen_1927},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1909, q_gen_1920) -> q_gen_1909
<node>(q_gen_1922, q_gen_1920, q_gen_1909) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1920
<node>(q_gen_1910, q_gen_1920, q_gen_1909) -> q_gen_1920
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1920
<a>() -> q_gen_1922
<a, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1920, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1920, q_gen_1920) -> q_gen_1908
<b, leaf>() -> q_gen_1927
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1927
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<a>() -> q_gen_1916
<b>() -> q_gen_1916
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913, q_gen_1938},
Q_f={q_gen_1906},
Delta=
{
<z>() -> q_gen_1938
<s, s>(q_gen_1913) -> q_gen_1913
<z, z>() -> q_gen_1913
<s, s, s>(q_gen_1906) -> q_gen_1906
<s, z, s>(q_gen_1913) -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, s>(q_gen_1938) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 6
() -> member([e2, node(e2, t1, t2)]) -> 6
() -> numnodes([leaf, z]) -> 4
() -> plus([n, z, n]) -> 6
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4
(leq([s(nn1), z])) -> BOT -> 4
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 4
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 6
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 7
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 5
(member([e, leaf])) -> BOT -> 6
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 7
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 7
}
Sat witness: Found: ((not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> b  ;  e2 -> a  ;  t1 -> leaf  ;  t2 -> node(a, node(a, leaf, leaf), leaf)
})

-------------------------------------------
Step 17, which took 0.025807 s (model generation: 0.024104,  model checking: 0.001703):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911, q_gen_1934},
Q_f={q_gen_1911},
Delta=
{
<z>() -> q_gen_1934
<s, s>(q_gen_1911) -> q_gen_1911
<z, s>(q_gen_1934) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1918, q_gen_1922, q_gen_1927},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1918
<node>(q_gen_1910, q_gen_1909, q_gen_1918) -> q_gen_1918
<node>(q_gen_1910, q_gen_1918, q_gen_1909) -> q_gen_1918
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1918
<node>(q_gen_1922, q_gen_1918, q_gen_1909) -> q_gen_1918
<node>(q_gen_1922, q_gen_1918, q_gen_1918) -> q_gen_1918
<a>() -> q_gen_1922
<a, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1909, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1918, q_gen_1909) -> q_gen_1908
<b, leaf>() -> q_gen_1927
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1927
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<a>() -> q_gen_1916
<b>() -> q_gen_1916
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913, q_gen_1938},
Q_f={q_gen_1906},
Delta=
{
<z>() -> q_gen_1938
<s, s>(q_gen_1913) -> q_gen_1913
<z, z>() -> q_gen_1913
<s, s, s>(q_gen_1906) -> q_gen_1906
<s, z, s>(q_gen_1913) -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, s>(q_gen_1938) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 6
() -> member([e2, node(e2, t1, t2)]) -> 6
() -> numnodes([leaf, z]) -> 4
() -> plus([n, z, n]) -> 6
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4
(leq([s(nn1), z])) -> BOT -> 4
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 7
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 6
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 7
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 5
(member([e, leaf])) -> BOT -> 6
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 7
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 7
}
Sat witness: Found: ((member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]), {
_wi -> s(s(s(z)))  ;  e -> b  ;  t1 -> node(a, leaf, node(b, leaf, node(a, leaf, leaf)))
})

-------------------------------------------
Step 18, which took 0.032492 s (model generation: 0.028068,  model checking: 0.004424):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911, q_gen_1934},
Q_f={q_gen_1911},
Delta=
{
<s>(q_gen_1934) -> q_gen_1934
<z>() -> q_gen_1934
<s, s>(q_gen_1911) -> q_gen_1911
<z, s>(q_gen_1934) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1918, q_gen_1922, q_gen_1927},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1918
<node>(q_gen_1910, q_gen_1909, q_gen_1918) -> q_gen_1918
<node>(q_gen_1910, q_gen_1918, q_gen_1909) -> q_gen_1918
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1918
<node>(q_gen_1922, q_gen_1918, q_gen_1909) -> q_gen_1918
<node>(q_gen_1922, q_gen_1918, q_gen_1918) -> q_gen_1918
<a>() -> q_gen_1922
<a, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1909, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1918, q_gen_1909) -> q_gen_1908
<b, leaf>() -> q_gen_1927
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1927
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<a>() -> q_gen_1916
<b>() -> q_gen_1916
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913, q_gen_1938},
Q_f={q_gen_1906},
Delta=
{
<z>() -> q_gen_1938
<s, s>(q_gen_1913) -> q_gen_1913
<z, z>() -> q_gen_1913
<s, s, s>(q_gen_1906) -> q_gen_1906
<s, z, s>(q_gen_1913) -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, s>(q_gen_1938) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 6
() -> member([e2, node(e2, t1, t2)]) -> 6
() -> numnodes([leaf, z]) -> 5
() -> plus([n, z, n]) -> 6
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5
(leq([s(nn1), z])) -> BOT -> 5
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 7
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 6
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 7
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 8
(member([e, leaf])) -> BOT -> 6
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 7
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 7
}
Sat witness: Found: ((not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]), {
e -> b  ;  e2 -> a  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 19, which took 0.029042 s (model generation: 0.026304,  model checking: 0.002738):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911, q_gen_1934},
Q_f={q_gen_1911},
Delta=
{
<s>(q_gen_1934) -> q_gen_1934
<z>() -> q_gen_1934
<s, s>(q_gen_1911) -> q_gen_1911
<z, s>(q_gen_1934) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1920, q_gen_1922, q_gen_1923},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1909, q_gen_1920) -> q_gen_1909
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1909
<node>(q_gen_1922, q_gen_1920, q_gen_1909) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1920
<a>() -> q_gen_1922
<a, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1909, q_gen_1920) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1920, q_gen_1909) -> q_gen_1908
<b, leaf>() -> q_gen_1923
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1923
<b, node>(q_gen_1922, q_gen_1920, q_gen_1920) -> q_gen_1923
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<a>() -> q_gen_1916
<b>() -> q_gen_1916
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913, q_gen_1938},
Q_f={q_gen_1906},
Delta=
{
<z>() -> q_gen_1938
<s, s>(q_gen_1913) -> q_gen_1913
<z, z>() -> q_gen_1913
<s, s, s>(q_gen_1906) -> q_gen_1906
<s, z, s>(q_gen_1913) -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, s>(q_gen_1938) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 6
() -> member([e2, node(e2, t1, t2)]) -> 6
() -> numnodes([leaf, z]) -> 6
() -> plus([n, z, n]) -> 6
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 6
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 6
(leq([s(nn1), z])) -> BOT -> 6
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 7
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 9
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 7
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 8
(member([e, leaf])) -> BOT -> 7
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 7
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 7
}
Sat witness: Found: ((member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> b  ;  e2 -> a  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 20, which took 0.030857 s (model generation: 0.028583,  model checking: 0.002274):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911, q_gen_1934},
Q_f={q_gen_1911},
Delta=
{
<s>(q_gen_1934) -> q_gen_1934
<z>() -> q_gen_1934
<s, s>(q_gen_1911) -> q_gen_1911
<z, s>(q_gen_1934) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1919, q_gen_1922, q_gen_1923},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1919, q_gen_1909) -> q_gen_1909
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1909
<node>(q_gen_1922, q_gen_1919, q_gen_1919) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1919
<node>(q_gen_1910, q_gen_1909, q_gen_1919) -> q_gen_1919
<a>() -> q_gen_1922
<a, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1919, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1919, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1919, q_gen_1919) -> q_gen_1908
<b, leaf>() -> q_gen_1923
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1923
<b, node>(q_gen_1922, q_gen_1909, q_gen_1919) -> q_gen_1923
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<a>() -> q_gen_1916
<b>() -> q_gen_1916
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913, q_gen_1938},
Q_f={q_gen_1906},
Delta=
{
<z>() -> q_gen_1938
<s, s>(q_gen_1913) -> q_gen_1913
<z, z>() -> q_gen_1913
<s, s, s>(q_gen_1906) -> q_gen_1906
<s, z, s>(q_gen_1913) -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, s>(q_gen_1938) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 6
() -> member([e2, node(e2, t1, t2)]) -> 9
() -> numnodes([leaf, z]) -> 7
() -> plus([n, z, n]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 7
(leq([s(nn1), z])) -> BOT -> 7
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 7
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 9
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 7
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 8
(member([e, leaf])) -> BOT -> 7
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 7
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 7
}
Sat witness: Found: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 21, which took 0.030412 s (model generation: 0.029975,  model checking: 0.000437):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911, q_gen_1934},
Q_f={q_gen_1911},
Delta=
{
<s>(q_gen_1934) -> q_gen_1934
<z>() -> q_gen_1934
<s, s>(q_gen_1911) -> q_gen_1911
<z, s>(q_gen_1934) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1919, q_gen_1922, q_gen_1923},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1919, q_gen_1909) -> q_gen_1909
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1909
<node>(q_gen_1922, q_gen_1919, q_gen_1919) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1919
<node>(q_gen_1910, q_gen_1909, q_gen_1919) -> q_gen_1919
<a>() -> q_gen_1922
<a, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1919, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1919, q_gen_1919) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1919, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1919, q_gen_1919) -> q_gen_1908
<b, leaf>() -> q_gen_1923
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1923
<b, node>(q_gen_1922, q_gen_1909, q_gen_1919) -> q_gen_1923
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<a>() -> q_gen_1916
<b>() -> q_gen_1916
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913, q_gen_1938},
Q_f={q_gen_1906},
Delta=
{
<z>() -> q_gen_1938
<s, s>(q_gen_1913) -> q_gen_1913
<z, z>() -> q_gen_1913
<s, s, s>(q_gen_1906) -> q_gen_1906
<s, z, s>(q_gen_1913) -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, s>(q_gen_1938) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 7
() -> member([e2, node(e2, t1, t2)]) -> 9
() -> numnodes([leaf, z]) -> 7
() -> plus([n, z, n]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 7
(leq([s(nn1), z])) -> BOT -> 7
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 7
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 9
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 7
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 8
(member([e, leaf])) -> BOT -> 7
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 7
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 10
}
Sat witness: Found: ((plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]), {
_li -> s(z)  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 22, which took 0.032431 s (model generation: 0.030954,  model checking: 0.001477):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911, q_gen_1934},
Q_f={q_gen_1911},
Delta=
{
<s>(q_gen_1934) -> q_gen_1934
<z>() -> q_gen_1934
<s, s>(q_gen_1911) -> q_gen_1911
<z, s>(q_gen_1934) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1919, q_gen_1922, q_gen_1923},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1919, q_gen_1909) -> q_gen_1909
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1909
<node>(q_gen_1922, q_gen_1919, q_gen_1919) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1919
<node>(q_gen_1910, q_gen_1909, q_gen_1919) -> q_gen_1919
<a>() -> q_gen_1922
<a, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1919, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1919, q_gen_1919) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1919, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1919, q_gen_1919) -> q_gen_1908
<b, leaf>() -> q_gen_1923
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1923
<b, node>(q_gen_1922, q_gen_1909, q_gen_1919) -> q_gen_1923
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<a>() -> q_gen_1916
<b>() -> q_gen_1916
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913, q_gen_1938},
Q_f={q_gen_1906},
Delta=
{
<z>() -> q_gen_1938
<s, s>(q_gen_1913) -> q_gen_1913
<z, s>(q_gen_1938) -> q_gen_1913
<z, z>() -> q_gen_1913
<s, s, s>(q_gen_1906) -> q_gen_1906
<s, z, s>(q_gen_1913) -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, s>(q_gen_1938) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 7
() -> member([e2, node(e2, t1, t2)]) -> 9
() -> numnodes([leaf, z]) -> 7
() -> plus([n, z, n]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 7
(leq([s(nn1), z])) -> BOT -> 7
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 7
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 9
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 7
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 8
(member([e, leaf])) -> BOT -> 7
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 10
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 10
}
Sat witness: Found: ((numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]), {
_qi -> z  ;  _ri -> z  ;  _si -> s(z)  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 23, which took 0.043583 s (model generation: 0.032252,  model checking: 0.011331):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911, q_gen_1934},
Q_f={q_gen_1911},
Delta=
{
<s>(q_gen_1934) -> q_gen_1934
<z>() -> q_gen_1934
<s, s>(q_gen_1911) -> q_gen_1911
<z, s>(q_gen_1934) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1919, q_gen_1922, q_gen_1923},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1919, q_gen_1909) -> q_gen_1909
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1909
<node>(q_gen_1922, q_gen_1919, q_gen_1919) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1919
<node>(q_gen_1910, q_gen_1909, q_gen_1919) -> q_gen_1919
<a>() -> q_gen_1922
<a, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1919, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1919, q_gen_1919) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1919, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1919, q_gen_1919) -> q_gen_1908
<b, leaf>() -> q_gen_1923
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1923
<b, node>(q_gen_1922, q_gen_1909, q_gen_1919) -> q_gen_1923
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916, q_gen_1957},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<a>() -> q_gen_1916
<b>() -> q_gen_1916
<z>() -> q_gen_1957
<leaf, s>(q_gen_1957) -> q_gen_1907
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913, q_gen_1938},
Q_f={q_gen_1906},
Delta=
{
<z>() -> q_gen_1938
<s, s>(q_gen_1913) -> q_gen_1913
<z, s>(q_gen_1938) -> q_gen_1913
<z, z>() -> q_gen_1913
<s, s, s>(q_gen_1906) -> q_gen_1906
<s, z, s>(q_gen_1913) -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, s>(q_gen_1938) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 7
() -> member([e2, node(e2, t1, t2)]) -> 9
() -> numnodes([leaf, z]) -> 7
() -> plus([n, z, n]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 7
(leq([s(nn1), z])) -> BOT -> 7
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 7
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 9
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 10
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 8
(member([e, leaf])) -> BOT -> 8
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 10
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 10
}
Sat witness: Found: ((not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> b  ;  e2 -> a  ;  t1 -> leaf  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 24, which took 0.098074 s (model generation: 0.034290,  model checking: 0.063784):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911, q_gen_1934},
Q_f={q_gen_1911},
Delta=
{
<s>(q_gen_1934) -> q_gen_1934
<z>() -> q_gen_1934
<s, s>(q_gen_1911) -> q_gen_1911
<z, s>(q_gen_1934) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1917, q_gen_1919, q_gen_1922},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1919, q_gen_1909) -> q_gen_1909
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1909
<node>(q_gen_1922, q_gen_1919, q_gen_1919) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1919
<node>(q_gen_1910, q_gen_1909, q_gen_1919) -> q_gen_1919
<a>() -> q_gen_1922
<a, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1919, q_gen_1919) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1909, q_gen_1919) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1919, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1919, q_gen_1919) -> q_gen_1908
<b, leaf>() -> q_gen_1917
<b, node>(q_gen_1910, q_gen_1919, q_gen_1909) -> q_gen_1917
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1917
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916, q_gen_1957},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<a>() -> q_gen_1916
<b>() -> q_gen_1916
<z>() -> q_gen_1957
<leaf, s>(q_gen_1957) -> q_gen_1907
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913, q_gen_1938},
Q_f={q_gen_1906},
Delta=
{
<z>() -> q_gen_1938
<s, s>(q_gen_1913) -> q_gen_1913
<z, s>(q_gen_1938) -> q_gen_1913
<z, z>() -> q_gen_1913
<s, s, s>(q_gen_1906) -> q_gen_1906
<s, z, s>(q_gen_1913) -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, s>(q_gen_1938) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 8
() -> member([e2, node(e2, t1, t2)]) -> 9
() -> numnodes([leaf, z]) -> 8
() -> plus([n, z, n]) -> 8
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 8
(leq([s(nn1), z])) -> BOT -> 8
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 8
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 9
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 10
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 11
(member([e, leaf])) -> BOT -> 9
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 10
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 10
}
Sat witness: Found: ((not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]), {
e -> b  ;  e2 -> a  ;  t1 -> node(b, node(a, leaf, leaf), node(b, leaf, node(a, leaf, leaf)))  ;  t2 -> node(a, leaf, leaf)
})

-------------------------------------------
Step 25, which took 0.045758 s (model generation: 0.040571,  model checking: 0.005187):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911, q_gen_1934},
Q_f={q_gen_1911},
Delta=
{
<s>(q_gen_1934) -> q_gen_1934
<z>() -> q_gen_1934
<s, s>(q_gen_1911) -> q_gen_1911
<z, s>(q_gen_1934) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1920, q_gen_1922, q_gen_1927},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1909, q_gen_1920) -> q_gen_1909
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1909
<node>(q_gen_1922, q_gen_1920, q_gen_1909) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1920
<a>() -> q_gen_1922
<a, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1920, q_gen_1920) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1909, q_gen_1920) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1920, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1920, q_gen_1920) -> q_gen_1908
<b, leaf>() -> q_gen_1927
<b, node>(q_gen_1910, q_gen_1909, q_gen_1920) -> q_gen_1927
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1927
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916, q_gen_1957},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<a>() -> q_gen_1916
<b>() -> q_gen_1916
<z>() -> q_gen_1957
<leaf, s>(q_gen_1957) -> q_gen_1907
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913, q_gen_1938},
Q_f={q_gen_1906},
Delta=
{
<z>() -> q_gen_1938
<s, s>(q_gen_1913) -> q_gen_1913
<z, s>(q_gen_1938) -> q_gen_1913
<z, z>() -> q_gen_1913
<s, s, s>(q_gen_1906) -> q_gen_1906
<s, z, s>(q_gen_1913) -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, s>(q_gen_1938) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 9
() -> member([e2, node(e2, t1, t2)]) -> 9
() -> numnodes([leaf, z]) -> 9
() -> plus([n, z, n]) -> 9
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 9
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 9
(leq([s(nn1), z])) -> BOT -> 9
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 9
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 12
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 10
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 11
(member([e, leaf])) -> BOT -> 10
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 10
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 10
}
Sat witness: Found: ((member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> b  ;  e2 -> a  ;  t1 -> node(a, node(b, leaf, leaf), leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 26, which took 0.020431 s (model generation: 0.019456,  model checking: 0.000975):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911, q_gen_1934},
Q_f={q_gen_1911},
Delta=
{
<s>(q_gen_1934) -> q_gen_1934
<z>() -> q_gen_1934
<s, s>(q_gen_1911) -> q_gen_1911
<z, s>(q_gen_1934) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1917, q_gen_1918, q_gen_1922},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1909, q_gen_1918) -> q_gen_1909
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1918
<node>(q_gen_1922, q_gen_1918, q_gen_1909) -> q_gen_1918
<a>() -> q_gen_1922
<a, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1909, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1918, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1918, q_gen_1918) -> q_gen_1908
<b, leaf>() -> q_gen_1917
<b, node>(q_gen_1910, q_gen_1909, q_gen_1918) -> q_gen_1917
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1917
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916, q_gen_1957},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<a>() -> q_gen_1916
<b>() -> q_gen_1916
<z>() -> q_gen_1957
<leaf, s>(q_gen_1957) -> q_gen_1907
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913, q_gen_1938},
Q_f={q_gen_1906},
Delta=
{
<z>() -> q_gen_1938
<s, s>(q_gen_1913) -> q_gen_1913
<z, s>(q_gen_1938) -> q_gen_1913
<z, z>() -> q_gen_1913
<s, s, s>(q_gen_1906) -> q_gen_1906
<s, z, s>(q_gen_1913) -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, s>(q_gen_1938) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 9
() -> member([e2, node(e2, t1, t2)]) -> 12
() -> numnodes([leaf, z]) -> 10
() -> plus([n, z, n]) -> 10
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10
(leq([s(nn1), z])) -> BOT -> 10
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 10
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 12
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 10
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 11
(member([e, leaf])) -> BOT -> 10
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 10
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 10
}
Sat witness: Found: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> b  ;  t1 -> leaf  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 27, which took 0.022557 s (model generation: 0.022056,  model checking: 0.000501):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911, q_gen_1934},
Q_f={q_gen_1911},
Delta=
{
<s>(q_gen_1934) -> q_gen_1934
<z>() -> q_gen_1934
<s, s>(q_gen_1911) -> q_gen_1911
<z, s>(q_gen_1934) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1918, q_gen_1922, q_gen_1927},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1909
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1918
<node>(q_gen_1910, q_gen_1909, q_gen_1918) -> q_gen_1918
<node>(q_gen_1922, q_gen_1918, q_gen_1909) -> q_gen_1918
<node>(q_gen_1922, q_gen_1918, q_gen_1918) -> q_gen_1918
<a>() -> q_gen_1922
<a, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1909, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1918, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1918, q_gen_1918) -> q_gen_1908
<b, leaf>() -> q_gen_1927
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1927
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916, q_gen_1957},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<a>() -> q_gen_1916
<b>() -> q_gen_1916
<z>() -> q_gen_1957
<leaf, s>(q_gen_1957) -> q_gen_1907
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913, q_gen_1938},
Q_f={q_gen_1906},
Delta=
{
<z>() -> q_gen_1938
<s, s>(q_gen_1913) -> q_gen_1913
<z, s>(q_gen_1938) -> q_gen_1913
<z, z>() -> q_gen_1913
<s, s, s>(q_gen_1906) -> q_gen_1906
<s, z, s>(q_gen_1913) -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, s>(q_gen_1938) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 10
() -> member([e2, node(e2, t1, t2)]) -> 12
() -> numnodes([leaf, z]) -> 10
() -> plus([n, z, n]) -> 10
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10
(leq([s(nn1), z])) -> BOT -> 10
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 10
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 12
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 10
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 11
(member([e, leaf])) -> BOT -> 10
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 10
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 13
}
Sat witness: Found: ((plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]), {
_li -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 28, which took 0.021349 s (model generation: 0.020282,  model checking: 0.001067):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911, q_gen_1934},
Q_f={q_gen_1911},
Delta=
{
<s>(q_gen_1934) -> q_gen_1934
<z>() -> q_gen_1934
<s, s>(q_gen_1911) -> q_gen_1911
<z, s>(q_gen_1934) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1918, q_gen_1922, q_gen_1927},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1909
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1918
<node>(q_gen_1910, q_gen_1909, q_gen_1918) -> q_gen_1918
<node>(q_gen_1922, q_gen_1918, q_gen_1909) -> q_gen_1918
<node>(q_gen_1922, q_gen_1918, q_gen_1918) -> q_gen_1918
<a>() -> q_gen_1922
<a, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1909, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1918, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1918, q_gen_1918) -> q_gen_1908
<b, leaf>() -> q_gen_1927
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1927
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916, q_gen_1957},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<a>() -> q_gen_1916
<b>() -> q_gen_1916
<z>() -> q_gen_1957
<leaf, s>(q_gen_1957) -> q_gen_1907
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913, q_gen_1938},
Q_f={q_gen_1906},
Delta=
{
<s>(q_gen_1938) -> q_gen_1938
<z>() -> q_gen_1938
<s, s>(q_gen_1913) -> q_gen_1913
<z, s>(q_gen_1938) -> q_gen_1913
<z, z>() -> q_gen_1913
<s, s, s>(q_gen_1906) -> q_gen_1906
<s, z, s>(q_gen_1913) -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, s>(q_gen_1938) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 10
() -> member([e2, node(e2, t1, t2)]) -> 12
() -> numnodes([leaf, z]) -> 10
() -> plus([n, z, n]) -> 10
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10
(leq([s(nn1), z])) -> BOT -> 10
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 10
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 12
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 10
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 11
(member([e, leaf])) -> BOT -> 10
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 13
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 13
}
Sat witness: Found: ((numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]), {
_qi -> z  ;  _ri -> z  ;  _si -> s(s(z))  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 29, which took 0.037564 s (model generation: 0.021739,  model checking: 0.015825):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911, q_gen_1934},
Q_f={q_gen_1911},
Delta=
{
<s>(q_gen_1934) -> q_gen_1934
<z>() -> q_gen_1934
<s, s>(q_gen_1911) -> q_gen_1911
<z, s>(q_gen_1934) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1918, q_gen_1922, q_gen_1927},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1909
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1918
<node>(q_gen_1910, q_gen_1909, q_gen_1918) -> q_gen_1918
<node>(q_gen_1922, q_gen_1918, q_gen_1909) -> q_gen_1918
<node>(q_gen_1922, q_gen_1918, q_gen_1918) -> q_gen_1918
<a>() -> q_gen_1922
<a, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1909, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1918, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1918, q_gen_1918) -> q_gen_1908
<b, leaf>() -> q_gen_1927
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1927
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916, q_gen_1957},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<a>() -> q_gen_1916
<b>() -> q_gen_1916
<s>(q_gen_1957) -> q_gen_1957
<z>() -> q_gen_1957
<leaf, s>(q_gen_1957) -> q_gen_1907
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913, q_gen_1938},
Q_f={q_gen_1906},
Delta=
{
<s>(q_gen_1938) -> q_gen_1938
<z>() -> q_gen_1938
<s, s>(q_gen_1913) -> q_gen_1913
<z, s>(q_gen_1938) -> q_gen_1913
<z, z>() -> q_gen_1913
<s, s, s>(q_gen_1906) -> q_gen_1906
<s, z, s>(q_gen_1913) -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, s>(q_gen_1938) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 10
() -> member([e2, node(e2, t1, t2)]) -> 12
() -> numnodes([leaf, z]) -> 10
() -> plus([n, z, n]) -> 10
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10
(leq([s(nn1), z])) -> BOT -> 10
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 10
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 12
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 13
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 11
(member([e, leaf])) -> BOT -> 11
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 13
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 13
}
Sat witness: Found: ((not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> b  ;  e2 -> a  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> node(b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
})

-------------------------------------------
Step 30, which took 0.039610 s (model generation: 0.024157,  model checking: 0.015453):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911, q_gen_1934},
Q_f={q_gen_1911},
Delta=
{
<s>(q_gen_1934) -> q_gen_1934
<z>() -> q_gen_1934
<s, s>(q_gen_1911) -> q_gen_1911
<z, s>(q_gen_1934) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1917, q_gen_1919, q_gen_1922},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1909
<node>(q_gen_1922, q_gen_1919, q_gen_1919) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1919
<node>(q_gen_1910, q_gen_1909, q_gen_1919) -> q_gen_1919
<node>(q_gen_1910, q_gen_1919, q_gen_1909) -> q_gen_1919
<node>(q_gen_1910, q_gen_1919, q_gen_1919) -> q_gen_1919
<node>(q_gen_1922, q_gen_1919, q_gen_1909) -> q_gen_1919
<a>() -> q_gen_1922
<a, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1919) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1919, q_gen_1919) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1909, q_gen_1919) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1919, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1919, q_gen_1919) -> q_gen_1908
<b, leaf>() -> q_gen_1917
<b, node>(q_gen_1910, q_gen_1919, q_gen_1909) -> q_gen_1917
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1917
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916, q_gen_1957},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<a>() -> q_gen_1916
<b>() -> q_gen_1916
<s>(q_gen_1957) -> q_gen_1957
<z>() -> q_gen_1957
<leaf, s>(q_gen_1957) -> q_gen_1907
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913, q_gen_1938},
Q_f={q_gen_1906},
Delta=
{
<s>(q_gen_1938) -> q_gen_1938
<z>() -> q_gen_1938
<s, s>(q_gen_1913) -> q_gen_1913
<z, s>(q_gen_1938) -> q_gen_1913
<z, z>() -> q_gen_1913
<s, s, s>(q_gen_1906) -> q_gen_1906
<s, z, s>(q_gen_1913) -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, s>(q_gen_1938) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 11
() -> member([e2, node(e2, t1, t2)]) -> 12
() -> numnodes([leaf, z]) -> 11
() -> plus([n, z, n]) -> 11
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11
(leq([s(nn1), z])) -> BOT -> 11
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 11
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 12
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 13
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 14
(member([e, leaf])) -> BOT -> 12
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 13
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 13
}
Sat witness: Found: ((not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]), {
e -> b  ;  e2 -> a  ;  t1 -> node(b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, leaf, leaf))  ;  t2 -> node(b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, leaf, leaf))
})

-------------------------------------------
Step 31, which took 0.050862 s (model generation: 0.028025,  model checking: 0.022837):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911, q_gen_1934},
Q_f={q_gen_1911},
Delta=
{
<s>(q_gen_1934) -> q_gen_1934
<z>() -> q_gen_1934
<s, s>(q_gen_1911) -> q_gen_1911
<z, s>(q_gen_1934) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1919, q_gen_1922, q_gen_1927},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1919, q_gen_1909) -> q_gen_1909
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1909
<node>(q_gen_1922, q_gen_1919, q_gen_1919) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1919
<node>(q_gen_1910, q_gen_1909, q_gen_1919) -> q_gen_1919
<node>(q_gen_1910, q_gen_1919, q_gen_1919) -> q_gen_1919
<node>(q_gen_1922, q_gen_1919, q_gen_1909) -> q_gen_1919
<a>() -> q_gen_1922
<a, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1919) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1919, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1919, q_gen_1919) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1909, q_gen_1919) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1919, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1919, q_gen_1919) -> q_gen_1908
<b, leaf>() -> q_gen_1927
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1927
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916, q_gen_1957},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<a>() -> q_gen_1916
<b>() -> q_gen_1916
<s>(q_gen_1957) -> q_gen_1957
<z>() -> q_gen_1957
<leaf, s>(q_gen_1957) -> q_gen_1907
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913, q_gen_1938},
Q_f={q_gen_1906},
Delta=
{
<s>(q_gen_1938) -> q_gen_1938
<z>() -> q_gen_1938
<s, s>(q_gen_1913) -> q_gen_1913
<z, s>(q_gen_1938) -> q_gen_1913
<z, z>() -> q_gen_1913
<s, s, s>(q_gen_1906) -> q_gen_1906
<s, z, s>(q_gen_1913) -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, s>(q_gen_1938) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 12
() -> member([e2, node(e2, t1, t2)]) -> 12
() -> numnodes([leaf, z]) -> 12
() -> plus([n, z, n]) -> 12
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 12
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 12
(leq([s(nn1), z])) -> BOT -> 12
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 12
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 15
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 13
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 14
(member([e, leaf])) -> BOT -> 13
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 13
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 13
}
Sat witness: Found: ((member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> b  ;  e2 -> a  ;  t1 -> node(a, node(b, leaf, node(a, leaf, leaf)), node(b, leaf, node(a, leaf, leaf)))  ;  t2 -> leaf
})

-------------------------------------------
Step 32, which took 0.034186 s (model generation: 0.033220,  model checking: 0.000966):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911, q_gen_1934},
Q_f={q_gen_1911},
Delta=
{
<s>(q_gen_1934) -> q_gen_1934
<z>() -> q_gen_1934
<s, s>(q_gen_1911) -> q_gen_1911
<z, s>(q_gen_1934) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1918, q_gen_1922, q_gen_1927},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1918, q_gen_1909) -> q_gen_1909
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1918
<node>(q_gen_1910, q_gen_1909, q_gen_1918) -> q_gen_1918
<node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1918
<node>(q_gen_1922, q_gen_1918, q_gen_1909) -> q_gen_1918
<node>(q_gen_1922, q_gen_1918, q_gen_1918) -> q_gen_1918
<a>() -> q_gen_1922
<a, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1909, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1918, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1918, q_gen_1918) -> q_gen_1908
<b, leaf>() -> q_gen_1927
<b, node>(q_gen_1910, q_gen_1918, q_gen_1909) -> q_gen_1927
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1927
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916, q_gen_1957},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<a>() -> q_gen_1916
<b>() -> q_gen_1916
<s>(q_gen_1957) -> q_gen_1957
<z>() -> q_gen_1957
<leaf, s>(q_gen_1957) -> q_gen_1907
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913, q_gen_1938},
Q_f={q_gen_1906},
Delta=
{
<s>(q_gen_1938) -> q_gen_1938
<z>() -> q_gen_1938
<s, s>(q_gen_1913) -> q_gen_1913
<z, s>(q_gen_1938) -> q_gen_1913
<z, z>() -> q_gen_1913
<s, s, s>(q_gen_1906) -> q_gen_1906
<s, z, s>(q_gen_1913) -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, s>(q_gen_1938) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 12
() -> member([e2, node(e2, t1, t2)]) -> 15
() -> numnodes([leaf, z]) -> 13
() -> plus([n, z, n]) -> 13
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 13
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 13
(leq([s(nn1), z])) -> BOT -> 13
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 13
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 15
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 13
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 14
(member([e, leaf])) -> BOT -> 13
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 13
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 13
}
Sat witness: Found: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 33, which took 0.078372 s (model generation: 0.072008,  model checking: 0.006364):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911, q_gen_1934},
Q_f={q_gen_1911},
Delta=
{
<s>(q_gen_1934) -> q_gen_1934
<z>() -> q_gen_1934
<s, s>(q_gen_1911) -> q_gen_1911
<z, s>(q_gen_1934) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1918, q_gen_1922, q_gen_1927},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1918, q_gen_1909) -> q_gen_1909
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1918
<node>(q_gen_1910, q_gen_1909, q_gen_1918) -> q_gen_1918
<node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1918
<node>(q_gen_1922, q_gen_1918, q_gen_1909) -> q_gen_1918
<node>(q_gen_1922, q_gen_1918, q_gen_1918) -> q_gen_1918
<a>() -> q_gen_1922
<a, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1918, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1909, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1918, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1918, q_gen_1918) -> q_gen_1908
<b, leaf>() -> q_gen_1927
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1927
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916, q_gen_1957},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<a>() -> q_gen_1916
<b>() -> q_gen_1916
<s>(q_gen_1957) -> q_gen_1957
<z>() -> q_gen_1957
<leaf, s>(q_gen_1957) -> q_gen_1907
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913, q_gen_1938},
Q_f={q_gen_1906},
Delta=
{
<s>(q_gen_1938) -> q_gen_1938
<z>() -> q_gen_1938
<s, s>(q_gen_1913) -> q_gen_1913
<z, s>(q_gen_1938) -> q_gen_1913
<z, z>() -> q_gen_1913
<s, s, s>(q_gen_1906) -> q_gen_1906
<s, z, s>(q_gen_1913) -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, s>(q_gen_1938) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 13
() -> member([e2, node(e2, t1, t2)]) -> 15
() -> numnodes([leaf, z]) -> 13
() -> plus([n, z, n]) -> 13
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 13
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 13
(leq([s(nn1), z])) -> BOT -> 13
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 13
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 15
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 13
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 14
(member([e, leaf])) -> BOT -> 13
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 16
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 14
}
Sat witness: Found: ((numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]), {
_qi -> s(z)  ;  _ri -> z  ;  _si -> s(z)  ;  e -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 34, which took 0.131379 s (model generation: 0.085128,  model checking: 0.046251):

Model:
|_
{
leq -> 
{{{
Q={q_gen_1911, q_gen_1934},
Q_f={q_gen_1911},
Delta=
{
<s>(q_gen_1934) -> q_gen_1934
<z>() -> q_gen_1934
<s, s>(q_gen_1911) -> q_gen_1911
<z, s>(q_gen_1934) -> q_gen_1911
<z, z>() -> q_gen_1911
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_1908, q_gen_1909, q_gen_1910, q_gen_1918, q_gen_1922, q_gen_1927},
Q_f={q_gen_1908},
Delta=
{
<leaf>() -> q_gen_1909
<node>(q_gen_1910, q_gen_1918, q_gen_1909) -> q_gen_1909
<node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1909
<b>() -> q_gen_1910
<node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1918
<node>(q_gen_1910, q_gen_1909, q_gen_1918) -> q_gen_1918
<node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1918
<node>(q_gen_1922, q_gen_1918, q_gen_1909) -> q_gen_1918
<node>(q_gen_1922, q_gen_1918, q_gen_1918) -> q_gen_1918
<a>() -> q_gen_1922
<a, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1909, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1918, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1910, q_gen_1918, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1909, q_gen_1918) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1918, q_gen_1909) -> q_gen_1908
<b, node>(q_gen_1922, q_gen_1918, q_gen_1918) -> q_gen_1908
<b, leaf>() -> q_gen_1927
<b, node>(q_gen_1922, q_gen_1909, q_gen_1909) -> q_gen_1927
}

Datatype: <elt, elt_bin_tree>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1907, q_gen_1915, q_gen_1916, q_gen_1957},
Q_f={q_gen_1907},
Delta=
{
<leaf>() -> q_gen_1915
<node>(q_gen_1916, q_gen_1915, q_gen_1915) -> q_gen_1915
<a>() -> q_gen_1916
<b>() -> q_gen_1916
<s>(q_gen_1957) -> q_gen_1957
<z>() -> q_gen_1957
<leaf, s>(q_gen_1957) -> q_gen_1907
<leaf, z>() -> q_gen_1907
<node, s>(q_gen_1916, q_gen_1915, q_gen_1907) -> q_gen_1907
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_1906, q_gen_1913, q_gen_1938},
Q_f={q_gen_1906},
Delta=
{
<s>(q_gen_1938) -> q_gen_1938
<z>() -> q_gen_1938
<s, s>(q_gen_1913) -> q_gen_1913
<z, s>(q_gen_1938) -> q_gen_1913
<z, z>() -> q_gen_1913
<s, s, s>(q_gen_1906) -> q_gen_1906
<s, z, s>(q_gen_1913) -> q_gen_1906
<z, s, s>(q_gen_1913) -> q_gen_1906
<z, z, s>(q_gen_1938) -> q_gen_1906
<z, z, z>() -> q_gen_1906
}

Datatype: <nat, nat, nat>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_elt, eq_elt_bin_tree, eq_nat}
_|

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 13
() -> member([e2, node(e2, t1, t2)]) -> 15
() -> numnodes([leaf, z]) -> 13
() -> plus([n, z, n]) -> 13
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 13
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 13
(leq([s(nn1), z])) -> BOT -> 13
(member([e, t1]) /\ numnodes([t1, _wi])) -> leq([s(z), _wi]) -> 13
(member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 15
(not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]) -> 16
(not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]) -> 14
(member([e, leaf])) -> BOT -> 14
(numnodes([t1, _qi]) /\ numnodes([t2, _ri]) /\ plus([_qi, _ri, _si])) -> numnodes([node(e, t1, t2), s(_si)]) -> 16
(plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]) -> 14
}
Sat witness: Found: ((not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> b  ;  e2 -> a  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> node(b, node(b, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))
})

Total time: 60.000870
Reason for stopping: DontKnow. Stopped because: timeout