Solving ../../benchmarks/true/tree_numnodes_member.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: 30s
Convolution: complete


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 30.001024 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
leq -> 
{{{
Q={q_gen_6943, q_gen_6954, q_gen_6962, q_gen_6963, q_gen_6976, q_gen_6977},
Q_f={},
Delta=
{
<z>() -> q_gen_6963
<s>(q_gen_6963) -> q_gen_6977
<z, z>() -> q_gen_6943
<s, s>(q_gen_6943) -> q_gen_6954
<z, s>(q_gen_6963) -> q_gen_6962
<z, s>(q_gen_6977) -> q_gen_6976
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  member -> 
{{{
Q={q_gen_6940, q_gen_6941, q_gen_6942, q_gen_6948, q_gen_6949, q_gen_6950, q_gen_6951, q_gen_6952, q_gen_6953, q_gen_6955, q_gen_6956, q_gen_6957, q_gen_6958, q_gen_6959, q_gen_6961, q_gen_6969, q_gen_6970, q_gen_6971, q_gen_6972, q_gen_6975, q_gen_6984, q_gen_6985, q_gen_6986, q_gen_6987, q_gen_6988, q_gen_6989},
Q_f={},
Delta=
{
<leaf>() -> q_gen_6941
<b>() -> q_gen_6942
<node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6949
<a>() -> q_gen_6950
<node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6952
<node>(q_gen_6950, q_gen_6941, q_gen_6949) -> q_gen_6953
<node>(q_gen_6950, q_gen_6952, q_gen_6952) -> q_gen_6959
<node>(q_gen_6950, q_gen_6941, q_gen_6952) -> q_gen_6971
<node>(q_gen_6950, q_gen_6987, q_gen_6986) -> q_gen_6985
<node>(q_gen_6950, q_gen_6949, q_gen_6987) -> q_gen_6986
<node>(q_gen_6942, q_gen_6941, q_gen_6949) -> q_gen_6987
<node>(q_gen_6942, q_gen_6987, q_gen_6985) -> q_gen_6989
<b, node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6941, q_gen_6949) -> q_gen_6948
<b, node>(q_gen_6950, q_gen_6953, q_gen_6952) -> q_gen_6951
<b, leaf>() -> q_gen_6955
<b, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6956
<b, node>(q_gen_6950, q_gen_6952, q_gen_6952) -> q_gen_6957
<b, node>(q_gen_6950, q_gen_6959, q_gen_6941) -> q_gen_6958
<a, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6961
<b, node>(q_gen_6950, q_gen_6941, q_gen_6952) -> q_gen_6969
<b, node>(q_gen_6950, q_gen_6941, q_gen_6971) -> q_gen_6970
<b, node>(q_gen_6950, q_gen_6949, q_gen_6941) -> q_gen_6972
<b, node>(q_gen_6942, q_gen_6952, q_gen_6952) -> q_gen_6975
<b, node>(q_gen_6942, q_gen_6987, q_gen_6985) -> q_gen_6984
<b, node>(q_gen_6950, q_gen_6949, q_gen_6989) -> q_gen_6988
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6939, q_gen_6946, q_gen_6947, q_gen_6967, q_gen_6968, q_gen_6980, q_gen_6981, q_gen_6982, q_gen_6983},
Q_f={},
Delta=
{
<z>() -> q_gen_6982
<leaf, z>() -> q_gen_6939
<node, s>(q_gen_6947, q_gen_6939, q_gen_6939) -> q_gen_6946
<b, z>() -> q_gen_6947
<node, s>(q_gen_6968, q_gen_6939, q_gen_6939) -> q_gen_6967
<a, z>() -> q_gen_6968
<node, s>(q_gen_6983, q_gen_6981, q_gen_6981) -> q_gen_6980
<leaf, s>(q_gen_6982) -> q_gen_6981
<b, s>(q_gen_6982) -> q_gen_6983
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6938, q_gen_6944, q_gen_6945, q_gen_6960, q_gen_6964, q_gen_6965, q_gen_6966, q_gen_6973, q_gen_6974, q_gen_6978, q_gen_6979},
Q_f={},
Delta=
{
<z>() -> q_gen_6966
<z, z>() -> q_gen_6945
<s, s>(q_gen_6945) -> q_gen_6974
<z, s>(q_gen_6966) -> q_gen_6979
<z, z, z>() -> q_gen_6938
<z, s, s>(q_gen_6945) -> q_gen_6944
<s, z, s>(q_gen_6945) -> q_gen_6960
<s, s, s>(q_gen_6965) -> q_gen_6964
<z, z, s>(q_gen_6966) -> q_gen_6965
<s, z, s>(q_gen_6974) -> q_gen_6973
<z, s, s>(q_gen_6979) -> q_gen_6978
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004135 s (model generation: 0.003857,  model checking: 0.000278):

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

}

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

}

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

}

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

}

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

}
--
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: Yes: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.003541 s (model generation: 0.003492,  model checking: 0.000049):

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

}

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

}

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

}

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

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

}
--
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: Yes: (() -> numnodes([leaf, z]), {

})

-------------------------------------------
Step 2, which took 0.003996 s (model generation: 0.003458,  model checking: 0.000538):

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

}

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

}

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

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

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

}
--
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: Yes: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 3, which took 0.003453 s (model generation: 0.003421,  model checking: 0.000032):

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

}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  member -> 
{{{
Q={q_gen_6940, q_gen_6941, q_gen_6942},
Q_f={q_gen_6940},
Delta=
{
<leaf>() -> q_gen_6941
<b>() -> q_gen_6942
<b, node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6940
}

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

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

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

}
--
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: Yes: (() -> leq([z, n2]), {
n2 -> z
})

-------------------------------------------
Step 4, which took 0.003583 s (model generation: 0.003512,  model checking: 0.000071):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  member -> 
{{{
Q={q_gen_6940, q_gen_6941, q_gen_6942},
Q_f={q_gen_6940},
Delta=
{
<leaf>() -> q_gen_6941
<b>() -> q_gen_6942
<b, node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6940
}

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

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

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

}
--
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: Yes: ((plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]), {
_li -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 5, which took 0.004694 s (model generation: 0.004487,  model checking: 0.000207):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  member -> 
{{{
Q={q_gen_6940, q_gen_6941, q_gen_6942},
Q_f={q_gen_6940},
Delta=
{
<leaf>() -> q_gen_6941
<b>() -> q_gen_6942
<b, node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6940
}

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

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6938, q_gen_6945},
Q_f={q_gen_6938},
Delta=
{
<z, z>() -> q_gen_6945
<z, s, s>(q_gen_6945) -> q_gen_6938
<z, z, z>() -> q_gen_6938
}

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

}
--
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: Yes: ((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.082185 s (model generation: 0.007024,  model checking: 0.075161):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  member -> 
{{{
Q={q_gen_6940, q_gen_6941, q_gen_6942},
Q_f={q_gen_6940},
Delta=
{
<leaf>() -> q_gen_6941
<b>() -> q_gen_6942
<b, node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6940
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6939, q_gen_6947},
Q_f={q_gen_6939},
Delta=
{
<leaf, z>() -> q_gen_6939
<node, s>(q_gen_6947, q_gen_6939, q_gen_6939) -> q_gen_6939
<b, z>() -> q_gen_6947
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6938, q_gen_6945},
Q_f={q_gen_6938},
Delta=
{
<z, z>() -> q_gen_6945
<z, s, s>(q_gen_6945) -> q_gen_6938
<z, z, z>() -> q_gen_6938
}

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

}
--
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: Yes: ((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, node(a, leaf, leaf))  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 7, which took 0.005077 s (model generation: 0.004887,  model checking: 0.000190):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  member -> 
{{{
Q={q_gen_6940, q_gen_6941, q_gen_6942},
Q_f={q_gen_6940},
Delta=
{
<leaf>() -> q_gen_6941
<node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6941
<a>() -> q_gen_6942
<b>() -> q_gen_6942
<b, node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6940
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6939, q_gen_6947},
Q_f={q_gen_6939},
Delta=
{
<leaf, z>() -> q_gen_6939
<node, s>(q_gen_6947, q_gen_6939, q_gen_6939) -> q_gen_6939
<b, z>() -> q_gen_6947
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6938, q_gen_6945},
Q_f={q_gen_6938},
Delta=
{
<z, z>() -> q_gen_6945
<z, s, s>(q_gen_6945) -> q_gen_6938
<z, z, z>() -> q_gen_6938
}

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

}
--
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: Yes: ((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.004605 s (model generation: 0.004379,  model checking: 0.000226):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  member -> 
{{{
Q={q_gen_6940, q_gen_6941, q_gen_6942},
Q_f={q_gen_6940},
Delta=
{
<leaf>() -> q_gen_6941
<node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6941
<a>() -> q_gen_6942
<b>() -> q_gen_6942
<b, node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6940
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6939, q_gen_6947},
Q_f={q_gen_6939},
Delta=
{
<leaf, z>() -> q_gen_6939
<node, s>(q_gen_6947, q_gen_6939, q_gen_6939) -> q_gen_6939
<b, z>() -> q_gen_6947
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6938, q_gen_6945},
Q_f={q_gen_6938},
Delta=
{
<z, z>() -> q_gen_6945
<z, s, s>(q_gen_6945) -> q_gen_6938
<z, z, z>() -> q_gen_6938
}

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

}
--
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: Yes: ((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.004652 s (model generation: 0.004524,  model checking: 0.000128):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  member -> 
{{{
Q={q_gen_6940, q_gen_6941, q_gen_6942},
Q_f={q_gen_6940},
Delta=
{
<leaf>() -> q_gen_6941
<node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6941
<a>() -> q_gen_6942
<b>() -> q_gen_6942
<b, leaf>() -> q_gen_6940
<b, node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6940
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6939, q_gen_6947},
Q_f={q_gen_6939},
Delta=
{
<leaf, z>() -> q_gen_6939
<node, s>(q_gen_6947, q_gen_6939, q_gen_6939) -> q_gen_6939
<b, z>() -> q_gen_6947
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6938, q_gen_6945},
Q_f={q_gen_6938},
Delta=
{
<z, z>() -> q_gen_6945
<z, s, s>(q_gen_6945) -> q_gen_6938
<z, z, z>() -> q_gen_6938
}

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

}
--
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: Yes: ((member([e, leaf])) -> BOT, {
e -> b
})

-------------------------------------------
Step 10, which took 0.009501 s (model generation: 0.004522,  model checking: 0.004979):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  member -> 
{{{
Q={q_gen_6940, q_gen_6941, q_gen_6942, q_gen_6949, q_gen_6950, q_gen_6955},
Q_f={q_gen_6940},
Delta=
{
<leaf>() -> q_gen_6941
<b>() -> q_gen_6942
<node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6949
<node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6949
<node>(q_gen_6950, q_gen_6941, q_gen_6949) -> q_gen_6949
<a>() -> q_gen_6950
<b, node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6941, q_gen_6949) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6949, q_gen_6949) -> q_gen_6940
<b, leaf>() -> q_gen_6955
<b, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6955
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6939, q_gen_6947},
Q_f={q_gen_6939},
Delta=
{
<leaf, z>() -> q_gen_6939
<node, s>(q_gen_6947, q_gen_6939, q_gen_6939) -> q_gen_6939
<b, z>() -> q_gen_6947
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6938, q_gen_6945},
Q_f={q_gen_6938},
Delta=
{
<z, z>() -> q_gen_6945
<z, s, s>(q_gen_6945) -> q_gen_6938
<z, z, z>() -> q_gen_6938
}

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

}
--
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: Yes: ((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), node(b, leaf, leaf))  ;  t2 -> leaf
})

-------------------------------------------
Step 11, which took 0.005282 s (model generation: 0.005140,  model checking: 0.000142):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  member -> 
{{{
Q={q_gen_6940, q_gen_6941, q_gen_6942, q_gen_6949, q_gen_6950, q_gen_6955},
Q_f={q_gen_6940},
Delta=
{
<leaf>() -> q_gen_6941
<node>(q_gen_6950, q_gen_6941, q_gen_6949) -> q_gen_6941
<node>(q_gen_6950, q_gen_6949, q_gen_6949) -> q_gen_6941
<b>() -> q_gen_6942
<node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6949
<node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6949
<a>() -> q_gen_6950
<b, node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6941, q_gen_6949) -> q_gen_6940
<b, leaf>() -> q_gen_6955
<b, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6955
<b, node>(q_gen_6950, q_gen_6949, q_gen_6949) -> q_gen_6955
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6939, q_gen_6947},
Q_f={q_gen_6939},
Delta=
{
<leaf, z>() -> q_gen_6939
<node, s>(q_gen_6947, q_gen_6939, q_gen_6939) -> q_gen_6939
<b, z>() -> q_gen_6947
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6938, q_gen_6945},
Q_f={q_gen_6938},
Delta=
{
<z, z>() -> q_gen_6945
<z, s, s>(q_gen_6945) -> q_gen_6938
<z, z, z>() -> q_gen_6938
}

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

}
--
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: Yes: (() -> plus([n, z, n]), {
n -> s(z)
})

-------------------------------------------
Step 12, which took 0.007015 s (model generation: 0.006155,  model checking: 0.000860):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  member -> 
{{{
Q={q_gen_6940, q_gen_6941, q_gen_6942, q_gen_6949, q_gen_6950, q_gen_6955},
Q_f={q_gen_6940},
Delta=
{
<leaf>() -> q_gen_6941
<node>(q_gen_6950, q_gen_6941, q_gen_6949) -> q_gen_6941
<node>(q_gen_6950, q_gen_6949, q_gen_6949) -> q_gen_6941
<b>() -> q_gen_6942
<node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6949
<node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6949
<a>() -> q_gen_6950
<b, node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6941, q_gen_6949) -> q_gen_6940
<b, leaf>() -> q_gen_6955
<b, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6955
<b, node>(q_gen_6950, q_gen_6949, q_gen_6949) -> q_gen_6955
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6939, q_gen_6947},
Q_f={q_gen_6939},
Delta=
{
<leaf, z>() -> q_gen_6939
<node, s>(q_gen_6947, q_gen_6939, q_gen_6939) -> q_gen_6939
<b, z>() -> q_gen_6947
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6938, q_gen_6945},
Q_f={q_gen_6938},
Delta=
{
<z, z>() -> q_gen_6945
<s, z, s>(q_gen_6945) -> q_gen_6938
<z, s, s>(q_gen_6945) -> q_gen_6938
<z, z, z>() -> q_gen_6938
}

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

}
--
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: Yes: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 13, which took 0.009545 s (model generation: 0.009506,  model checking: 0.000039):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  member -> 
{{{
Q={q_gen_6940, q_gen_6941, q_gen_6942, q_gen_6949, q_gen_6950, q_gen_6955},
Q_f={q_gen_6940},
Delta=
{
<leaf>() -> q_gen_6941
<node>(q_gen_6950, q_gen_6941, q_gen_6949) -> q_gen_6941
<node>(q_gen_6950, q_gen_6949, q_gen_6949) -> q_gen_6941
<b>() -> q_gen_6942
<node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6949
<node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6949
<a>() -> q_gen_6950
<a, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6941, q_gen_6949) -> q_gen_6940
<b, leaf>() -> q_gen_6955
<b, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6955
<b, node>(q_gen_6950, q_gen_6949, q_gen_6949) -> q_gen_6955
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6939, q_gen_6947},
Q_f={q_gen_6939},
Delta=
{
<leaf, z>() -> q_gen_6939
<node, s>(q_gen_6947, q_gen_6939, q_gen_6939) -> q_gen_6939
<b, z>() -> q_gen_6947
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6938, q_gen_6945},
Q_f={q_gen_6938},
Delta=
{
<z, z>() -> q_gen_6945
<s, z, s>(q_gen_6945) -> q_gen_6938
<z, s, s>(q_gen_6945) -> q_gen_6938
<z, z, z>() -> q_gen_6938
}

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

}
--
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: Yes: (() -> leq([z, n2]), {
n2 -> s(z)
})

-------------------------------------------
Step 14, which took 0.008109 s (model generation: 0.007918,  model checking: 0.000191):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  member -> 
{{{
Q={q_gen_6940, q_gen_6941, q_gen_6942, q_gen_6949, q_gen_6950, q_gen_6955},
Q_f={q_gen_6940},
Delta=
{
<leaf>() -> q_gen_6941
<node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6941
<b>() -> q_gen_6942
<node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6949
<node>(q_gen_6950, q_gen_6941, q_gen_6949) -> q_gen_6949
<a>() -> q_gen_6950
<a, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6941, q_gen_6949) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6949, q_gen_6941) -> q_gen_6940
<b, leaf>() -> q_gen_6955
<b, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6955
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6939, q_gen_6947},
Q_f={q_gen_6939},
Delta=
{
<leaf, z>() -> q_gen_6939
<node, s>(q_gen_6947, q_gen_6939, q_gen_6939) -> q_gen_6939
<b, z>() -> q_gen_6947
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6938, q_gen_6945},
Q_f={q_gen_6938},
Delta=
{
<z, z>() -> q_gen_6945
<s, z, s>(q_gen_6945) -> q_gen_6938
<z, s, s>(q_gen_6945) -> q_gen_6938
<z, z, z>() -> q_gen_6938
}

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

}
--
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: Yes: ((plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]), {
_li -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 15, which took 0.010203 s (model generation: 0.009489,  model checking: 0.000714):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  member -> 
{{{
Q={q_gen_6940, q_gen_6941, q_gen_6942, q_gen_6949, q_gen_6950, q_gen_6955},
Q_f={q_gen_6940},
Delta=
{
<leaf>() -> q_gen_6941
<node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6941
<b>() -> q_gen_6942
<node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6949
<node>(q_gen_6950, q_gen_6941, q_gen_6949) -> q_gen_6949
<a>() -> q_gen_6950
<a, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6941, q_gen_6949) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6949, q_gen_6941) -> q_gen_6940
<b, leaf>() -> q_gen_6955
<b, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6955
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6939, q_gen_6947},
Q_f={q_gen_6939},
Delta=
{
<leaf, z>() -> q_gen_6939
<node, s>(q_gen_6947, q_gen_6939, q_gen_6939) -> q_gen_6939
<b, z>() -> q_gen_6947
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6938, q_gen_6945, q_gen_6966},
Q_f={q_gen_6938},
Delta=
{
<z>() -> q_gen_6966
<z, z>() -> q_gen_6945
<s, s, s>(q_gen_6938) -> q_gen_6938
<s, z, s>(q_gen_6945) -> q_gen_6938
<z, s, s>(q_gen_6945) -> q_gen_6938
<z, z, s>(q_gen_6966) -> q_gen_6938
<z, z, z>() -> q_gen_6938
}

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

}
--
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: Yes: ((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.016411 s (model generation: 0.009726,  model checking: 0.006685):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  member -> 
{{{
Q={q_gen_6940, q_gen_6941, q_gen_6942, q_gen_6949, q_gen_6950, q_gen_6955},
Q_f={q_gen_6940},
Delta=
{
<leaf>() -> q_gen_6941
<node>(q_gen_6950, q_gen_6941, q_gen_6949) -> q_gen_6941
<node>(q_gen_6950, q_gen_6949, q_gen_6949) -> q_gen_6941
<b>() -> q_gen_6942
<node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6949
<node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6949
<a>() -> q_gen_6950
<a, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6941, q_gen_6949) -> q_gen_6940
<b, leaf>() -> q_gen_6955
<b, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6955
<b, node>(q_gen_6950, q_gen_6949, q_gen_6949) -> q_gen_6955
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6939, q_gen_6947},
Q_f={q_gen_6939},
Delta=
{
<leaf, z>() -> q_gen_6939
<node, s>(q_gen_6947, q_gen_6939, q_gen_6939) -> q_gen_6939
<a, z>() -> q_gen_6947
<b, z>() -> q_gen_6947
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6938, q_gen_6945, q_gen_6966},
Q_f={q_gen_6938},
Delta=
{
<z>() -> q_gen_6966
<z, z>() -> q_gen_6945
<s, s, s>(q_gen_6938) -> q_gen_6938
<s, z, s>(q_gen_6945) -> q_gen_6938
<z, s, s>(q_gen_6945) -> q_gen_6938
<z, z, s>(q_gen_6966) -> q_gen_6938
<z, z, z>() -> q_gen_6938
}

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

}
--
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: Yes: ((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, leaf, node(b, leaf, leaf))
})

-------------------------------------------
Step 17, which took 0.015438 s (model generation: 0.014256,  model checking: 0.001182):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  member -> 
{{{
Q={q_gen_6940, q_gen_6941, q_gen_6942, q_gen_6949, q_gen_6950, q_gen_6955},
Q_f={q_gen_6940},
Delta=
{
<leaf>() -> q_gen_6941
<node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6941
<b>() -> q_gen_6942
<node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6949
<node>(q_gen_6950, q_gen_6941, q_gen_6949) -> q_gen_6949
<a>() -> q_gen_6950
<a, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6941, q_gen_6949) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6949, q_gen_6941) -> q_gen_6940
<b, leaf>() -> q_gen_6955
<b, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6955
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6939, q_gen_6947},
Q_f={q_gen_6939},
Delta=
{
<leaf, z>() -> q_gen_6939
<node, s>(q_gen_6947, q_gen_6939, q_gen_6939) -> q_gen_6939
<a, z>() -> q_gen_6947
<b, z>() -> q_gen_6947
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6938, q_gen_6945, q_gen_6966},
Q_f={q_gen_6938},
Delta=
{
<z>() -> q_gen_6966
<z, z>() -> q_gen_6945
<s, s, s>(q_gen_6938) -> q_gen_6938
<s, z, s>(q_gen_6945) -> q_gen_6938
<z, s, s>(q_gen_6945) -> q_gen_6938
<z, z, s>(q_gen_6966) -> q_gen_6938
<z, z, z>() -> q_gen_6938
}

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

}
--
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]) -> 5  ;  (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: Yes: ((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 18, which took 0.020996 s (model generation: 0.019052,  model checking: 0.001944):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  member -> 
{{{
Q={q_gen_6940, q_gen_6941, q_gen_6942, q_gen_6948, q_gen_6950, q_gen_6952},
Q_f={q_gen_6940},
Delta=
{
<leaf>() -> q_gen_6941
<node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6941
<b>() -> q_gen_6942
<a>() -> q_gen_6950
<node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6952
<node>(q_gen_6950, q_gen_6941, q_gen_6952) -> q_gen_6952
<node>(q_gen_6950, q_gen_6952, q_gen_6952) -> q_gen_6952
<a, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6941, q_gen_6952) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6952, q_gen_6941) -> q_gen_6940
<b, leaf>() -> q_gen_6948
<b, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6948
<b, node>(q_gen_6950, q_gen_6952, q_gen_6952) -> q_gen_6948
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6939, q_gen_6947},
Q_f={q_gen_6939},
Delta=
{
<leaf, z>() -> q_gen_6939
<node, s>(q_gen_6947, q_gen_6939, q_gen_6939) -> q_gen_6939
<a, z>() -> q_gen_6947
<b, z>() -> q_gen_6947
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6938, q_gen_6945, q_gen_6966},
Q_f={q_gen_6938},
Delta=
{
<z>() -> q_gen_6966
<z, z>() -> q_gen_6945
<s, s, s>(q_gen_6938) -> q_gen_6938
<s, z, s>(q_gen_6945) -> q_gen_6938
<z, s, s>(q_gen_6945) -> q_gen_6938
<z, z, s>(q_gen_6966) -> q_gen_6938
<z, z, z>() -> q_gen_6938
}

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

}
--
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]) -> 6  ;  (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: Yes: ((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 19, which took 0.019105 s (model generation: 0.018228,  model checking: 0.000877):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  member -> 
{{{
Q={q_gen_6940, q_gen_6941, q_gen_6942, q_gen_6948, q_gen_6950, q_gen_6952},
Q_f={q_gen_6940},
Delta=
{
<leaf>() -> q_gen_6941
<node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6941
<b>() -> q_gen_6942
<a>() -> q_gen_6950
<node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6952
<node>(q_gen_6950, q_gen_6941, q_gen_6952) -> q_gen_6952
<node>(q_gen_6950, q_gen_6952, q_gen_6952) -> q_gen_6952
<a, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6941, q_gen_6952) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6952, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6952, q_gen_6952) -> q_gen_6940
<b, leaf>() -> q_gen_6948
<b, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6948
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6939, q_gen_6947},
Q_f={q_gen_6939},
Delta=
{
<leaf, z>() -> q_gen_6939
<node, s>(q_gen_6947, q_gen_6939, q_gen_6939) -> q_gen_6939
<a, z>() -> q_gen_6947
<b, z>() -> q_gen_6947
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6938, q_gen_6945, q_gen_6966},
Q_f={q_gen_6938},
Delta=
{
<z>() -> q_gen_6966
<z, z>() -> q_gen_6945
<s, s, s>(q_gen_6938) -> q_gen_6938
<s, z, s>(q_gen_6945) -> q_gen_6938
<z, s, s>(q_gen_6945) -> q_gen_6938
<z, z, s>(q_gen_6966) -> q_gen_6938
<z, z, z>() -> q_gen_6938
}

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

}
--
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]) -> 9  ;  (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: Yes: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 20, which took 0.023145 s (model generation: 0.022004,  model checking: 0.001141):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  member -> 
{{{
Q={q_gen_6940, q_gen_6941, q_gen_6942, q_gen_6948, q_gen_6950, q_gen_6952},
Q_f={q_gen_6940},
Delta=
{
<leaf>() -> q_gen_6941
<node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6941
<b>() -> q_gen_6942
<a>() -> q_gen_6950
<node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6952
<node>(q_gen_6950, q_gen_6941, q_gen_6952) -> q_gen_6952
<node>(q_gen_6950, q_gen_6952, q_gen_6952) -> q_gen_6952
<a, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6941, q_gen_6952) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6952, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6952, q_gen_6952) -> q_gen_6940
<b, leaf>() -> q_gen_6948
<b, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6948
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6939, q_gen_6947},
Q_f={q_gen_6939},
Delta=
{
<leaf, z>() -> q_gen_6939
<node, s>(q_gen_6947, q_gen_6939, q_gen_6939) -> q_gen_6939
<a, z>() -> q_gen_6947
<b, z>() -> q_gen_6947
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6938, q_gen_6945, q_gen_6966},
Q_f={q_gen_6938},
Delta=
{
<z>() -> q_gen_6966
<s, s>(q_gen_6945) -> q_gen_6945
<z, z>() -> q_gen_6945
<s, s, s>(q_gen_6938) -> q_gen_6938
<s, z, s>(q_gen_6945) -> q_gen_6938
<z, s, s>(q_gen_6945) -> q_gen_6938
<z, z, s>(q_gen_6966) -> q_gen_6938
<z, z, z>() -> q_gen_6938
}

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

}
--
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]) -> 9  ;  (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: Yes: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 21, which took 0.022416 s (model generation: 0.022297,  model checking: 0.000119):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  member -> 
{{{
Q={q_gen_6940, q_gen_6941, q_gen_6942, q_gen_6948, q_gen_6950, q_gen_6952},
Q_f={q_gen_6940},
Delta=
{
<leaf>() -> q_gen_6941
<node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6941
<b>() -> q_gen_6942
<a>() -> q_gen_6950
<node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6952
<node>(q_gen_6950, q_gen_6941, q_gen_6952) -> q_gen_6952
<node>(q_gen_6950, q_gen_6952, q_gen_6952) -> q_gen_6952
<a, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6942, q_gen_6952, q_gen_6952) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6941, q_gen_6952) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6952, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6952, q_gen_6952) -> q_gen_6940
<b, leaf>() -> q_gen_6948
<b, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6948
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6939, q_gen_6947},
Q_f={q_gen_6939},
Delta=
{
<leaf, z>() -> q_gen_6939
<node, s>(q_gen_6947, q_gen_6939, q_gen_6939) -> q_gen_6939
<a, z>() -> q_gen_6947
<b, z>() -> q_gen_6947
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6938, q_gen_6945, q_gen_6966},
Q_f={q_gen_6938},
Delta=
{
<z>() -> q_gen_6966
<s, s>(q_gen_6945) -> q_gen_6945
<z, z>() -> q_gen_6945
<s, s, s>(q_gen_6938) -> q_gen_6938
<s, z, s>(q_gen_6945) -> q_gen_6938
<z, s, s>(q_gen_6945) -> q_gen_6938
<z, z, s>(q_gen_6966) -> q_gen_6938
<z, z, z>() -> q_gen_6938
}

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

}
--
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]) -> 7  ;  () -> plus([n, z, n]) -> 9  ;  (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: Yes: (() -> leq([z, n2]), {
n2 -> s(s(z))
})

-------------------------------------------
Step 22, which took 0.013030 s (model generation: 0.012547,  model checking: 0.000483):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  member -> 
{{{
Q={q_gen_6940, q_gen_6941, q_gen_6942, q_gen_6948, q_gen_6950, q_gen_6952},
Q_f={q_gen_6940},
Delta=
{
<leaf>() -> q_gen_6941
<node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6941
<b>() -> q_gen_6942
<a>() -> q_gen_6950
<node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6952
<node>(q_gen_6950, q_gen_6941, q_gen_6952) -> q_gen_6952
<node>(q_gen_6950, q_gen_6952, q_gen_6952) -> q_gen_6952
<a, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6942, q_gen_6952, q_gen_6952) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6941, q_gen_6952) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6952, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6952, q_gen_6952) -> q_gen_6940
<b, leaf>() -> q_gen_6948
<b, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6948
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6939, q_gen_6947},
Q_f={q_gen_6939},
Delta=
{
<leaf, z>() -> q_gen_6939
<node, s>(q_gen_6947, q_gen_6939, q_gen_6939) -> q_gen_6939
<a, z>() -> q_gen_6947
<b, z>() -> q_gen_6947
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6938, q_gen_6945, q_gen_6966},
Q_f={q_gen_6938},
Delta=
{
<z>() -> q_gen_6966
<s, s>(q_gen_6945) -> q_gen_6945
<z, z>() -> q_gen_6945
<s, s, s>(q_gen_6938) -> q_gen_6938
<s, z, s>(q_gen_6945) -> q_gen_6938
<z, s, s>(q_gen_6945) -> q_gen_6938
<z, z, s>(q_gen_6966) -> q_gen_6938
<z, z, z>() -> q_gen_6938
}

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

}
--
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]) -> 7  ;  () -> plus([n, z, n]) -> 9  ;  (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: Yes: ((plus([n, mm, _li])) -> plus([n, s(mm), s(_li)]), {
_li -> s(z)  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 23, which took 0.024687 s (model generation: 0.023373,  model checking: 0.001314):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  member -> 
{{{
Q={q_gen_6940, q_gen_6941, q_gen_6942, q_gen_6948, q_gen_6950, q_gen_6952},
Q_f={q_gen_6940},
Delta=
{
<leaf>() -> q_gen_6941
<node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6941
<b>() -> q_gen_6942
<a>() -> q_gen_6950
<node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6952
<node>(q_gen_6950, q_gen_6941, q_gen_6952) -> q_gen_6952
<node>(q_gen_6950, q_gen_6952, q_gen_6952) -> q_gen_6952
<a, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6942, q_gen_6952, q_gen_6952) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6941, q_gen_6952) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6952, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6952, q_gen_6952) -> q_gen_6940
<b, leaf>() -> q_gen_6948
<b, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6948
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6939, q_gen_6947},
Q_f={q_gen_6939},
Delta=
{
<leaf, z>() -> q_gen_6939
<node, s>(q_gen_6947, q_gen_6939, q_gen_6939) -> q_gen_6939
<a, z>() -> q_gen_6947
<b, z>() -> q_gen_6947
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6938, q_gen_6945, q_gen_6966},
Q_f={q_gen_6938},
Delta=
{
<z>() -> q_gen_6966
<s, s>(q_gen_6945) -> q_gen_6945
<z, s>(q_gen_6966) -> q_gen_6945
<z, z>() -> q_gen_6945
<s, s, s>(q_gen_6938) -> q_gen_6938
<s, z, s>(q_gen_6945) -> q_gen_6938
<z, s, s>(q_gen_6945) -> q_gen_6938
<z, z, s>(q_gen_6966) -> q_gen_6938
<z, z, z>() -> q_gen_6938
}

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

}
--
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]) -> 7  ;  () -> plus([n, z, n]) -> 9  ;  (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: Yes: ((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 24, which took 5.356470 s (model generation: 0.013582,  model checking: 5.342888):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  member -> 
{{{
Q={q_gen_6940, q_gen_6941, q_gen_6942, q_gen_6948, q_gen_6950, q_gen_6952},
Q_f={q_gen_6940},
Delta=
{
<leaf>() -> q_gen_6941
<node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6941
<b>() -> q_gen_6942
<a>() -> q_gen_6950
<node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6952
<node>(q_gen_6950, q_gen_6941, q_gen_6952) -> q_gen_6952
<node>(q_gen_6950, q_gen_6952, q_gen_6952) -> q_gen_6952
<a, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6942, q_gen_6941, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6942, q_gen_6952, q_gen_6952) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6941, q_gen_6952) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6952, q_gen_6941) -> q_gen_6940
<b, node>(q_gen_6950, q_gen_6952, q_gen_6952) -> q_gen_6940
<b, leaf>() -> q_gen_6948
<b, node>(q_gen_6950, q_gen_6941, q_gen_6941) -> q_gen_6948
}

Datatype: <elt, elt_bin_tree>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6939, q_gen_6947, q_gen_6982},
Q_f={q_gen_6939},
Delta=
{
<z>() -> q_gen_6982
<leaf, s>(q_gen_6982) -> q_gen_6939
<leaf, z>() -> q_gen_6939
<node, s>(q_gen_6947, q_gen_6939, q_gen_6939) -> q_gen_6939
<a, z>() -> q_gen_6947
<b, s>(q_gen_6982) -> q_gen_6947
<b, z>() -> q_gen_6947
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6938, q_gen_6945, q_gen_6966},
Q_f={q_gen_6938},
Delta=
{
<z>() -> q_gen_6966
<s, s>(q_gen_6945) -> q_gen_6945
<z, s>(q_gen_6966) -> q_gen_6945
<z, z>() -> q_gen_6945
<s, s, s>(q_gen_6938) -> q_gen_6938
<s, z, s>(q_gen_6945) -> q_gen_6938
<z, s, s>(q_gen_6945) -> q_gen_6938
<z, z, s>(q_gen_6966) -> q_gen_6938
<z, z, z>() -> q_gen_6938
}

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

}
--
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]) -> 7  ;  () -> plus([n, z, n]) -> 9  ;  (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: Yes: ((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, node(b, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(b, leaf, node(a, leaf, leaf)))))
})

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