Solving ../../benchmarks/true/tree_numnodes_subtree.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, _qs])) -> plus([n, s(mm), s(_qs)])}
(plus([_rs, _ss, _ts]) /\ plus([_rs, _ss, _us])) -> eq_nat([_ts, _us])
)
(numnodes, F:
{() -> numnodes([leaf, z])
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)])}
(numnodes([_ys, _at]) /\ numnodes([_ys, _zs])) -> eq_nat([_zs, _at])
)
}

properties:
{(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct])}


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

Clause system for inference is:

{
() -> leq([z, n2]) -> 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  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 0  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 0  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 0
}


Solving took 30.901459 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
leq -> 
{{{
Q={q_gen_6992, q_gen_6997, q_gen_6998, q_gen_6999, q_gen_7001, q_gen_7002, q_gen_7026, q_gen_7027, q_gen_7031, q_gen_7040},
Q_f={},
Delta=
{
<z>() -> q_gen_6998
<s>(q_gen_6998) -> q_gen_7002
<z, z>() -> q_gen_6992
<z, s>(q_gen_6998) -> q_gen_6997
<s, s>(q_gen_6992) -> q_gen_6999
<z, s>(q_gen_7002) -> q_gen_7001
<s, s>(q_gen_7027) -> q_gen_7026
<s, z>(q_gen_6998) -> q_gen_7027
<s, s>(q_gen_7026) -> q_gen_7031
<s, s>(q_gen_7031) -> q_gen_7040
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6991, q_gen_6995, q_gen_6996, q_gen_7006, q_gen_7007, q_gen_7012, q_gen_7013, q_gen_7014, q_gen_7015, q_gen_7020, q_gen_7021, q_gen_7022, q_gen_7023, q_gen_7024, q_gen_7025, q_gen_7028, q_gen_7029, q_gen_7030, q_gen_7034, q_gen_7035, q_gen_7036, q_gen_7037, q_gen_7038, q_gen_7039, q_gen_7041},
Q_f={},
Delta=
{
<z>() -> q_gen_7014
<s>(q_gen_7014) -> q_gen_7024
<s>(q_gen_7024) -> q_gen_7037
<leaf, z>() -> q_gen_6991
<node, s>(q_gen_6996, q_gen_6991, q_gen_6991) -> q_gen_6995
<b, z>() -> q_gen_6996
<node, s>(q_gen_7007, q_gen_6991, q_gen_6991) -> q_gen_7006
<a, z>() -> q_gen_7007
<node, s>(q_gen_7015, q_gen_7013, q_gen_7013) -> q_gen_7012
<leaf, s>(q_gen_7014) -> q_gen_7013
<b, s>(q_gen_7014) -> q_gen_7015
<node, s>(q_gen_7021, q_gen_7013, q_gen_7013) -> q_gen_7020
<a, s>(q_gen_7014) -> q_gen_7021
<node, s>(q_gen_7025, q_gen_7023, q_gen_7023) -> q_gen_7022
<leaf, s>(q_gen_7024) -> q_gen_7023
<b, s>(q_gen_7024) -> q_gen_7025
<node, s>(q_gen_7029, q_gen_7023, q_gen_7023) -> q_gen_7028
<a, s>(q_gen_7024) -> q_gen_7029
<node, s>(q_gen_7021, q_gen_7006, q_gen_6995) -> q_gen_7030
<node, s>(q_gen_7029, q_gen_7020, q_gen_7020) -> q_gen_7034
<node, s>(q_gen_7038, q_gen_7036, q_gen_7036) -> q_gen_7035
<leaf, s>(q_gen_7037) -> q_gen_7036
<a, s>(q_gen_7037) -> q_gen_7038
<node, s>(q_gen_7025, q_gen_7020, q_gen_7012) -> q_gen_7039
<node, s>(q_gen_7025, q_gen_7023, q_gen_7012) -> q_gen_7041
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6990, q_gen_6993, q_gen_6994, q_gen_7000, q_gen_7003, q_gen_7004, q_gen_7005, q_gen_7008, q_gen_7009, q_gen_7010, q_gen_7011, q_gen_7016, q_gen_7017, q_gen_7018, q_gen_7019, q_gen_7032, q_gen_7033},
Q_f={},
Delta=
{
<z>() -> q_gen_7005
<s>(q_gen_7005) -> q_gen_7019
<z, z>() -> q_gen_6994
<s, s>(q_gen_6994) -> q_gen_7009
<z, s>(q_gen_7005) -> q_gen_7011
<z, z, z>() -> q_gen_6990
<z, s, s>(q_gen_6994) -> q_gen_6993
<s, z, s>(q_gen_6994) -> q_gen_7000
<s, s, s>(q_gen_7004) -> q_gen_7003
<z, z, s>(q_gen_7005) -> q_gen_7004
<s, z, s>(q_gen_7009) -> q_gen_7008
<z, s, s>(q_gen_7011) -> q_gen_7010
<s, z, s>(q_gen_7011) -> q_gen_7016
<s, s, s>(q_gen_7018) -> q_gen_7017
<z, z, s>(q_gen_7019) -> q_gen_7018
<s, s, s>(q_gen_7016) -> q_gen_7032
<s, s, s>(q_gen_6993) -> q_gen_7033
}

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.004079 s (model generation: 0.003903,  model checking: 0.000176):

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

}

Datatype: <nat, nat>
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  ;  () -> 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  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 1  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 1  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 1
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.003479 s (model generation: 0.003429,  model checking: 0.000050):

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

}

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

}

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

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  ;  () -> 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  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 1  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 1  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 1
}
Sat witness: Yes: (() -> numnodes([leaf, z]), {

})

-------------------------------------------
Step 2, which took 0.003721 s (model generation: 0.003676,  model checking: 0.000045):

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

}

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

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

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  ;  () -> 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  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 1  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 1  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 1
}
Sat witness: Yes: (() -> leq([z, n2]), {
n2 -> z
})

-------------------------------------------
Step 3, which took 0.003788 s (model generation: 0.003516,  model checking: 0.000272):

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

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

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

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  ;  () -> 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  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 1  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 1  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 4
}
Sat witness: Yes: ((plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]), {
_qs -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 4, which took 0.003700 s (model generation: 0.003585,  model checking: 0.000115):

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

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

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

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  ;  () -> 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  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 1  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 4  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 4
}
Sat witness: Yes: ((numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]), {
_vs -> z  ;  _ws -> z  ;  _xs -> z  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 5, which took 0.005021 s (model generation: 0.004841,  model checking: 0.000180):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6991, q_gen_6996},
Q_f={q_gen_6991},
Delta=
{
<leaf, z>() -> q_gen_6991
<node, s>(q_gen_6996, q_gen_6991, q_gen_6991) -> q_gen_6991
<b, z>() -> q_gen_6996
}

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

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  ;  () -> 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  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 4  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 4  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 4
}
Sat witness: Yes: ((numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]), {
_bt -> z  ;  _ct -> s(z)  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 6, which took 0.006224 s (model generation: 0.006119,  model checking: 0.000105):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6991, q_gen_6996},
Q_f={q_gen_6991},
Delta=
{
<leaf, z>() -> q_gen_6991
<node, s>(q_gen_6996, q_gen_6991, q_gen_6991) -> q_gen_6991
<b, z>() -> q_gen_6996
}

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

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  ;  () -> numnodes([leaf, z]) -> 3  ;  () -> plus([n, z, n]) -> 3  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2  ;  (leq([s(nn1), z])) -> BOT -> 2  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 4  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 4  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 4
}
Sat witness: Yes: ((leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 7, which took 0.009748 s (model generation: 0.009419,  model checking: 0.000329):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6991, q_gen_6996},
Q_f={q_gen_6991},
Delta=
{
<leaf, z>() -> q_gen_6991
<node, s>(q_gen_6996, q_gen_6991, q_gen_6991) -> q_gen_6991
<b, z>() -> q_gen_6996
}

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

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  ;  () -> 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]) -> 3  ;  (leq([s(nn1), z])) -> BOT -> 3  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 4  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 4  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 4
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> s(z)
})

-------------------------------------------
Step 8, which took 0.008219 s (model generation: 0.007570,  model checking: 0.000649):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6991, q_gen_6996},
Q_f={q_gen_6991},
Delta=
{
<leaf, z>() -> q_gen_6991
<node, s>(q_gen_6996, q_gen_6991, q_gen_6991) -> q_gen_6991
<b, z>() -> q_gen_6996
}

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

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  ;  () -> 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  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 4  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 4  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 4
}
Sat witness: Yes: (() -> leq([z, n2]), {
n2 -> s(s(z))
})

-------------------------------------------
Step 9, which took 0.007716 s (model generation: 0.007617,  model checking: 0.000099):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6991, q_gen_6996},
Q_f={q_gen_6991},
Delta=
{
<leaf, z>() -> q_gen_6991
<node, s>(q_gen_6996, q_gen_6991, q_gen_6991) -> q_gen_6991
<b, z>() -> q_gen_6996
}

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

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  ;  () -> 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  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 4  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 4  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 7
}
Sat witness: Yes: ((plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]), {
_qs -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 10, which took 0.010567 s (model generation: 0.008378,  model checking: 0.002189):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6991, q_gen_6996},
Q_f={q_gen_6991},
Delta=
{
<leaf, z>() -> q_gen_6991
<node, s>(q_gen_6996, q_gen_6991, q_gen_6991) -> q_gen_6991
<b, z>() -> q_gen_6996
}

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

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  ;  () -> 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  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 4  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 7  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 7
}
Sat witness: Yes: ((numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]), {
_vs -> z  ;  _ws -> z  ;  _xs -> z  ;  e -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 11, which took 0.015904 s (model generation: 0.014806,  model checking: 0.001098):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6991, q_gen_6996},
Q_f={q_gen_6991},
Delta=
{
<leaf, z>() -> q_gen_6991
<node, s>(q_gen_6996, q_gen_6991, q_gen_6991) -> q_gen_6991
<a, z>() -> q_gen_6996
<b, z>() -> q_gen_6996
}

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

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  ;  () -> numnodes([leaf, z]) -> 5  ;  () -> plus([n, z, n]) -> 9  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5  ;  (leq([s(nn1), z])) -> BOT -> 5  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 5  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 7  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 7
}
Sat witness: Yes: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 12, which took 0.016088 s (model generation: 0.014913,  model checking: 0.001175):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6991, q_gen_6996},
Q_f={q_gen_6991},
Delta=
{
<leaf, z>() -> q_gen_6991
<node, s>(q_gen_6996, q_gen_6991, q_gen_6991) -> q_gen_6991
<a, z>() -> q_gen_6996
<b, z>() -> q_gen_6996
}

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

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]) -> 7  ;  () -> numnodes([leaf, z]) -> 6  ;  () -> plus([n, z, n]) -> 9  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 6  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 6  ;  (leq([s(nn1), z])) -> BOT -> 6  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 6  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 7  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 10
}
Sat witness: Yes: ((plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]), {
_qs -> s(z)  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 13, which took 0.014787 s (model generation: 0.013141,  model checking: 0.001646):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6991, q_gen_6996},
Q_f={q_gen_6991},
Delta=
{
<leaf, z>() -> q_gen_6991
<node, s>(q_gen_6996, q_gen_6991, q_gen_6991) -> q_gen_6991
<a, z>() -> q_gen_6996
<b, z>() -> q_gen_6996
}

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

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]) -> 7  ;  () -> 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  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 7  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 10  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 10
}
Sat witness: Yes: ((numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]), {
_vs -> z  ;  _ws -> z  ;  _xs -> s(z)  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 14, which took 0.015945 s (model generation: 0.014641,  model checking: 0.001304):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6991, q_gen_6996, q_gen_7014},
Q_f={q_gen_6991},
Delta=
{
<z>() -> q_gen_7014
<leaf, s>(q_gen_7014) -> q_gen_6991
<leaf, z>() -> q_gen_6991
<node, s>(q_gen_6996, q_gen_6991, q_gen_6991) -> q_gen_6991
<a, z>() -> q_gen_6996
<b, s>(q_gen_7014) -> q_gen_6996
<b, z>() -> q_gen_6996
}

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

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]) -> 8  ;  () -> numnodes([leaf, z]) -> 8  ;  () -> plus([n, z, n]) -> 10  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 8  ;  (leq([s(nn1), z])) -> BOT -> 8  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 8  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 10  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 13
}
Sat witness: Yes: ((plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]), {
_qs -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 15, which took 0.019160 s (model generation: 0.015882,  model checking: 0.003278):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6991, q_gen_6996, q_gen_7014},
Q_f={q_gen_6991},
Delta=
{
<z>() -> q_gen_7014
<leaf, s>(q_gen_7014) -> q_gen_6991
<leaf, z>() -> q_gen_6991
<node, s>(q_gen_6996, q_gen_6991, q_gen_6991) -> q_gen_6991
<a, z>() -> q_gen_6996
<b, s>(q_gen_7014) -> q_gen_6996
<b, z>() -> q_gen_6996
}

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

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  ;  () -> numnodes([leaf, z]) -> 9  ;  () -> plus([n, z, n]) -> 10  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 9  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 9  ;  (leq([s(nn1), z])) -> BOT -> 9  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 9  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 13  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 13
}
Sat witness: Yes: ((numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]), {
_vs -> z  ;  _ws -> z  ;  _xs -> s(z)  ;  e -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 16, which took 0.023217 s (model generation: 0.017397,  model checking: 0.005820):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6991, q_gen_6996, q_gen_7014},
Q_f={q_gen_6991},
Delta=
{
<z>() -> q_gen_7014
<leaf, s>(q_gen_7014) -> q_gen_6991
<leaf, z>() -> q_gen_6991
<node, s>(q_gen_6996, q_gen_6991, q_gen_6991) -> q_gen_6991
<a, s>(q_gen_7014) -> q_gen_6996
<a, z>() -> q_gen_6996
<b, s>(q_gen_7014) -> q_gen_6996
<b, z>() -> q_gen_6996
}

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

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]) -> 10  ;  () -> numnodes([leaf, z]) -> 10  ;  () -> plus([n, z, n]) -> 11  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10  ;  (leq([s(nn1), z])) -> BOT -> 10  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 10  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 16  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 14
}
Sat witness: Yes: ((numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]), {
_vs -> z  ;  _ws -> z  ;  _xs -> s(s(z))  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 17, which took 0.011610 s (model generation: 0.011244,  model checking: 0.000366):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6991, q_gen_6996, q_gen_7014},
Q_f={q_gen_6991},
Delta=
{
<s>(q_gen_7014) -> q_gen_7014
<z>() -> q_gen_7014
<leaf, s>(q_gen_7014) -> q_gen_6991
<leaf, z>() -> q_gen_6991
<node, s>(q_gen_6996, q_gen_6991, q_gen_6991) -> q_gen_6991
<a, s>(q_gen_7014) -> q_gen_6996
<a, z>() -> q_gen_6996
<b, s>(q_gen_7014) -> q_gen_6996
<b, z>() -> q_gen_6996
}

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

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]) -> 10  ;  () -> numnodes([leaf, z]) -> 10  ;  () -> plus([n, z, n]) -> 11  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10  ;  (leq([s(nn1), z])) -> BOT -> 10  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 13  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 16  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 14
}
Sat witness: Yes: ((numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]), {
_bt -> s(s(z))  ;  _ct -> s(z)  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 18, which took 0.021073 s (model generation: 0.021017,  model checking: 0.000056):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6991, q_gen_6996, q_gen_7014},
Q_f={q_gen_6991},
Delta=
{
<s>(q_gen_7014) -> q_gen_7014
<z>() -> q_gen_7014
<leaf, s>(q_gen_7014) -> q_gen_6991
<leaf, z>() -> q_gen_6991
<node, s>(q_gen_6996, q_gen_6991, q_gen_6991) -> q_gen_6991
<a, s>(q_gen_7014) -> q_gen_6996
<a, z>() -> q_gen_6996
<b, s>(q_gen_7014) -> q_gen_6996
<b, z>() -> q_gen_6996
}

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

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]) -> 10  ;  () -> numnodes([leaf, z]) -> 10  ;  () -> plus([n, z, n]) -> 11  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10  ;  (leq([s(nn1), z])) -> BOT -> 13  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 13  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 16  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 14
}
Sat witness: Yes: ((leq([s(nn1), z])) -> BOT, {
nn1 -> z
})

-------------------------------------------
Step 19, which took 0.020031 s (model generation: 0.019914,  model checking: 0.000117):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6991, q_gen_6996, q_gen_7014},
Q_f={q_gen_6991},
Delta=
{
<s>(q_gen_7014) -> q_gen_7014
<z>() -> q_gen_7014
<leaf, s>(q_gen_7014) -> q_gen_6991
<leaf, z>() -> q_gen_6991
<node, s>(q_gen_6996, q_gen_6991, q_gen_6991) -> q_gen_6991
<a, s>(q_gen_7014) -> q_gen_6996
<a, z>() -> q_gen_6996
<b, s>(q_gen_7014) -> q_gen_6996
<b, z>() -> q_gen_6996
}

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

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]) -> 10  ;  () -> numnodes([leaf, z]) -> 10  ;  () -> plus([n, z, n]) -> 11  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 13  ;  (leq([s(nn1), z])) -> BOT -> 13  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 13  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 16  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 14
}
Sat witness: Yes: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(z)  ;  nn2 -> z
})

-------------------------------------------
Step 20, which took 0.021115 s (model generation: 0.018983,  model checking: 0.002132):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6991, q_gen_6996, q_gen_7013, q_gen_7014},
Q_f={q_gen_6991},
Delta=
{
<s>(q_gen_7014) -> q_gen_7014
<z>() -> q_gen_7014
<leaf, z>() -> q_gen_6991
<node, s>(q_gen_6996, q_gen_6991, q_gen_6991) -> q_gen_6991
<node, s>(q_gen_6996, q_gen_7013, q_gen_7013) -> q_gen_6991
<a, s>(q_gen_7014) -> q_gen_6996
<a, z>() -> q_gen_6996
<b, s>(q_gen_7014) -> q_gen_6996
<b, z>() -> q_gen_6996
<leaf, s>(q_gen_7014) -> q_gen_7013
}

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

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]) -> 11  ;  () -> numnodes([leaf, z]) -> 11  ;  () -> plus([n, z, n]) -> 12  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 13  ;  (leq([s(nn1), z])) -> BOT -> 13  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 16  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 16  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 14
}
Sat witness: Yes: ((numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]), {
_bt -> s(s(s(z)))  ;  _ct -> s(s(z))  ;  e -> a  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 21, which took 0.021416 s (model generation: 0.020634,  model checking: 0.000782):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6991, q_gen_6996, q_gen_7012, q_gen_7014},
Q_f={q_gen_6991},
Delta=
{
<s>(q_gen_7014) -> q_gen_7014
<z>() -> q_gen_7014
<leaf, z>() -> q_gen_6991
<node, s>(q_gen_6996, q_gen_6991, q_gen_6991) -> q_gen_6991
<a, s>(q_gen_7014) -> q_gen_6996
<a, z>() -> q_gen_6996
<b, s>(q_gen_7014) -> q_gen_6996
<b, z>() -> q_gen_6996
<leaf, s>(q_gen_7014) -> q_gen_7012
<node, s>(q_gen_6996, q_gen_7012, q_gen_7012) -> q_gen_7012
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6990, q_gen_6994, q_gen_7004, q_gen_7005},
Q_f={q_gen_6990},
Delta=
{
<s>(q_gen_7005) -> q_gen_7005
<z>() -> q_gen_7005
<s, s>(q_gen_6994) -> q_gen_6994
<z, s>(q_gen_7005) -> q_gen_6994
<z, z>() -> q_gen_6994
<s, s, s>(q_gen_7004) -> q_gen_6990
<s, z, s>(q_gen_6994) -> q_gen_6990
<z, s, s>(q_gen_6994) -> q_gen_6990
<z, z, z>() -> q_gen_6990
<z, z, s>(q_gen_7005) -> q_gen_7004
}

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]) -> 12  ;  () -> numnodes([leaf, z]) -> 12  ;  () -> plus([n, z, n]) -> 13  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 12  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14  ;  (leq([s(nn1), z])) -> BOT -> 14  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 16  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 16  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 17
}
Sat witness: Yes: ((plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]), {
_qs -> s(s(z))  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 22, which took 0.064837 s (model generation: 0.019851,  model checking: 0.044986):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6991, q_gen_6996, q_gen_7013, q_gen_7014, q_gen_7021},
Q_f={q_gen_6991},
Delta=
{
<s>(q_gen_7014) -> q_gen_7014
<z>() -> q_gen_7014
<leaf, z>() -> q_gen_6991
<node, s>(q_gen_6996, q_gen_6991, q_gen_6991) -> q_gen_6991
<node, s>(q_gen_6996, q_gen_7013, q_gen_7013) -> q_gen_6991
<node, s>(q_gen_7021, q_gen_7013, q_gen_7013) -> q_gen_6991
<a, z>() -> q_gen_6996
<b, s>(q_gen_7014) -> q_gen_6996
<b, z>() -> q_gen_6996
<leaf, s>(q_gen_7014) -> q_gen_7013
<node, s>(q_gen_7021, q_gen_6991, q_gen_6991) -> q_gen_7013
<a, s>(q_gen_7014) -> q_gen_7021
}

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

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]) -> 13  ;  () -> numnodes([leaf, z]) -> 13  ;  () -> plus([n, z, n]) -> 14  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 13  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 15  ;  (leq([s(nn1), z])) -> BOT -> 15  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 16  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 19  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 17
}
Sat witness: Yes: ((numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]), {
_vs -> s(z)  ;  _ws -> s(s(z))  ;  _xs -> s(s(z))  ;  e -> a  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> node(a, leaf, leaf)
})

-------------------------------------------
Step 23, which took 0.009781 s (model generation: 0.009472,  model checking: 0.000309):

Model:
|_
{
leq -> 
{{{
Q={q_gen_6992, q_gen_6998, q_gen_7026, q_gen_7027},
Q_f={q_gen_6992},
Delta=
{
<s>(q_gen_6998) -> q_gen_6998
<z>() -> q_gen_6998
<s, s>(q_gen_6992) -> q_gen_6992
<s, s>(q_gen_7026) -> q_gen_6992
<z, s>(q_gen_6998) -> q_gen_6992
<z, z>() -> q_gen_6992
<s, s>(q_gen_7027) -> q_gen_7026
<s, z>(q_gen_6998) -> q_gen_7027
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6991, q_gen_6996, q_gen_7013, q_gen_7014},
Q_f={q_gen_6991},
Delta=
{
<s>(q_gen_7014) -> q_gen_7014
<z>() -> q_gen_7014
<leaf, z>() -> q_gen_6991
<node, s>(q_gen_6996, q_gen_6991, q_gen_6991) -> q_gen_6991
<node, s>(q_gen_6996, q_gen_7013, q_gen_7013) -> q_gen_6991
<a, s>(q_gen_7014) -> q_gen_6996
<a, z>() -> q_gen_6996
<b, s>(q_gen_7014) -> q_gen_6996
<b, z>() -> q_gen_6996
<leaf, s>(q_gen_7014) -> q_gen_7013
}

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

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]) -> 14  ;  () -> numnodes([leaf, z]) -> 14  ;  () -> plus([n, z, n]) -> 15  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 14  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 18  ;  (leq([s(nn1), z])) -> BOT -> 16  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 16  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 19  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 17
}
Sat witness: Yes: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(s(z))  ;  nn2 -> s(z)
})

-------------------------------------------
Step 24, which took 0.143978 s (model generation: 0.016411,  model checking: 0.127567):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6991, q_gen_6995, q_gen_6996, q_gen_7013, q_gen_7014},
Q_f={q_gen_6991, q_gen_6995},
Delta=
{
<s>(q_gen_7014) -> q_gen_7014
<z>() -> q_gen_7014
<leaf, z>() -> q_gen_6991
<node, s>(q_gen_6996, q_gen_7013, q_gen_7013) -> q_gen_6991
<node, s>(q_gen_6996, q_gen_6991, q_gen_6991) -> q_gen_6995
<a, s>(q_gen_7014) -> q_gen_6996
<a, z>() -> q_gen_6996
<b, s>(q_gen_7014) -> q_gen_6996
<b, z>() -> q_gen_6996
<leaf, s>(q_gen_7014) -> q_gen_7013
<node, s>(q_gen_6996, q_gen_6995, q_gen_6995) -> q_gen_7013
}

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

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]) -> 15  ;  () -> numnodes([leaf, z]) -> 15  ;  () -> plus([n, z, n]) -> 16  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 15  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 18  ;  (leq([s(nn1), z])) -> BOT -> 16  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 19  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 19  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 17
}
Sat witness: Yes: ((numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]), {
_bt -> s(s(s(s(z))))  ;  _ct -> s(s(s(z)))  ;  e -> b  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 25, which took 0.012456 s (model generation: 0.011636,  model checking: 0.000820):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  numnodes -> 
{{{
Q={q_gen_6991, q_gen_6996, q_gen_7012, q_gen_7014},
Q_f={q_gen_6991},
Delta=
{
<s>(q_gen_7014) -> q_gen_7014
<z>() -> q_gen_7014
<leaf, z>() -> q_gen_6991
<node, s>(q_gen_6996, q_gen_6991, q_gen_6991) -> q_gen_6991
<a, s>(q_gen_7014) -> q_gen_6996
<a, z>() -> q_gen_6996
<b, s>(q_gen_7014) -> q_gen_6996
<b, z>() -> q_gen_6996
<leaf, s>(q_gen_7014) -> q_gen_7012
<node, s>(q_gen_6996, q_gen_7012, q_gen_7012) -> q_gen_7012
}

Datatype: <elt_bin_tree, nat>
Convolution form: complete
}}}
  ;  plus -> 
{{{
Q={q_gen_6990, q_gen_6994, q_gen_7004, q_gen_7005},
Q_f={q_gen_6990},
Delta=
{
<s>(q_gen_7005) -> q_gen_7005
<z>() -> q_gen_7005
<s, s>(q_gen_6994) -> q_gen_6994
<z, s>(q_gen_7005) -> q_gen_6994
<z, z>() -> q_gen_6994
<s, s, s>(q_gen_6990) -> q_gen_6990
<s, s, s>(q_gen_7004) -> q_gen_6990
<s, z, s>(q_gen_6994) -> q_gen_6990
<z, s, s>(q_gen_6994) -> q_gen_6990
<z, z, z>() -> q_gen_6990
<z, z, s>(q_gen_7005) -> q_gen_7004
}

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]) -> 16  ;  () -> numnodes([leaf, z]) -> 16  ;  () -> plus([n, z, n]) -> 17  ;  (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 16  ;  (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 19  ;  (leq([s(nn1), z])) -> BOT -> 17  ;  (numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 19  ;  (numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 22  ;  (plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 18
}
Sat witness: Yes: ((numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]), {
_vs -> z  ;  _ws -> s(z)  ;  _xs -> s(s(z))  ;  e -> b  ;  t1 -> leaf  ;  t2 -> node(b, leaf, leaf)
})

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