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


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, _kf])) -> plus([n, s(mm), s(_kf)])}
(plus([_lf, _mf, _nf]) /\ plus([_lf, _mf, _of])) -> eq_nat([_nf, _of])
)
(numnodes, F:
{() -> numnodes([leaf, z])
(numnodes([t1, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)])}
(numnodes([_sf, _tf]) /\ numnodes([_sf, _uf])) -> eq_nat([_tf, _uf])
)
(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, _vf])) -> leq([s(z), _vf])}


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, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 0
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 0
}


Solving took 60.001275 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
leq -> 
{{{
Q={q_gen_1471, q_gen_1482, q_gen_1488, q_gen_1489, q_gen_1501, q_gen_1502},
Q_f={},
Delta=
{
<z>() -> q_gen_1489
<s>(q_gen_1489) -> q_gen_1502
<z, z>() -> q_gen_1471
<s, s>(q_gen_1471) -> q_gen_1482
<z, s>(q_gen_1489) -> q_gen_1488
<z, s>(q_gen_1502) -> q_gen_1501
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_1468, q_gen_1469, q_gen_1470, q_gen_1477, q_gen_1478, q_gen_1479, q_gen_1480, q_gen_1481, q_gen_1483, q_gen_1484, q_gen_1487, q_gen_1496, q_gen_1497, q_gen_1498, q_gen_1499, q_gen_1500, q_gen_1508, q_gen_1509, q_gen_1510, q_gen_1511},
Q_f={},
Delta=
{
<leaf>() -> q_gen_1469
<b>() -> q_gen_1470
<a>() -> q_gen_1478
<node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1480
<node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1481
<node>(q_gen_1478, q_gen_1480, q_gen_1469) -> q_gen_1497
<node>(q_gen_1470, q_gen_1481, q_gen_1481) -> q_gen_1509
<node>(q_gen_1470, q_gen_1509, q_gen_1509) -> q_gen_1511
<b, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1477
<b, node>(q_gen_1478, q_gen_1481, q_gen_1480) -> q_gen_1479
<b, leaf>() -> q_gen_1483
<b, node>(q_gen_1478, q_gen_1480, q_gen_1469) -> q_gen_1484
<a, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1487
<b, node>(q_gen_1478, q_gen_1481, q_gen_1497) -> q_gen_1496
<b, node>(q_gen_1478, q_gen_1481, q_gen_1469) -> q_gen_1498
<a, node>(q_gen_1470, q_gen_1481, q_gen_1469) -> q_gen_1499
<b, node>(q_gen_1470, q_gen_1480, q_gen_1480) -> q_gen_1500
<b, node>(q_gen_1470, q_gen_1509, q_gen_1509) -> q_gen_1508
<b, node>(q_gen_1478, q_gen_1481, q_gen_1511) -> q_gen_1510
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1467, q_gen_1474, q_gen_1475, q_gen_1476, q_gen_1494, q_gen_1495, q_gen_1505, q_gen_1506, q_gen_1507},
Q_f={},
Delta=
{
<leaf>() -> q_gen_1475
<z>() -> q_gen_1507
<leaf, z>() -> q_gen_1467
<node, s>(q_gen_1476, q_gen_1475, q_gen_1475) -> q_gen_1474
<b, z>() -> q_gen_1476
<node, s>(q_gen_1495, q_gen_1475, q_gen_1475) -> q_gen_1494
<a, z>() -> q_gen_1495
<node, s>(q_gen_1506, q_gen_1475, q_gen_1475) -> q_gen_1505
<b, s>(q_gen_1507) -> q_gen_1506
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_1466, q_gen_1472, q_gen_1473, q_gen_1485, q_gen_1486, q_gen_1490, q_gen_1491, q_gen_1492, q_gen_1493, q_gen_1503, q_gen_1504},
Q_f={},
Delta=
{
<z>() -> q_gen_1493
<z, z>() -> q_gen_1473
<s, s>(q_gen_1473) -> q_gen_1486
<z, s>(q_gen_1493) -> q_gen_1504
<z, z, z>() -> q_gen_1466
<z, s, s>(q_gen_1473) -> q_gen_1472
<s, z, s>(q_gen_1486) -> q_gen_1485
<s, z, s>(q_gen_1473) -> q_gen_1490
<s, s, s>(q_gen_1492) -> q_gen_1491
<z, z, s>(q_gen_1493) -> q_gen_1492
<z, s, s>(q_gen_1504) -> q_gen_1503
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.007919 s (model generation: 0.007509,  model checking: 0.000410):

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

}

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

}

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

}

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

}

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

}
--
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, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 1
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 1
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.007023 s (model generation: 0.006947,  model checking: 0.000076):

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

}

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

}

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

}

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

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

}
--
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, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 1
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 1
}
Sat witness: Found: (() -> numnodes([leaf, z]), {

})

-------------------------------------------
Step 2, which took 0.007793 s (model generation: 0.007276,  model checking: 0.000517):

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

}

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

}

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

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

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

}
--
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, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 1
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 1
}
Sat witness: Found: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 3, which took 0.007721 s (model generation: 0.007663,  model checking: 0.000058):

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

}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_1468, q_gen_1469, q_gen_1470},
Q_f={q_gen_1468},
Delta=
{
<leaf>() -> q_gen_1469
<b>() -> q_gen_1470
<b, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
}

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

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

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

}
--
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, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 1
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 1
}
Sat witness: Found: (() -> leq([z, n2]), {
n2 -> z
})

-------------------------------------------
Step 4, which took 0.008126 s (model generation: 0.008027,  model checking: 0.000099):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_1468, q_gen_1469, q_gen_1470},
Q_f={q_gen_1468},
Delta=
{
<leaf>() -> q_gen_1469
<b>() -> q_gen_1470
<b, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
}

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

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

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

}
--
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, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 1
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 4
}
Sat witness: Found: ((plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]), {
_kf -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 5, which took 0.011257 s (model generation: 0.007949,  model checking: 0.003308):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_1468, q_gen_1469, q_gen_1470},
Q_f={q_gen_1468},
Delta=
{
<leaf>() -> q_gen_1469
<b>() -> q_gen_1470
<b, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
}

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

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_1466, q_gen_1473},
Q_f={q_gen_1466},
Delta=
{
<z, z>() -> q_gen_1473
<z, s, s>(q_gen_1473) -> q_gen_1466
<z, z, z>() -> q_gen_1466
}

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

}
--
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, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 4
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 4
}
Sat witness: Found: ((numnodes([t1, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]), {
_pf -> z  ;  _qf -> z  ;  _rf -> z  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 6, which took 0.135474 s (model generation: 0.008098,  model checking: 0.127376):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_1468, q_gen_1469, q_gen_1470},
Q_f={q_gen_1468},
Delta=
{
<leaf>() -> q_gen_1469
<b>() -> q_gen_1470
<b, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1467, q_gen_1475, q_gen_1476},
Q_f={q_gen_1467},
Delta=
{
<leaf>() -> q_gen_1475
<leaf, z>() -> q_gen_1467
<node, s>(q_gen_1476, q_gen_1475, q_gen_1475) -> q_gen_1467
<b, z>() -> q_gen_1476
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_1466, q_gen_1473},
Q_f={q_gen_1466},
Delta=
{
<z, z>() -> q_gen_1473
<z, s, s>(q_gen_1473) -> q_gen_1466
<z, z, z>() -> q_gen_1466
}

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

}
--
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, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 4
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 4
}
Sat witness: Found: ((not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> b  ;  e2 -> a  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 7, which took 0.009555 s (model generation: 0.009308,  model checking: 0.000247):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_1468, q_gen_1469, q_gen_1470},
Q_f={q_gen_1468},
Delta=
{
<leaf>() -> q_gen_1469
<node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1469
<a>() -> q_gen_1470
<b>() -> q_gen_1470
<b, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1467, q_gen_1475, q_gen_1476},
Q_f={q_gen_1467},
Delta=
{
<leaf>() -> q_gen_1475
<leaf, z>() -> q_gen_1467
<node, s>(q_gen_1476, q_gen_1475, q_gen_1475) -> q_gen_1467
<b, z>() -> q_gen_1476
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_1466, q_gen_1473},
Q_f={q_gen_1466},
Delta=
{
<z, z>() -> q_gen_1473
<z, s, s>(q_gen_1473) -> q_gen_1466
<z, z, z>() -> q_gen_1466
}

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

}
--
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, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 4
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 4
}
Sat witness: Found: ((member([e, t1]) /\ numnodes([t1, _vf])) -> leq([s(z), _vf]), {
_vf -> s(z)  ;  e -> b  ;  t1 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 8, which took 0.010655 s (model generation: 0.010331,  model checking: 0.000324):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_1468, q_gen_1469, q_gen_1470},
Q_f={q_gen_1468},
Delta=
{
<leaf>() -> q_gen_1469
<node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1469
<a>() -> q_gen_1470
<b>() -> q_gen_1470
<b, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1467, q_gen_1475, q_gen_1476},
Q_f={q_gen_1467},
Delta=
{
<leaf>() -> q_gen_1475
<leaf, z>() -> q_gen_1467
<node, s>(q_gen_1476, q_gen_1475, q_gen_1475) -> q_gen_1467
<b, z>() -> q_gen_1476
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_1466, q_gen_1473},
Q_f={q_gen_1466},
Delta=
{
<z, z>() -> q_gen_1473
<z, s, s>(q_gen_1473) -> q_gen_1466
<z, z, z>() -> q_gen_1466
}

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

}
--
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, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 4
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 4
}
Sat witness: Found: ((not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]), {
e -> b  ;  e2 -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 9, which took 0.009655 s (model generation: 0.009336,  model checking: 0.000319):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_1468, q_gen_1469, q_gen_1470},
Q_f={q_gen_1468},
Delta=
{
<leaf>() -> q_gen_1469
<node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1469
<a>() -> q_gen_1470
<b>() -> q_gen_1470
<b, leaf>() -> q_gen_1468
<b, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1467, q_gen_1475, q_gen_1476},
Q_f={q_gen_1467},
Delta=
{
<leaf>() -> q_gen_1475
<leaf, z>() -> q_gen_1467
<node, s>(q_gen_1476, q_gen_1475, q_gen_1475) -> q_gen_1467
<b, z>() -> q_gen_1476
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_1466, q_gen_1473},
Q_f={q_gen_1466},
Delta=
{
<z, z>() -> q_gen_1473
<z, s, s>(q_gen_1473) -> q_gen_1466
<z, z, z>() -> q_gen_1466
}

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

}
--
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, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 4
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 4
}
Sat witness: Found: ((member([e, leaf])) -> BOT, {
e -> b
})

-------------------------------------------
Step 10, which took 0.010743 s (model generation: 0.010287,  model checking: 0.000456):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_1468, q_gen_1469, q_gen_1470, q_gen_1477, q_gen_1478, q_gen_1481},
Q_f={q_gen_1468},
Delta=
{
<leaf>() -> q_gen_1469
<node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1469
<b>() -> q_gen_1470
<a>() -> q_gen_1478
<node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1481
<b, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1481, q_gen_1469) -> q_gen_1468
<b, leaf>() -> q_gen_1477
<b, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1477
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1467, q_gen_1475, q_gen_1476},
Q_f={q_gen_1467},
Delta=
{
<leaf>() -> q_gen_1475
<leaf, z>() -> q_gen_1467
<node, s>(q_gen_1476, q_gen_1475, q_gen_1475) -> q_gen_1467
<b, z>() -> q_gen_1476
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_1466, q_gen_1473},
Q_f={q_gen_1466},
Delta=
{
<z, z>() -> q_gen_1473
<z, s, s>(q_gen_1473) -> q_gen_1466
<z, z, z>() -> q_gen_1466
}

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

}
--
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, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 4
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 4
}
Sat witness: Found: ((member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> b  ;  e2 -> a  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 11, which took 0.010825 s (model generation: 0.010598,  model checking: 0.000227):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_1468, q_gen_1469, q_gen_1470, q_gen_1477, q_gen_1478, q_gen_1480},
Q_f={q_gen_1468},
Delta=
{
<leaf>() -> q_gen_1469
<b>() -> q_gen_1470
<a>() -> q_gen_1478
<node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1480
<node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1480
<b, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1480, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1480, q_gen_1480) -> q_gen_1468
<b, leaf>() -> q_gen_1477
<b, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1477
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1467, q_gen_1475, q_gen_1476},
Q_f={q_gen_1467},
Delta=
{
<leaf>() -> q_gen_1475
<leaf, z>() -> q_gen_1467
<node, s>(q_gen_1476, q_gen_1475, q_gen_1475) -> q_gen_1467
<b, z>() -> q_gen_1476
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_1466, q_gen_1473},
Q_f={q_gen_1466},
Delta=
{
<z, z>() -> q_gen_1473
<z, s, s>(q_gen_1473) -> q_gen_1466
<z, z, z>() -> q_gen_1466
}

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

}
--
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, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 4
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 4
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 12, which took 0.010759 s (model generation: 0.009913,  model checking: 0.000846):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_1468, q_gen_1469, q_gen_1470, q_gen_1477, q_gen_1478, q_gen_1480},
Q_f={q_gen_1468},
Delta=
{
<leaf>() -> q_gen_1469
<b>() -> q_gen_1470
<a>() -> q_gen_1478
<node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1480
<node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1480
<b, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1480, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1480, q_gen_1480) -> q_gen_1468
<b, leaf>() -> q_gen_1477
<b, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1477
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1467, q_gen_1475, q_gen_1476},
Q_f={q_gen_1467},
Delta=
{
<leaf>() -> q_gen_1475
<leaf, z>() -> q_gen_1467
<node, s>(q_gen_1476, q_gen_1475, q_gen_1475) -> q_gen_1467
<b, z>() -> q_gen_1476
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_1466, q_gen_1473},
Q_f={q_gen_1466},
Delta=
{
<s, s>(q_gen_1473) -> q_gen_1473
<z, z>() -> q_gen_1473
<s, z, s>(q_gen_1473) -> q_gen_1466
<z, s, s>(q_gen_1473) -> q_gen_1466
<z, z, z>() -> q_gen_1466
}

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

}
--
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, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 4
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 4
}
Sat witness: Found: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 13, which took 0.010307 s (model generation: 0.010238,  model checking: 0.000069):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_1468, q_gen_1469, q_gen_1470, q_gen_1477, q_gen_1478, q_gen_1480},
Q_f={q_gen_1468},
Delta=
{
<leaf>() -> q_gen_1469
<node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1469
<b>() -> q_gen_1470
<a>() -> q_gen_1478
<node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1480
<a, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1469, q_gen_1480) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1480, q_gen_1469) -> q_gen_1468
<b, leaf>() -> q_gen_1477
<b, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1477
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1467, q_gen_1475, q_gen_1476},
Q_f={q_gen_1467},
Delta=
{
<leaf>() -> q_gen_1475
<leaf, z>() -> q_gen_1467
<node, s>(q_gen_1476, q_gen_1475, q_gen_1475) -> q_gen_1467
<b, z>() -> q_gen_1476
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_1466, q_gen_1473},
Q_f={q_gen_1466},
Delta=
{
<s, s>(q_gen_1473) -> q_gen_1473
<z, z>() -> q_gen_1473
<s, z, s>(q_gen_1473) -> q_gen_1466
<z, s, s>(q_gen_1473) -> q_gen_1466
<z, z, z>() -> q_gen_1466
}

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

}
--
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, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 4
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 4
}
Sat witness: Found: (() -> leq([z, n2]), {
n2 -> s(z)
})

-------------------------------------------
Step 14, which took 0.010746 s (model generation: 0.010563,  model checking: 0.000183):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_1468, q_gen_1469, q_gen_1470, q_gen_1477, q_gen_1478, q_gen_1480},
Q_f={q_gen_1468},
Delta=
{
<leaf>() -> q_gen_1469
<b>() -> q_gen_1470
<a>() -> q_gen_1478
<node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1480
<node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1480
<a, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1480, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1480, q_gen_1480) -> q_gen_1468
<b, leaf>() -> q_gen_1477
<b, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1477
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1467, q_gen_1475, q_gen_1476},
Q_f={q_gen_1467},
Delta=
{
<leaf>() -> q_gen_1475
<leaf, z>() -> q_gen_1467
<node, s>(q_gen_1476, q_gen_1475, q_gen_1475) -> q_gen_1467
<b, z>() -> q_gen_1476
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_1466, q_gen_1473},
Q_f={q_gen_1466},
Delta=
{
<s, s>(q_gen_1473) -> q_gen_1473
<z, z>() -> q_gen_1473
<s, z, s>(q_gen_1473) -> q_gen_1466
<z, s, s>(q_gen_1473) -> q_gen_1466
<z, z, z>() -> q_gen_1466
}

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

}
--
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, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 4
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 7
}
Sat witness: Found: ((plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]), {
_kf -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 15, which took 0.013538 s (model generation: 0.012551,  model checking: 0.000987):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_1468, q_gen_1469, q_gen_1470, q_gen_1477, q_gen_1478, q_gen_1480},
Q_f={q_gen_1468},
Delta=
{
<leaf>() -> q_gen_1469
<b>() -> q_gen_1470
<a>() -> q_gen_1478
<node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1480
<node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1480
<a, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1480, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1480, q_gen_1480) -> q_gen_1468
<b, leaf>() -> q_gen_1477
<b, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1477
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1467, q_gen_1475, q_gen_1476},
Q_f={q_gen_1467},
Delta=
{
<leaf>() -> q_gen_1475
<leaf, z>() -> q_gen_1467
<node, s>(q_gen_1476, q_gen_1475, q_gen_1475) -> q_gen_1467
<b, z>() -> q_gen_1476
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_1466, q_gen_1473, q_gen_1493},
Q_f={q_gen_1466},
Delta=
{
<z>() -> q_gen_1493
<s, s>(q_gen_1473) -> q_gen_1473
<z, z>() -> q_gen_1473
<s, s, s>(q_gen_1466) -> q_gen_1466
<s, z, s>(q_gen_1473) -> q_gen_1466
<z, s, s>(q_gen_1473) -> q_gen_1466
<z, z, s>(q_gen_1493) -> q_gen_1466
<z, z, z>() -> q_gen_1466
}

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

}
--
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, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 7
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 7
}
Sat witness: Found: ((numnodes([t1, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]), {
_pf -> z  ;  _qf -> z  ;  _rf -> z  ;  e -> a  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 16, which took 0.024633 s (model generation: 0.012776,  model checking: 0.011857):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_1468, q_gen_1469, q_gen_1470, q_gen_1477, q_gen_1478, q_gen_1480},
Q_f={q_gen_1468},
Delta=
{
<leaf>() -> q_gen_1469
<node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1469
<b>() -> q_gen_1470
<a>() -> q_gen_1478
<node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1480
<a, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1469, q_gen_1480) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1480, q_gen_1469) -> q_gen_1468
<b, leaf>() -> q_gen_1477
<b, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1477
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1467, q_gen_1475, q_gen_1476},
Q_f={q_gen_1467},
Delta=
{
<leaf>() -> q_gen_1475
<leaf, z>() -> q_gen_1467
<node, s>(q_gen_1476, q_gen_1475, q_gen_1475) -> q_gen_1467
<a, z>() -> q_gen_1476
<b, z>() -> q_gen_1476
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_1466, q_gen_1473, q_gen_1493},
Q_f={q_gen_1466},
Delta=
{
<z>() -> q_gen_1493
<s, s>(q_gen_1473) -> q_gen_1473
<z, z>() -> q_gen_1473
<s, s, s>(q_gen_1466) -> q_gen_1466
<s, z, s>(q_gen_1473) -> q_gen_1466
<z, s, s>(q_gen_1473) -> q_gen_1466
<z, z, s>(q_gen_1493) -> q_gen_1466
<z, z, z>() -> q_gen_1466
}

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

}
--
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, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 7
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 7
}
Sat witness: Found: ((not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> b  ;  e2 -> a  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> node(a, node(b, leaf, leaf), leaf)
})

-------------------------------------------
Step 17, which took 0.015168 s (model generation: 0.013461,  model checking: 0.001707):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_1468, q_gen_1469, q_gen_1470, q_gen_1477, q_gen_1478, q_gen_1480},
Q_f={q_gen_1468},
Delta=
{
<leaf>() -> q_gen_1469
<b>() -> q_gen_1470
<a>() -> q_gen_1478
<node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1480
<node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1480
<node>(q_gen_1478, q_gen_1480, q_gen_1469) -> q_gen_1480
<a, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1480, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1480, q_gen_1480) -> q_gen_1468
<b, leaf>() -> q_gen_1477
<b, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1477
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1467, q_gen_1475, q_gen_1476},
Q_f={q_gen_1467},
Delta=
{
<leaf>() -> q_gen_1475
<leaf, z>() -> q_gen_1467
<node, s>(q_gen_1476, q_gen_1475, q_gen_1475) -> q_gen_1467
<a, z>() -> q_gen_1476
<b, z>() -> q_gen_1476
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_1466, q_gen_1473, q_gen_1493},
Q_f={q_gen_1466},
Delta=
{
<z>() -> q_gen_1493
<s, s>(q_gen_1473) -> q_gen_1473
<z, z>() -> q_gen_1473
<s, s, s>(q_gen_1466) -> q_gen_1466
<s, z, s>(q_gen_1473) -> q_gen_1466
<z, s, s>(q_gen_1473) -> q_gen_1466
<z, z, s>(q_gen_1493) -> q_gen_1466
<z, z, z>() -> q_gen_1466
}

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

}
--
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, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 7
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 7
}
Sat witness: Found: ((not member([e, t1]) /\ member([e, node(e2, t1, t2)]) /\ not eq_elt([e, e2])) -> member([e, t2]), {
e -> b  ;  e2 -> a  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 18, which took 0.015458 s (model generation: 0.013322,  model checking: 0.002136):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_1468, q_gen_1469, q_gen_1470, q_gen_1477, q_gen_1478, q_gen_1480},
Q_f={q_gen_1468},
Delta=
{
<leaf>() -> q_gen_1469
<node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1469
<b>() -> q_gen_1470
<a>() -> q_gen_1478
<node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1480
<node>(q_gen_1478, q_gen_1480, q_gen_1469) -> q_gen_1480
<a, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1469, q_gen_1480) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1480, q_gen_1469) -> q_gen_1468
<b, leaf>() -> q_gen_1477
<b, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1477
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1467, q_gen_1475, q_gen_1476},
Q_f={q_gen_1467},
Delta=
{
<leaf>() -> q_gen_1475
<leaf, z>() -> q_gen_1467
<node, s>(q_gen_1476, q_gen_1475, q_gen_1475) -> q_gen_1467
<a, z>() -> q_gen_1476
<b, z>() -> q_gen_1476
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_1466, q_gen_1473, q_gen_1493},
Q_f={q_gen_1466},
Delta=
{
<z>() -> q_gen_1493
<s, s>(q_gen_1473) -> q_gen_1473
<z, z>() -> q_gen_1473
<s, s, s>(q_gen_1466) -> q_gen_1466
<s, z, s>(q_gen_1473) -> q_gen_1466
<z, s, s>(q_gen_1473) -> q_gen_1466
<z, z, s>(q_gen_1493) -> q_gen_1466
<z, z, z>() -> q_gen_1466
}

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

}
--
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, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 7
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 7
}
Sat witness: Found: ((member([e, t1]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> a  ;  e2 -> b  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 19, which took 0.016652 s (model generation: 0.015354,  model checking: 0.001298):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_1468, q_gen_1469, q_gen_1470, q_gen_1477, q_gen_1478, q_gen_1480},
Q_f={q_gen_1468},
Delta=
{
<leaf>() -> q_gen_1469
<node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1469
<b>() -> q_gen_1470
<a>() -> q_gen_1478
<node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1480
<node>(q_gen_1478, q_gen_1480, q_gen_1469) -> q_gen_1480
<a, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
<a, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1469, q_gen_1480) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1480, q_gen_1469) -> q_gen_1468
<b, leaf>() -> q_gen_1477
<b, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1477
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1467, q_gen_1475, q_gen_1476},
Q_f={q_gen_1467},
Delta=
{
<leaf>() -> q_gen_1475
<leaf, z>() -> q_gen_1467
<node, s>(q_gen_1476, q_gen_1475, q_gen_1475) -> q_gen_1467
<a, z>() -> q_gen_1476
<b, z>() -> q_gen_1476
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_1466, q_gen_1473, q_gen_1493},
Q_f={q_gen_1466},
Delta=
{
<z>() -> q_gen_1493
<s, s>(q_gen_1473) -> q_gen_1473
<z, z>() -> q_gen_1473
<s, s, s>(q_gen_1466) -> q_gen_1466
<s, z, s>(q_gen_1473) -> q_gen_1466
<z, s, s>(q_gen_1473) -> q_gen_1466
<z, z, s>(q_gen_1493) -> q_gen_1466
<z, z, z>() -> q_gen_1466
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 6
() -> member([e2, node(e2, t1, t2)]) -> 9
() -> numnodes([leaf, z]) -> 7
() -> plus([n, z, n]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 7
(leq([s(nn1), z])) -> BOT -> 7
(member([e, t1]) /\ numnodes([t1, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 7
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 7
}
Sat witness: Found: (() -> member([e2, node(e2, t1, t2)]), {
e2 -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 20, which took 0.015761 s (model generation: 0.015663,  model checking: 0.000098):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_1468, q_gen_1469, q_gen_1470, q_gen_1477, q_gen_1478, q_gen_1480},
Q_f={q_gen_1468},
Delta=
{
<leaf>() -> q_gen_1469
<node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1469
<b>() -> q_gen_1470
<a>() -> q_gen_1478
<node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1480
<node>(q_gen_1478, q_gen_1480, q_gen_1469) -> q_gen_1480
<a, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
<a, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1470, q_gen_1480, q_gen_1480) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1469, q_gen_1480) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1480, q_gen_1469) -> q_gen_1468
<b, leaf>() -> q_gen_1477
<b, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1477
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1467, q_gen_1475, q_gen_1476},
Q_f={q_gen_1467},
Delta=
{
<leaf>() -> q_gen_1475
<leaf, z>() -> q_gen_1467
<node, s>(q_gen_1476, q_gen_1475, q_gen_1475) -> q_gen_1467
<a, z>() -> q_gen_1476
<b, z>() -> q_gen_1476
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_1466, q_gen_1473, q_gen_1493},
Q_f={q_gen_1466},
Delta=
{
<z>() -> q_gen_1493
<s, s>(q_gen_1473) -> q_gen_1473
<z, z>() -> q_gen_1473
<s, s, s>(q_gen_1466) -> q_gen_1466
<s, z, s>(q_gen_1473) -> q_gen_1466
<z, s, s>(q_gen_1473) -> q_gen_1466
<z, z, s>(q_gen_1493) -> q_gen_1466
<z, z, z>() -> q_gen_1466
}

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

}
--
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]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 7
(leq([s(nn1), z])) -> BOT -> 7
(member([e, t1]) /\ numnodes([t1, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 7
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 7
}
Sat witness: Found: (() -> leq([z, n2]), {
n2 -> s(s(z))
})

-------------------------------------------
Step 21, which took 0.015224 s (model generation: 0.015048,  model checking: 0.000176):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_1468, q_gen_1469, q_gen_1470, q_gen_1477, q_gen_1478, q_gen_1480},
Q_f={q_gen_1468},
Delta=
{
<leaf>() -> q_gen_1469
<node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1469
<b>() -> q_gen_1470
<a>() -> q_gen_1478
<node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1480
<node>(q_gen_1478, q_gen_1480, q_gen_1469) -> q_gen_1480
<a, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
<a, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1470, q_gen_1480, q_gen_1480) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1469, q_gen_1480) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1480, q_gen_1469) -> q_gen_1468
<b, leaf>() -> q_gen_1477
<b, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1477
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1467, q_gen_1475, q_gen_1476},
Q_f={q_gen_1467},
Delta=
{
<leaf>() -> q_gen_1475
<leaf, z>() -> q_gen_1467
<node, s>(q_gen_1476, q_gen_1475, q_gen_1475) -> q_gen_1467
<a, z>() -> q_gen_1476
<b, z>() -> q_gen_1476
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_1466, q_gen_1473, q_gen_1493},
Q_f={q_gen_1466},
Delta=
{
<z>() -> q_gen_1493
<s, s>(q_gen_1473) -> q_gen_1473
<z, z>() -> q_gen_1473
<s, s, s>(q_gen_1466) -> q_gen_1466
<s, z, s>(q_gen_1473) -> q_gen_1466
<z, s, s>(q_gen_1473) -> q_gen_1466
<z, z, s>(q_gen_1493) -> q_gen_1466
<z, z, z>() -> q_gen_1466
}

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

}
--
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]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 7
(leq([s(nn1), z])) -> BOT -> 7
(member([e, t1]) /\ numnodes([t1, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 7
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 10
}
Sat witness: Found: ((plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]), {
_kf -> s(z)  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 22, which took 0.016248 s (model generation: 0.015213,  model checking: 0.001035):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_1468, q_gen_1469, q_gen_1470, q_gen_1477, q_gen_1478, q_gen_1480},
Q_f={q_gen_1468},
Delta=
{
<leaf>() -> q_gen_1469
<node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1469
<b>() -> q_gen_1470
<a>() -> q_gen_1478
<node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1480
<node>(q_gen_1478, q_gen_1480, q_gen_1469) -> q_gen_1480
<a, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
<a, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1470, q_gen_1480, q_gen_1480) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1469, q_gen_1480) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1480, q_gen_1469) -> q_gen_1468
<b, leaf>() -> q_gen_1477
<b, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1477
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1467, q_gen_1475, q_gen_1476},
Q_f={q_gen_1467},
Delta=
{
<leaf>() -> q_gen_1475
<leaf, z>() -> q_gen_1467
<node, s>(q_gen_1476, q_gen_1475, q_gen_1475) -> q_gen_1467
<a, z>() -> q_gen_1476
<b, z>() -> q_gen_1476
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_1466, q_gen_1473, q_gen_1493},
Q_f={q_gen_1466},
Delta=
{
<z>() -> q_gen_1493
<s, s>(q_gen_1473) -> q_gen_1473
<z, s>(q_gen_1493) -> q_gen_1473
<z, z>() -> q_gen_1473
<s, s, s>(q_gen_1466) -> q_gen_1466
<s, z, s>(q_gen_1473) -> q_gen_1466
<z, s, s>(q_gen_1473) -> q_gen_1466
<z, z, s>(q_gen_1493) -> q_gen_1466
<z, z, z>() -> q_gen_1466
}

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

}
--
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]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 7
(leq([s(nn1), z])) -> BOT -> 7
(member([e, t1]) /\ numnodes([t1, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 10
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 10
}
Sat witness: Found: ((numnodes([t1, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]), {
_pf -> z  ;  _qf -> z  ;  _rf -> s(z)  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 23, which took 6.460919 s (model generation: 0.016046,  model checking: 6.444873):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_1468, q_gen_1469, q_gen_1470, q_gen_1477, q_gen_1478, q_gen_1480},
Q_f={q_gen_1468},
Delta=
{
<leaf>() -> q_gen_1469
<node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1469
<b>() -> q_gen_1470
<a>() -> q_gen_1478
<node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1480
<node>(q_gen_1478, q_gen_1480, q_gen_1469) -> q_gen_1480
<a, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
<a, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1470, q_gen_1469, q_gen_1469) -> q_gen_1468
<b, node>(q_gen_1470, q_gen_1480, q_gen_1480) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1469, q_gen_1480) -> q_gen_1468
<b, node>(q_gen_1478, q_gen_1480, q_gen_1469) -> q_gen_1468
<b, leaf>() -> q_gen_1477
<b, node>(q_gen_1478, q_gen_1469, q_gen_1469) -> q_gen_1477
}

Datatype: <elt, elt_bin_tree>
Convolution form: left
}}}
  ;  numnodes -> 
{{{
Q={q_gen_1467, q_gen_1475, q_gen_1476, q_gen_1507},
Q_f={q_gen_1467},
Delta=
{
<leaf>() -> q_gen_1475
<z>() -> q_gen_1507
<leaf, z>() -> q_gen_1467
<node, s>(q_gen_1476, q_gen_1475, q_gen_1475) -> q_gen_1467
<a, z>() -> q_gen_1476
<b, s>(q_gen_1507) -> q_gen_1476
<b, z>() -> q_gen_1476
}

Datatype: <elt_bin_tree, nat>
Convolution form: left
}}}
  ;  plus -> 
{{{
Q={q_gen_1466, q_gen_1473, q_gen_1493},
Q_f={q_gen_1466},
Delta=
{
<z>() -> q_gen_1493
<s, s>(q_gen_1473) -> q_gen_1473
<z, s>(q_gen_1493) -> q_gen_1473
<z, z>() -> q_gen_1473
<s, s, s>(q_gen_1466) -> q_gen_1466
<s, z, s>(q_gen_1473) -> q_gen_1466
<z, s, s>(q_gen_1473) -> q_gen_1466
<z, z, s>(q_gen_1493) -> q_gen_1466
<z, z, z>() -> q_gen_1466
}

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

}
--
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]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 7
(leq([s(nn1), z])) -> BOT -> 7
(member([e, t1]) /\ numnodes([t1, _vf])) -> leq([s(z), _vf]) -> 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, _pf]) /\ numnodes([t2, _qf]) /\ plus([_pf, _qf, _rf])) -> numnodes([node(e, t1, t2), s(_rf)]) -> 10
(plus([n, mm, _kf])) -> plus([n, s(mm), s(_kf)]) -> 10
}
Sat witness: Found: ((not member([e, t1]) /\ member([e, t2]) /\ not eq_elt([e, e2])) -> member([e, node(e2, t1, t2)]), {
e -> b  ;  e2 -> a  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> node(b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
})

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