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


Learning problem is:

env: {
elt -> {a, b}  ;  elt_bin_tree -> {leaf, node}  ;  nat -> {s, z}
}
definition:
{
(leq, P:
{() -> leq([z, n2])
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)])
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2])
(leq([s(nn1), z])) -> BOT}
)
(plus, F:
{() -> plus([n, z, n])
(plus([n, mm, _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 60.000297 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
leq -> 
{{{
Q={q_gen_3589, q_gen_3595, q_gen_3596, q_gen_3597, q_gen_3600, q_gen_3601, q_gen_3620, q_gen_3621, q_gen_3639, q_gen_3670, q_gen_3671, q_gen_3684},
Q_f={},
Delta=
{
<z>() -> q_gen_3596
<s>(q_gen_3596) -> q_gen_3601
<z, z>() -> q_gen_3589
<z, s>(q_gen_3596) -> q_gen_3595
<s, s>(q_gen_3589) -> q_gen_3597
<z, s>(q_gen_3601) -> q_gen_3600
<s, s>(q_gen_3621) -> q_gen_3620
<s, z>(q_gen_3596) -> q_gen_3621
<s, s>(q_gen_3620) -> q_gen_3639
<s, s>(q_gen_3671) -> q_gen_3670
<s, s>(q_gen_3639) -> q_gen_3671
<s, s>(q_gen_3670) -> q_gen_3684
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3592, q_gen_3593, q_gen_3594, q_gen_3606, q_gen_3607, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3617, q_gen_3618, q_gen_3619, q_gen_3622, q_gen_3623, q_gen_3624, q_gen_3626, q_gen_3627, q_gen_3628, q_gen_3629, q_gen_3630, q_gen_3631, q_gen_3632, q_gen_3633, q_gen_3636, q_gen_3637, q_gen_3638, q_gen_3640, q_gen_3641, q_gen_3642, q_gen_3643, q_gen_3644, q_gen_3645, q_gen_3646, q_gen_3647, q_gen_3648, q_gen_3649, q_gen_3651, q_gen_3652, q_gen_3662, q_gen_3663, q_gen_3664, q_gen_3665, q_gen_3666, q_gen_3667, q_gen_3668, q_gen_3669, q_gen_3672, q_gen_3673, q_gen_3674, q_gen_3675, q_gen_3676, q_gen_3677, q_gen_3678, q_gen_3679, q_gen_3680, q_gen_3681, q_gen_3682, q_gen_3683, q_gen_3685, q_gen_3687, q_gen_3688, q_gen_3689, q_gen_3690, q_gen_3691, q_gen_3692, q_gen_3693, q_gen_3694, q_gen_3695, q_gen_3696, q_gen_3697, q_gen_3698, q_gen_3699, q_gen_3700, q_gen_3704, q_gen_3705, q_gen_3706, q_gen_3707, q_gen_3708, q_gen_3709, q_gen_3710, q_gen_3711, q_gen_3712, q_gen_3713, q_gen_3714, q_gen_3715, q_gen_3716, q_gen_3717, q_gen_3718, q_gen_3719, q_gen_3720, q_gen_3721, q_gen_3722, q_gen_3723, q_gen_3724, q_gen_3725},
Q_f={},
Delta=
{
<leaf>() -> q_gen_3593
<b>() -> q_gen_3594
<a>() -> q_gen_3607
<z>() -> q_gen_3612
<s>(q_gen_3612) -> q_gen_3619
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3630) -> q_gen_3629
<node>(q_gen_3607, q_gen_3623, q_gen_3593) -> q_gen_3630
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3633
<node>(q_gen_3594, q_gen_3633, q_gen_3593) -> q_gen_3637
<node>(q_gen_3607, q_gen_3593, q_gen_3593) -> q_gen_3641
<node>(q_gen_3594, q_gen_3623, q_gen_3633) -> q_gen_3648
<node>(q_gen_3594, q_gen_3637, q_gen_3593) -> q_gen_3652
<s>(q_gen_3619) -> q_gen_3665
<node>(q_gen_3594, q_gen_3648, q_gen_3652) -> q_gen_3669
<node>(q_gen_3594, q_gen_3623, q_gen_3623) -> q_gen_3673
<s>(q_gen_3679) -> q_gen_3678
<s>(q_gen_3665) -> q_gen_3679
<node>(q_gen_3594, q_gen_3641, q_gen_3593) -> q_gen_3691
<node>(q_gen_3607, q_gen_3641, q_gen_3593) -> q_gen_3693
<node>(q_gen_3594, q_gen_3693, q_gen_3593) -> q_gen_3696
<node>(q_gen_3594, q_gen_3673, q_gen_3593) -> q_gen_3700
<node>(q_gen_3607, q_gen_3641, q_gen_3691) -> q_gen_3709
<node>(q_gen_3594, q_gen_3641, q_gen_3641) -> q_gen_3711
<node>(q_gen_3594, q_gen_3711, q_gen_3593) -> q_gen_3714
<node>(q_gen_3607, q_gen_3648, q_gen_3593) -> q_gen_3725
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3592
<node, s>(q_gen_3607, q_gen_3593, q_gen_3588) -> q_gen_3606
<node, s>(q_gen_3594, q_gen_3593, q_gen_3611) -> q_gen_3610
<leaf, s>(q_gen_3612) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3593, q_gen_3618) -> q_gen_3617
<leaf, s>(q_gen_3619) -> q_gen_3618
<node, s>(q_gen_3594, q_gen_3623, q_gen_3618) -> q_gen_3622
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3624
<node, s>(q_gen_3594, q_gen_3623, q_gen_3627) -> q_gen_3626
<node, s>(q_gen_3607, q_gen_3623, q_gen_3588) -> q_gen_3627
<node, s>(q_gen_3594, q_gen_3629, q_gen_3588) -> q_gen_3628
<node, s>(q_gen_3594, q_gen_3623, q_gen_3611) -> q_gen_3631
<node, s>(q_gen_3594, q_gen_3633, q_gen_3611) -> q_gen_3632
<node, s>(q_gen_3594, q_gen_3637, q_gen_3631) -> q_gen_3636
<node, s>(q_gen_3594, q_gen_3623, q_gen_3624) -> q_gen_3638
<node, s>(q_gen_3594, q_gen_3641, q_gen_3624) -> q_gen_3640
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3642
<node, s>(q_gen_3607, q_gen_3623, q_gen_3618) -> q_gen_3643
<node, s>(q_gen_3594, q_gen_3630, q_gen_3592) -> q_gen_3644
<node, s>(q_gen_3594, q_gen_3623, q_gen_3646) -> q_gen_3645
<node, s>(q_gen_3594, q_gen_3633, q_gen_3588) -> q_gen_3646
<node, s>(q_gen_3607, q_gen_3648, q_gen_3611) -> q_gen_3647
<node, s>(q_gen_3594, q_gen_3637, q_gen_3588) -> q_gen_3649
<node, s>(q_gen_3594, q_gen_3652, q_gen_3647) -> q_gen_3651
<node, s>(q_gen_3594, q_gen_3648, q_gen_3663) -> q_gen_3662
<node, s>(q_gen_3594, q_gen_3637, q_gen_3664) -> q_gen_3663
<leaf, s>(q_gen_3665) -> q_gen_3664
<node, s>(q_gen_3594, q_gen_3669, q_gen_3667) -> q_gen_3666
<node, s>(q_gen_3594, q_gen_3593, q_gen_3668) -> q_gen_3667
<node, s>(q_gen_3594, q_gen_3633, q_gen_3624) -> q_gen_3668
<node, s>(q_gen_3607, q_gen_3673, q_gen_3611) -> q_gen_3672
<node, s>(q_gen_3594, q_gen_3637, q_gen_3675) -> q_gen_3674
<node, s>(q_gen_3607, q_gen_3673, q_gen_3618) -> q_gen_3675
<node, s>(q_gen_3607, q_gen_3623, q_gen_3677) -> q_gen_3676
<leaf, s>(q_gen_3678) -> q_gen_3677
<node, s>(q_gen_3594, q_gen_3630, q_gen_3681) -> q_gen_3680
<node, s>(q_gen_3594, q_gen_3593, q_gen_3682) -> q_gen_3681
<node, s>(q_gen_3594, q_gen_3593, q_gen_3683) -> q_gen_3682
<node, s>(q_gen_3594, q_gen_3593, q_gen_3592) -> q_gen_3683
<node, s>(q_gen_3594, q_gen_3633, q_gen_3646) -> q_gen_3685
<node, s>(q_gen_3594, q_gen_3630, q_gen_3688) -> q_gen_3687
<node, s>(q_gen_3594, q_gen_3633, q_gen_3632) -> q_gen_3688
<node, s>(q_gen_3594, q_gen_3641, q_gen_3588) -> q_gen_3689
<node, s>(q_gen_3607, q_gen_3691, q_gen_3611) -> q_gen_3690
<node, s>(q_gen_3594, q_gen_3693, q_gen_3664) -> q_gen_3692
<node, s>(q_gen_3594, q_gen_3696, q_gen_3695) -> q_gen_3694
<node, s>(q_gen_3594, q_gen_3593, q_gen_3624) -> q_gen_3695
<node, s>(q_gen_3607, q_gen_3623, q_gen_3698) -> q_gen_3697
<node, s>(q_gen_3594, q_gen_3700, q_gen_3699) -> q_gen_3698
<node, s>(q_gen_3594, q_gen_3593, q_gen_3631) -> q_gen_3699
<node, s>(q_gen_3594, q_gen_3623, q_gen_3697) -> q_gen_3704
<node, s>(q_gen_3594, q_gen_3623, q_gen_3677) -> q_gen_3705
<node, s>(q_gen_3594, q_gen_3633, q_gen_3707) -> q_gen_3706
<node, s>(q_gen_3594, q_gen_3623, q_gen_3617) -> q_gen_3707
<node, s>(q_gen_3594, q_gen_3709, q_gen_3588) -> q_gen_3708
<node, s>(q_gen_3594, q_gen_3711, q_gen_3588) -> q_gen_3710
<node, s>(q_gen_3594, q_gen_3714, q_gen_3713) -> q_gen_3712
<node, s>(q_gen_3594, q_gen_3709, q_gen_3611) -> q_gen_3713
<node, s>(q_gen_3607, q_gen_3714, q_gen_3716) -> q_gen_3715
<node, s>(q_gen_3607, q_gen_3623, q_gen_3626) -> q_gen_3716
<node, s>(q_gen_3594, q_gen_3711, q_gen_3718) -> q_gen_3717
<leaf, s>(q_gen_3679) -> q_gen_3718
<node, s>(q_gen_3594, q_gen_3630, q_gen_3588) -> q_gen_3719
<node, s>(q_gen_3607, q_gen_3593, q_gen_3721) -> q_gen_3720
<node, s>(q_gen_3594, q_gen_3630, q_gen_3611) -> q_gen_3721
<node, s>(q_gen_3594, q_gen_3711, q_gen_3618) -> q_gen_3722
<node, s>(q_gen_3594, q_gen_3714, q_gen_3606) -> q_gen_3723
<node, s>(q_gen_3594, q_gen_3725, q_gen_3618) -> q_gen_3724
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3590, q_gen_3591, q_gen_3598, q_gen_3599, q_gen_3602, q_gen_3603, q_gen_3604, q_gen_3605, q_gen_3608, q_gen_3609, q_gen_3613, q_gen_3614, q_gen_3615, q_gen_3616, q_gen_3625, q_gen_3634, q_gen_3635, q_gen_3650, q_gen_3653, q_gen_3654, q_gen_3655, q_gen_3656, q_gen_3657, q_gen_3658, q_gen_3659, q_gen_3660, q_gen_3661, q_gen_3686, q_gen_3701, q_gen_3702, q_gen_3703},
Q_f={},
Delta=
{
<z>() -> q_gen_3605
<s>(q_gen_3605) -> q_gen_3616
<z, z>() -> q_gen_3591
<s, s>(q_gen_3591) -> q_gen_3599
<z, s>(q_gen_3605) -> q_gen_3609
<s, s>(q_gen_3599) -> q_gen_3656
<s, s>(q_gen_3609) -> q_gen_3661
<s, s>(q_gen_3656) -> q_gen_3703
<z, z, z>() -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3590
<s, z, s>(q_gen_3599) -> q_gen_3598
<s, z, s>(q_gen_3591) -> q_gen_3602
<s, s, s>(q_gen_3604) -> q_gen_3603
<z, z, s>(q_gen_3605) -> q_gen_3604
<z, s, s>(q_gen_3609) -> q_gen_3608
<s, z, s>(q_gen_3609) -> q_gen_3613
<s, s, s>(q_gen_3615) -> q_gen_3614
<z, z, s>(q_gen_3616) -> q_gen_3615
<s, s, s>(q_gen_3613) -> q_gen_3625
<s, s, s>(q_gen_3635) -> q_gen_3634
<s, s, s>(q_gen_3587) -> q_gen_3635
<s, s, s>(q_gen_3590) -> q_gen_3650
<s, s, s>(q_gen_3602) -> q_gen_3653
<s, s, s>(q_gen_3603) -> q_gen_3654
<s, z, s>(q_gen_3656) -> q_gen_3655
<z, s, s>(q_gen_3599) -> q_gen_3657
<s, s, s>(q_gen_3614) -> q_gen_3658
<s, s, s>(q_gen_3660) -> q_gen_3659
<s, z, s>(q_gen_3661) -> q_gen_3660
<s, s, s>(q_gen_3653) -> q_gen_3686
<s, s, s>(q_gen_3702) -> q_gen_3701
<z, s, s>(q_gen_3703) -> q_gen_3702
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.010383 s (model generation: 0.009956,  model checking: 0.000427):

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

}

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 0
() -> 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: Found: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.010586 s (model generation: 0.010470,  model checking: 0.000116):

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

}

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 0
() -> 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: Found: (() -> numnodes([leaf, z]), {

})

-------------------------------------------
Step 2, which took 0.010764 s (model generation: 0.010629,  model checking: 0.000135):

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

}

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

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 3
() -> 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: Found: (() -> leq([z, n2]), {
n2 -> z
})

-------------------------------------------
Step 3, which took 0.010732 s (model generation: 0.010546,  model checking: 0.000186):

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 3
() -> 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: Found: ((plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]), {
_qs -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 4, which took 0.010846 s (model generation: 0.010493,  model checking: 0.000353):

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

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

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 3
() -> 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: Found: ((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.011201 s (model generation: 0.010913,  model checking: 0.000288):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<b>() -> q_gen_3594
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 3
() -> 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: Found: ((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.012123 s (model generation: 0.011062,  model checking: 0.001061):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<b>() -> q_gen_3594
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 3
() -> 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: Found: ((leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 7, which took 0.005489 s (model generation: 0.005081,  model checking: 0.000408):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<b>() -> q_gen_3594
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 3
() -> 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: Found: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 8, which took 0.012444 s (model generation: 0.011932,  model checking: 0.000512):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<b>() -> q_gen_3594
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 6
() -> 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: Found: (() -> leq([z, n2]), {
n2 -> s(s(z))
})

-------------------------------------------
Step 9, which took 0.013357 s (model generation: 0.012120,  model checking: 0.001237):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<b>() -> q_gen_3594
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 6
() -> 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: Found: ((plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]), {
_qs -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 10, which took 0.015264 s (model generation: 0.013226,  model checking: 0.002038):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<b>() -> q_gen_3594
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 6
() -> 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: Found: ((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.015175 s (model generation: 0.013735,  model checking: 0.001440):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 7
() -> numnodes([leaf, z]) -> 5
() -> plus([n, z, n]) -> 7
(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)]) -> 10
}
Sat witness: Found: ((plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]), {
_qs -> s(z)  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 12, which took 0.016384 s (model generation: 0.014476,  model checking: 0.001908):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 7
() -> numnodes([leaf, z]) -> 6
() -> plus([n, z, n]) -> 7
(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)]) -> 10
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 10
}
Sat witness: Found: ((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 13, which took 0.016857 s (model generation: 0.015243,  model checking: 0.001614):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3612},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<z>() -> q_gen_3612
<leaf, s>(q_gen_3612) -> q_gen_3588
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 8
() -> numnodes([leaf, z]) -> 7
() -> plus([n, z, n]) -> 8
(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)]) -> 13
}
Sat witness: Found: ((plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]), {
_qs -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 14, which took 0.020149 s (model generation: 0.017080,  model checking: 0.003069):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3612},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<z>() -> q_gen_3612
<leaf, s>(q_gen_3612) -> q_gen_3588
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 9
() -> numnodes([leaf, z]) -> 8
() -> plus([n, z, n]) -> 9
(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)]) -> 13
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 13
}
Sat witness: Found: ((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 15, which took 0.018793 s (model generation: 0.018453,  model checking: 0.000340):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3612},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<leaf, s>(q_gen_3612) -> q_gen_3588
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 9
() -> numnodes([leaf, z]) -> 8
() -> plus([n, z, n]) -> 9
(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]) -> 11
(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: Found: ((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 16, which took 0.019499 s (model generation: 0.019439,  model checking: 0.000060):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3612},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<leaf, s>(q_gen_3612) -> q_gen_3588
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 9
() -> numnodes([leaf, z]) -> 8
() -> plus([n, z, n]) -> 9
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 8
(leq([s(nn1), z])) -> BOT -> 11
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 11
(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: Found: ((leq([s(nn1), z])) -> BOT, {
nn1 -> z
})

-------------------------------------------
Step 17, which took 0.020510 s (model generation: 0.020323,  model checking: 0.000187):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3612},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<leaf, s>(q_gen_3612) -> q_gen_3588
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 9
() -> numnodes([leaf, z]) -> 8
() -> plus([n, z, n]) -> 9
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11
(leq([s(nn1), z])) -> BOT -> 11
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 11
(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: Found: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(z)  ;  nn2 -> z
})

-------------------------------------------
Step 18, which took 0.028655 s (model generation: 0.019681,  model checking: 0.008974):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3611, q_gen_3612},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3611) -> q_gen_3588
<leaf, s>(q_gen_3612) -> q_gen_3611
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 10
() -> 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]) -> 12
(leq([s(nn1), z])) -> BOT -> 12
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 12
(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: Found: ((numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]), {
_vs -> s(s(z))  ;  _ws -> z  ;  _xs -> s(s(z))  ;  e -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 19, which took 0.022775 s (model generation: 0.020639,  model checking: 0.002136):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3611, q_gen_3612},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3611) -> q_gen_3588
<leaf, s>(q_gen_3612) -> q_gen_3611
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 11
() -> 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]) -> 12
(leq([s(nn1), z])) -> BOT -> 12
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 15
(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: Found: ((numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]), {
_bt -> s(s(z))  ;  _ct -> s(z)  ;  e -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 20, which took 0.022899 s (model generation: 0.021426,  model checking: 0.001473):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3610, q_gen_3612},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<leaf, s>(q_gen_3612) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3610
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3604, q_gen_3605},
Q_f={q_gen_3587},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<s, s>(q_gen_3591) -> q_gen_3591
<z, s>(q_gen_3605) -> q_gen_3591
<z, z>() -> q_gen_3591
<s, s, s>(q_gen_3604) -> q_gen_3587
<s, z, s>(q_gen_3591) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 12
() -> 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]) -> 15
(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: Found: ((plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]), {
_qs -> s(s(z))  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 21, which took 0.024529 s (model generation: 0.022036,  model checking: 0.002493):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3610, q_gen_3612},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<leaf, s>(q_gen_3612) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3610
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3604, q_gen_3605},
Q_f={q_gen_3587},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<s, s>(q_gen_3591) -> q_gen_3591
<z, s>(q_gen_3605) -> q_gen_3591
<z, z>() -> q_gen_3591
<s, s, s>(q_gen_3587) -> q_gen_3587
<s, s, s>(q_gen_3604) -> q_gen_3587
<s, z, s>(q_gen_3591) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 13
() -> 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]) -> 18
(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: Found: ((numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]), {
_bt -> s(s(z))  ;  _ct -> s(z)  ;  e -> b  ;  t1 -> node(b, node(b, leaf, leaf), node(a, node(b, leaf, leaf), leaf))  ;  t2 -> leaf
})

-------------------------------------------
Step 22, which took 0.167581 s (model generation: 0.026759,  model checking: 0.140822):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3611, q_gen_3612, q_gen_3623},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3623) -> q_gen_3623
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3611) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3611) -> q_gen_3588
<leaf, s>(q_gen_3612) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3611
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 14
() -> 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]) -> 18
(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: Found: ((numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]), {
_vs -> s(s(z))  ;  _ws -> s(s(z))  ;  _xs -> s(s(z))  ;  e -> b  ;  t1 -> node(b, node(b, node(b, leaf, leaf), leaf), leaf)  ;  t2 -> node(b, node(b, leaf, leaf), leaf)
})

-------------------------------------------
Step 23, which took 0.015487 s (model generation: 0.014091,  model checking: 0.001396):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3612, q_gen_3618, q_gen_3619, q_gen_3623},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<z>() -> q_gen_3612
<s>(q_gen_3612) -> q_gen_3619
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3623) -> q_gen_3623
<leaf, s>(q_gen_3612) -> q_gen_3588
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3618) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3618) -> q_gen_3588
<leaf, s>(q_gen_3619) -> q_gen_3618
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3618
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 15
() -> 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]) -> 16
(leq([s(nn1), z])) -> BOT -> 16
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 21
(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)]) -> 18
}
Sat witness: Found: ((numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]), {
_bt -> s(s(s(z)))  ;  _ct -> s(s(z))  ;  e -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> node(b, node(b, leaf, leaf), leaf)
})

-------------------------------------------
Step 24, which took 0.025874 s (model generation: 0.020131,  model checking: 0.005743):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3592, q_gen_3593, q_gen_3594, q_gen_3610, q_gen_3612},
Q_f={q_gen_3588, q_gen_3592},
Delta=
{
<leaf>() -> q_gen_3593
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3592
<leaf, s>(q_gen_3612) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3593, q_gen_3592) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3610
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3604, q_gen_3605},
Q_f={q_gen_3587},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<s, s>(q_gen_3591) -> q_gen_3591
<z, s>(q_gen_3605) -> q_gen_3591
<z, z>() -> q_gen_3591
<s, s, s>(q_gen_3587) -> q_gen_3587
<s, s, s>(q_gen_3604) -> q_gen_3587
<s, z, s>(q_gen_3591) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 16
() -> 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]) -> 17
(leq([s(nn1), z])) -> BOT -> 17
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 21
(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)]) -> 19
}
Sat witness: Found: ((numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]), {
_vs -> s(z)  ;  _ws -> s(z)  ;  _xs -> s(z)  ;  e -> b  ;  t1 -> node(a, leaf, leaf)  ;  t2 -> node(b, node(b, leaf, leaf), leaf)
})

-------------------------------------------
Step 25, which took 0.049234 s (model generation: 0.045333,  model checking: 0.003901):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3610, q_gen_3612, q_gen_3623},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3623) -> q_gen_3623
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<leaf, s>(q_gen_3612) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3623, q_gen_3610) -> q_gen_3610
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3604, q_gen_3605},
Q_f={q_gen_3587},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<s, s>(q_gen_3591) -> q_gen_3591
<z, s>(q_gen_3605) -> q_gen_3591
<z, z>() -> q_gen_3591
<s, s, s>(q_gen_3587) -> q_gen_3587
<s, s, s>(q_gen_3604) -> q_gen_3587
<s, z, s>(q_gen_3591) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 17
() -> 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]) -> 18
(leq([s(nn1), z])) -> BOT -> 18
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 22
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 25
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 20
}
Sat witness: Found: ((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)
})

-------------------------------------------
Step 26, which took 0.056609 s (model generation: 0.049906,  model checking: 0.006703):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3612, q_gen_3618, q_gen_3619, q_gen_3623, q_gen_3624},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<z>() -> q_gen_3612
<s>(q_gen_3612) -> q_gen_3619
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<leaf, s>(q_gen_3612) -> q_gen_3588
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3618) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3618) -> q_gen_3588
<leaf, s>(q_gen_3619) -> q_gen_3618
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3624
<node, s>(q_gen_3594, q_gen_3623, q_gen_3624) -> q_gen_3624
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 18
() -> numnodes([leaf, z]) -> 17
() -> plus([n, z, n]) -> 18
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 17
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 19
(leq([s(nn1), z])) -> BOT -> 19
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 25
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 25
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 21
}
Sat witness: Found: ((numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]), {
_bt -> s(s(s(z)))  ;  _ct -> s(s(z))  ;  e -> b  ;  t1 -> node(a, node(b, leaf, leaf), leaf)  ;  t2 -> node(b, leaf, leaf)
})

-------------------------------------------
Step 27, which took 0.057241 s (model generation: 0.055736,  model checking: 0.001505):

Model:
|_
{
leq -> 
{{{
Q={q_gen_3589, q_gen_3596, q_gen_3620, q_gen_3621},
Q_f={q_gen_3589},
Delta=
{
<s>(q_gen_3596) -> q_gen_3596
<z>() -> q_gen_3596
<s, s>(q_gen_3589) -> q_gen_3589
<s, s>(q_gen_3620) -> q_gen_3589
<z, s>(q_gen_3596) -> q_gen_3589
<z, z>() -> q_gen_3589
<s, s>(q_gen_3621) -> q_gen_3620
<s, z>(q_gen_3596) -> q_gen_3621
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3612, q_gen_3618, q_gen_3619, q_gen_3623},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<z>() -> q_gen_3612
<s>(q_gen_3612) -> q_gen_3619
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3623) -> q_gen_3623
<leaf, s>(q_gen_3612) -> q_gen_3588
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3618) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3618) -> q_gen_3588
<leaf, s>(q_gen_3619) -> q_gen_3618
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3618
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 19
() -> numnodes([leaf, z]) -> 18
() -> plus([n, z, n]) -> 19
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 18
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 22
(leq([s(nn1), z])) -> BOT -> 20
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 25
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 25
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 21
}
Sat witness: Found: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(s(z))  ;  nn2 -> s(z)
})

-------------------------------------------
Step 28, which took 0.083307 s (model generation: 0.054723,  model checking: 0.028584):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3612, q_gen_3618, q_gen_3619, q_gen_3623, q_gen_3624},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<z>() -> q_gen_3612
<s>(q_gen_3612) -> q_gen_3619
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3623) -> q_gen_3623
<leaf, s>(q_gen_3612) -> q_gen_3588
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3618) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3618) -> q_gen_3588
<leaf, s>(q_gen_3619) -> q_gen_3618
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3624
<node, s>(q_gen_3594, q_gen_3623, q_gen_3624) -> q_gen_3624
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 20
() -> numnodes([leaf, z]) -> 19
() -> plus([n, z, n]) -> 20
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 19
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 23
(leq([s(nn1), z])) -> BOT -> 21
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 25
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 28
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 22
}
Sat witness: Found: ((numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]), {
_vs -> s(z)  ;  _ws -> z  ;  _xs -> s(z)  ;  e -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 29, which took 0.059376 s (model generation: 0.058116,  model checking: 0.001260):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3610, q_gen_3612, q_gen_3623},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3623) -> q_gen_3623
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<leaf, s>(q_gen_3612) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3623, q_gen_3610) -> q_gen_3610
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3599, q_gen_3602, q_gen_3605},
Q_f={q_gen_3587},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<z, z>() -> q_gen_3591
<s, s>(q_gen_3591) -> q_gen_3599
<z, s>(q_gen_3605) -> q_gen_3599
<s, s, s>(q_gen_3587) -> q_gen_3587
<s, s, s>(q_gen_3602) -> q_gen_3587
<s, z, s>(q_gen_3599) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<s, z, s>(q_gen_3591) -> q_gen_3602
<z, s, s>(q_gen_3599) -> q_gen_3602
<z, z, s>(q_gen_3605) -> q_gen_3602
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 20
() -> numnodes([leaf, z]) -> 20
() -> plus([n, z, n]) -> 23
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 20
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 23
(leq([s(nn1), z])) -> BOT -> 21
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 25
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 28
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 22
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(z)
})

-------------------------------------------
Step 30, which took 0.068502 s (model generation: 0.055502,  model checking: 0.013000):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3611, q_gen_3612, q_gen_3623, q_gen_3624, q_gen_3630},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<node>(q_gen_3594, q_gen_3623, q_gen_3630) -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3630, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3630
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3611) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3611) -> q_gen_3588
<leaf, s>(q_gen_3612) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3624) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3630, q_gen_3588) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3624
<node, s>(q_gen_3594, q_gen_3630, q_gen_3611) -> q_gen_3624
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 21
() -> numnodes([leaf, z]) -> 21
() -> plus([n, z, n]) -> 24
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 21
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 24
(leq([s(nn1), z])) -> BOT -> 22
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 28
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 28
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 23
}
Sat witness: Found: ((numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]), {
_bt -> s(s(s(z)))  ;  _ct -> s(s(z))  ;  e -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> node(b, node(b, node(b, leaf, leaf), leaf), leaf)
})

-------------------------------------------
Step 31, which took 0.204984 s (model generation: 0.065421,  model checking: 0.139563):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3611, q_gen_3612, q_gen_3623, q_gen_3624, q_gen_3630},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<node>(q_gen_3594, q_gen_3630, q_gen_3593) -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3630) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3630
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3611) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3611) -> q_gen_3588
<leaf, s>(q_gen_3612) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3624) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3630, q_gen_3611) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3624
<node, s>(q_gen_3594, q_gen_3630, q_gen_3588) -> q_gen_3624
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 22
() -> numnodes([leaf, z]) -> 22
() -> plus([n, z, n]) -> 25
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 22
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 25
(leq([s(nn1), z])) -> BOT -> 23
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 28
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 31
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 24
}
Sat witness: Found: ((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 -> b  ;  t1 -> node(b, node(b, node(b, node(b, leaf, leaf), leaf), leaf), leaf)  ;  t2 -> node(a, node(b, node(b, leaf, leaf), node(b, node(b, leaf, leaf), leaf)), leaf)
})

-------------------------------------------
Step 32, which took 0.036835 s (model generation: 0.034080,  model checking: 0.002755):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3611, q_gen_3612, q_gen_3623, q_gen_3624, q_gen_3630},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<node>(q_gen_3594, q_gen_3623, q_gen_3630) -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3630
<node>(q_gen_3594, q_gen_3630, q_gen_3593) -> q_gen_3630
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3611) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3611) -> q_gen_3588
<leaf, s>(q_gen_3612) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3624
<node, s>(q_gen_3594, q_gen_3623, q_gen_3624) -> q_gen_3624
<node, s>(q_gen_3594, q_gen_3630, q_gen_3588) -> q_gen_3624
<node, s>(q_gen_3594, q_gen_3630, q_gen_3611) -> q_gen_3624
}

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

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 23
() -> numnodes([leaf, z]) -> 23
() -> plus([n, z, n]) -> 26
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 23
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 26
(leq([s(nn1), z])) -> BOT -> 24
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 31
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 31
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 25
}
Sat witness: Found: ((numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]), {
_bt -> s(s(s(z)))  ;  _ct -> s(s(z))  ;  e -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 33, which took 0.078284 s (model generation: 0.077240,  model checking: 0.001044):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3610, q_gen_3612, q_gen_3623},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3623) -> q_gen_3623
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3610) -> q_gen_3588
<leaf, s>(q_gen_3612) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3610
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3603, q_gen_3604, q_gen_3605, q_gen_3609},
Q_f={q_gen_3587, q_gen_3603},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<s, s>(q_gen_3591) -> q_gen_3591
<z, z>() -> q_gen_3591
<z, s>(q_gen_3605) -> q_gen_3609
<s, z, s>(q_gen_3591) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<s, s, s>(q_gen_3587) -> q_gen_3603
<s, s, s>(q_gen_3604) -> q_gen_3603
<s, s, s>(q_gen_3603) -> q_gen_3604
<s, z, s>(q_gen_3609) -> q_gen_3604
<z, s, s>(q_gen_3609) -> q_gen_3604
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 24
() -> numnodes([leaf, z]) -> 24
() -> plus([n, z, n]) -> 26
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 24
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 26
(leq([s(nn1), z])) -> BOT -> 25
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 31
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 31
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 28
}
Sat witness: Found: ((plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]), {
_qs -> s(s(z))  ;  mm -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 34, which took 0.076971 s (model generation: 0.075962,  model checking: 0.001009):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3610, q_gen_3612, q_gen_3623, q_gen_3630},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3630) -> q_gen_3623
<node>(q_gen_3594, q_gen_3630, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3630
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3610) -> q_gen_3588
<leaf, s>(q_gen_3612) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3630, q_gen_3588) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3630, q_gen_3610) -> q_gen_3610
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3599, q_gen_3604, q_gen_3605},
Q_f={q_gen_3587},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<z, z>() -> q_gen_3591
<s, s>(q_gen_3591) -> q_gen_3599
<z, s>(q_gen_3605) -> q_gen_3599
<s, s, s>(q_gen_3587) -> q_gen_3587
<s, s, s>(q_gen_3604) -> q_gen_3587
<s, z, s>(q_gen_3591) -> q_gen_3587
<s, z, s>(q_gen_3599) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<z, s, s>(q_gen_3599) -> q_gen_3604
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 25
() -> numnodes([leaf, z]) -> 25
() -> plus([n, z, n]) -> 29
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 25
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 27
(leq([s(nn1), z])) -> BOT -> 26
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 31
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 31
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 28
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(s(s(z)))
})

-------------------------------------------
Step 35, which took 0.077459 s (model generation: 0.076510,  model checking: 0.000949):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3610, q_gen_3612, q_gen_3623, q_gen_3629},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<node>(q_gen_3594, q_gen_3629, q_gen_3593) -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3629
<node>(q_gen_3594, q_gen_3623, q_gen_3629) -> q_gen_3629
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3610) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3629, q_gen_3610) -> q_gen_3588
<leaf, s>(q_gen_3612) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3629, q_gen_3588) -> q_gen_3610
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3599, q_gen_3604, q_gen_3605},
Q_f={q_gen_3587},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<z, z>() -> q_gen_3591
<s, s>(q_gen_3591) -> q_gen_3599
<s, s>(q_gen_3599) -> q_gen_3599
<z, s>(q_gen_3605) -> q_gen_3599
<s, s, s>(q_gen_3587) -> q_gen_3587
<s, s, s>(q_gen_3604) -> q_gen_3587
<s, z, s>(q_gen_3591) -> q_gen_3587
<s, z, s>(q_gen_3599) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<z, s, s>(q_gen_3599) -> q_gen_3604
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 26
() -> numnodes([leaf, z]) -> 26
() -> plus([n, z, n]) -> 29
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 26
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 28
(leq([s(nn1), z])) -> BOT -> 27
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 31
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 31
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 31
}
Sat witness: Found: ((plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]), {
_qs -> s(z)  ;  mm -> s(z)  ;  n -> z
})

-------------------------------------------
Step 36, which took 0.078022 s (model generation: 0.077141,  model checking: 0.000881):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3610, q_gen_3612, q_gen_3623},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3623) -> q_gen_3623
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3610) -> q_gen_3588
<leaf, s>(q_gen_3612) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3610
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3598, q_gen_3604, q_gen_3605, q_gen_3609},
Q_f={q_gen_3587, q_gen_3598},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<s, s>(q_gen_3591) -> q_gen_3591
<z, z>() -> q_gen_3591
<z, s>(q_gen_3605) -> q_gen_3609
<s, z, s>(q_gen_3609) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<s, s, s>(q_gen_3587) -> q_gen_3598
<s, s, s>(q_gen_3604) -> q_gen_3598
<s, z, s>(q_gen_3591) -> q_gen_3598
<s, s, s>(q_gen_3598) -> q_gen_3604
<z, s, s>(q_gen_3609) -> q_gen_3604
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 27
() -> numnodes([leaf, z]) -> 27
() -> plus([n, z, n]) -> 30
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 27
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 29
(leq([s(nn1), z])) -> BOT -> 28
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 31
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 31
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 34
}
Sat witness: Found: ((plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]), {
_qs -> s(s(s(z)))  ;  mm -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 37, which took 0.082913 s (model generation: 0.080233,  model checking: 0.002680):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3611, q_gen_3612, q_gen_3617, q_gen_3619, q_gen_3623},
Q_f={q_gen_3588, q_gen_3611},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<z>() -> q_gen_3612
<s>(q_gen_3612) -> q_gen_3619
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3623) -> q_gen_3623
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3611) -> q_gen_3588
<leaf, s>(q_gen_3612) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3611) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3617) -> q_gen_3611
<leaf, s>(q_gen_3619) -> q_gen_3617
<node, s>(q_gen_3594, q_gen_3593, q_gen_3617) -> q_gen_3617
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3617
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3604, q_gen_3605},
Q_f={q_gen_3587},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<s, s>(q_gen_3591) -> q_gen_3591
<z, s>(q_gen_3605) -> q_gen_3591
<z, z>() -> q_gen_3591
<s, s, s>(q_gen_3587) -> q_gen_3587
<s, s, s>(q_gen_3604) -> q_gen_3587
<s, z, s>(q_gen_3591) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 28
() -> numnodes([leaf, z]) -> 28
() -> plus([n, z, n]) -> 31
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 28
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 30
(leq([s(nn1), z])) -> BOT -> 29
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 31
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 34
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 34
}
Sat witness: Found: ((numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]), {
_vs -> s(z)  ;  _ws -> s(z)  ;  _xs -> s(s(z))  ;  e -> b  ;  t1 -> leaf  ;  t2 -> leaf
})

-------------------------------------------
Step 38, which took 0.219079 s (model generation: 0.079842,  model checking: 0.139237):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3610, q_gen_3612, q_gen_3623, q_gen_3630},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3630) -> q_gen_3623
<node>(q_gen_3594, q_gen_3630, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3630
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3610) -> q_gen_3588
<leaf, s>(q_gen_3612) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3630, q_gen_3588) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3630, q_gen_3610) -> q_gen_3610
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3604, q_gen_3605, q_gen_3609},
Q_f={q_gen_3587},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<s, s>(q_gen_3591) -> q_gen_3591
<z, z>() -> q_gen_3591
<z, s>(q_gen_3605) -> q_gen_3609
<s, s, s>(q_gen_3587) -> q_gen_3587
<s, s, s>(q_gen_3604) -> q_gen_3587
<s, z, s>(q_gen_3591) -> q_gen_3587
<s, z, s>(q_gen_3609) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<z, s, s>(q_gen_3609) -> q_gen_3604
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 29
() -> numnodes([leaf, z]) -> 29
() -> plus([n, z, n]) -> 32
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 29
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 31
(leq([s(nn1), z])) -> BOT -> 30
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 32
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 34
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 37
}
Sat witness: Found: ((plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]), {
_qs -> s(s(s(z)))  ;  mm -> z  ;  n -> s(s(s(z)))
})

-------------------------------------------
Step 39, which took 0.105197 s (model generation: 0.042421,  model checking: 0.062776):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3610, q_gen_3612, q_gen_3623, q_gen_3630},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3630) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3630
<node>(q_gen_3594, q_gen_3630, q_gen_3593) -> q_gen_3630
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3610) -> q_gen_3588
<leaf, s>(q_gen_3612) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3630, q_gen_3588) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3630, q_gen_3610) -> q_gen_3610
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3604, q_gen_3605, q_gen_3609},
Q_f={q_gen_3587},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<s, s>(q_gen_3591) -> q_gen_3591
<s, s>(q_gen_3609) -> q_gen_3591
<z, z>() -> q_gen_3591
<z, s>(q_gen_3605) -> q_gen_3609
<s, s, s>(q_gen_3587) -> q_gen_3587
<s, s, s>(q_gen_3604) -> q_gen_3587
<s, z, s>(q_gen_3591) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<s, z, s>(q_gen_3609) -> q_gen_3604
<z, s, s>(q_gen_3609) -> q_gen_3604
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 30
() -> numnodes([leaf, z]) -> 30
() -> plus([n, z, n]) -> 32
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 30
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 32
(leq([s(nn1), z])) -> BOT -> 31
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 35
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 34
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 37
}
Sat witness: Found: ((numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]), {
_bt -> s(s(s(s(s(z)))))  ;  _ct -> s(s(s(s(z))))  ;  e -> b  ;  t1 -> node(b, node(b, node(b, leaf, leaf), node(b, node(b, leaf, leaf), leaf)), node(b, node(b, node(b, node(b, leaf, leaf), leaf), leaf), leaf))  ;  t2 -> node(b, leaf, node(b, node(b, node(b, leaf, leaf), leaf), node(b, node(b, leaf, leaf), leaf)))
})

-------------------------------------------
Step 40, which took 0.360578 s (model generation: 0.086198,  model checking: 0.274380):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3623},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3623) -> q_gen_3623
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3611) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3611) -> q_gen_3610
<leaf, s>(q_gen_3612) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3611
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3590, q_gen_3591, q_gen_3604, q_gen_3605},
Q_f={q_gen_3587, q_gen_3590},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<s, s>(q_gen_3591) -> q_gen_3591
<z, s>(q_gen_3605) -> q_gen_3591
<z, z>() -> q_gen_3591
<s, s, s>(q_gen_3604) -> q_gen_3587
<s, z, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<s, s, s>(q_gen_3587) -> q_gen_3590
<z, s, s>(q_gen_3591) -> q_gen_3590
<s, s, s>(q_gen_3590) -> q_gen_3604
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 31
() -> numnodes([leaf, z]) -> 31
() -> plus([n, z, n]) -> 33
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 31
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 33
(leq([s(nn1), z])) -> BOT -> 32
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 35
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 37
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 37
}
Sat witness: Found: ((numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]), {
_vs -> s(s(z))  ;  _ws -> s(s(z))  ;  _xs -> s(s(s(z)))  ;  e -> b  ;  t1 -> node(b, node(b, node(b, leaf, leaf), leaf), leaf)  ;  t2 -> node(a, node(b, node(b, leaf, leaf), node(b, leaf, leaf)), leaf)
})

-------------------------------------------
Step 41, which took 0.085779 s (model generation: 0.081643,  model checking: 0.004136):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3592, q_gen_3593, q_gen_3594, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3623},
Q_f={q_gen_3588, q_gen_3592},
Delta=
{
<leaf>() -> q_gen_3593
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3593
<node>(q_gen_3594, q_gen_3623, q_gen_3623) -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3592
<node, s>(q_gen_3594, q_gen_3623, q_gen_3592) -> q_gen_3592
<node, s>(q_gen_3594, q_gen_3623, q_gen_3611) -> q_gen_3592
<node, s>(q_gen_3594, q_gen_3593, q_gen_3611) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3623, q_gen_3610) -> q_gen_3610
<leaf, s>(q_gen_3612) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3593, q_gen_3592) -> q_gen_3611
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3604, q_gen_3605},
Q_f={q_gen_3587},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<s, s>(q_gen_3591) -> q_gen_3591
<z, s>(q_gen_3605) -> q_gen_3591
<z, z>() -> q_gen_3591
<s, s, s>(q_gen_3587) -> q_gen_3587
<s, s, s>(q_gen_3604) -> q_gen_3587
<s, z, s>(q_gen_3591) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 32
() -> numnodes([leaf, z]) -> 32
() -> plus([n, z, n]) -> 34
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 32
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 34
(leq([s(nn1), z])) -> BOT -> 33
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 38
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 37
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 37
}
Sat witness: Found: ((numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]), {
_bt -> s(s(s(s(s(s(z))))))  ;  _ct -> s(s(s(s(s(z)))))  ;  e -> b  ;  t1 -> node(a, node(b, leaf, leaf), leaf)  ;  t2 -> node(b, leaf, node(b, leaf, node(b, leaf, node(b, leaf, leaf))))
})

-------------------------------------------
Step 42, which took 0.842083 s (model generation: 0.129695,  model checking: 0.712388):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3622, q_gen_3623},
Q_f={q_gen_3588, q_gen_3622},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3623) -> q_gen_3623
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3622) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3611) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3593, q_gen_3622) -> q_gen_3610
<leaf, s>(q_gen_3612) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3610) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3611) -> q_gen_3622
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3604, q_gen_3605},
Q_f={q_gen_3587},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<s, s>(q_gen_3591) -> q_gen_3591
<z, s>(q_gen_3605) -> q_gen_3591
<z, z>() -> q_gen_3591
<s, s, s>(q_gen_3587) -> q_gen_3587
<s, s, s>(q_gen_3604) -> q_gen_3587
<s, z, s>(q_gen_3591) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 33
() -> numnodes([leaf, z]) -> 33
() -> plus([n, z, n]) -> 35
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 33
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 35
(leq([s(nn1), z])) -> BOT -> 34
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 38
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 40
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 38
}
Sat witness: Found: ((numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]), {
_vs -> s(s(s(z)))  ;  _ws -> s(s(z))  ;  _xs -> s(s(s(z)))  ;  e -> b  ;  t1 -> node(a, node(b, leaf, leaf), leaf)  ;  t2 -> node(b, node(b, node(b, leaf, leaf), leaf), node(b, node(b, node(b, leaf, leaf), leaf), leaf))
})

-------------------------------------------
Step 43, which took 0.124745 s (model generation: 0.122635,  model checking: 0.002110):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3592, q_gen_3593, q_gen_3594, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3623},
Q_f={q_gen_3588, q_gen_3592},
Delta=
{
<leaf>() -> q_gen_3593
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3593
<node>(q_gen_3594, q_gen_3623, q_gen_3623) -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3592) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3592
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3592
<node, s>(q_gen_3594, q_gen_3623, q_gen_3611) -> q_gen_3592
<node, s>(q_gen_3594, q_gen_3593, q_gen_3611) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3610
<leaf, s>(q_gen_3612) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3593, q_gen_3592) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3610) -> q_gen_3611
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3604, q_gen_3605},
Q_f={q_gen_3587},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<s, s>(q_gen_3591) -> q_gen_3591
<z, s>(q_gen_3605) -> q_gen_3591
<z, z>() -> q_gen_3591
<s, s, s>(q_gen_3587) -> q_gen_3587
<s, s, s>(q_gen_3604) -> q_gen_3587
<s, z, s>(q_gen_3591) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 34
() -> numnodes([leaf, z]) -> 34
() -> plus([n, z, n]) -> 36
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 34
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 36
(leq([s(nn1), z])) -> BOT -> 35
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 41
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 40
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 39
}
Sat witness: Found: ((numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]), {
_bt -> s(s(s(z)))  ;  _ct -> s(s(z))  ;  e -> b  ;  t1 -> node(b, node(b, leaf, leaf), leaf)  ;  t2 -> node(b, node(b, leaf, leaf), leaf)
})

-------------------------------------------
Step 44, which took 0.230877 s (model generation: 0.143322,  model checking: 0.087555):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3607, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3623},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3593
<node>(q_gen_3607, q_gen_3593, q_gen_3593) -> q_gen_3593
<b>() -> q_gen_3594
<a>() -> q_gen_3607
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3623) -> q_gen_3623
<node>(q_gen_3607, q_gen_3623, q_gen_3593) -> q_gen_3623
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3611) -> q_gen_3588
<node, s>(q_gen_3607, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3607, q_gen_3593, q_gen_3611) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3611) -> q_gen_3610
<node, s>(q_gen_3607, q_gen_3623, q_gen_3588) -> q_gen_3610
<leaf, s>(q_gen_3612) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3610) -> q_gen_3611
<node, s>(q_gen_3607, q_gen_3623, q_gen_3611) -> q_gen_3611
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3604, q_gen_3605},
Q_f={q_gen_3587},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<s, s>(q_gen_3591) -> q_gen_3591
<z, s>(q_gen_3605) -> q_gen_3591
<z, z>() -> q_gen_3591
<s, s, s>(q_gen_3587) -> q_gen_3587
<s, s, s>(q_gen_3604) -> q_gen_3587
<s, z, s>(q_gen_3591) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 35
() -> numnodes([leaf, z]) -> 35
() -> plus([n, z, n]) -> 37
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 35
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 37
(leq([s(nn1), z])) -> BOT -> 36
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 41
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 43
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 40
}
Sat witness: Found: ((numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]), {
_vs -> s(z)  ;  _ws -> z  ;  _xs -> s(z)  ;  e -> a  ;  t1 -> node(b, node(a, leaf, leaf), leaf)  ;  t2 -> leaf
})

-------------------------------------------
Step 45, which took 0.164155 s (model generation: 0.143061,  model checking: 0.021094):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3607, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3623},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3593
<b>() -> q_gen_3594
<a>() -> q_gen_3607
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3623) -> q_gen_3623
<node>(q_gen_3607, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3607, q_gen_3623, q_gen_3593) -> q_gen_3623
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3611) -> q_gen_3588
<node, s>(q_gen_3607, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3611) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3623, q_gen_3610) -> q_gen_3610
<node, s>(q_gen_3607, q_gen_3623, q_gen_3588) -> q_gen_3610
<leaf, s>(q_gen_3612) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3611
<node, s>(q_gen_3607, q_gen_3593, q_gen_3611) -> q_gen_3611
<node, s>(q_gen_3607, q_gen_3623, q_gen_3611) -> q_gen_3611
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3604, q_gen_3605},
Q_f={q_gen_3587},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<s, s>(q_gen_3591) -> q_gen_3591
<z, s>(q_gen_3605) -> q_gen_3591
<z, z>() -> q_gen_3591
<s, s, s>(q_gen_3587) -> q_gen_3587
<s, s, s>(q_gen_3604) -> q_gen_3587
<s, z, s>(q_gen_3591) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 36
() -> numnodes([leaf, z]) -> 36
() -> plus([n, z, n]) -> 38
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 36
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 38
(leq([s(nn1), z])) -> BOT -> 37
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 44
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 43
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 41
}
Sat witness: Found: ((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(b, node(a, node(a, leaf, leaf), leaf), leaf)  ;  t2 -> node(b, leaf, node(b, node(b, leaf, leaf), leaf))
})

-------------------------------------------
Step 46, which took 0.675369 s (model generation: 0.153298,  model checking: 0.522071):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3623, q_gen_3629},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3629, q_gen_3629) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3629
<node>(q_gen_3594, q_gen_3623, q_gen_3623) -> q_gen_3629
<node>(q_gen_3594, q_gen_3623, q_gen_3629) -> q_gen_3629
<node>(q_gen_3594, q_gen_3629, q_gen_3593) -> q_gen_3629
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3611) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3611) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3629, q_gen_3610) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3629, q_gen_3611) -> q_gen_3610
<leaf, s>(q_gen_3612) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3629, q_gen_3588) -> q_gen_3611
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3604, q_gen_3605},
Q_f={q_gen_3587},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<s, s>(q_gen_3591) -> q_gen_3591
<z, s>(q_gen_3605) -> q_gen_3591
<z, z>() -> q_gen_3591
<s, s, s>(q_gen_3587) -> q_gen_3587
<s, s, s>(q_gen_3604) -> q_gen_3587
<s, z, s>(q_gen_3591) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 37
() -> numnodes([leaf, z]) -> 37
() -> plus([n, z, n]) -> 39
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 37
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 39
(leq([s(nn1), z])) -> BOT -> 38
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 44
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 46
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 42
}
Sat witness: Found: ((numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]), {
_vs -> s(z)  ;  _ws -> s(s(s(s(s(z)))))  ;  _xs -> s(s(s(s(s(z)))))  ;  e -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> node(a, node(b, leaf, leaf), node(b, node(b, node(b, node(b, leaf, leaf), node(b, leaf, leaf)), leaf), node(b, leaf, node(b, node(b, leaf, leaf), leaf))))
})

-------------------------------------------
Step 47, which took 0.189815 s (model generation: 0.184596,  model checking: 0.005219):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3622, q_gen_3623},
Q_f={q_gen_3588, q_gen_3622},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3623) -> q_gen_3623
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3622) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3622) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3611) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3610
<leaf, s>(q_gen_3612) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3610) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3611) -> q_gen_3622
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3604, q_gen_3605},
Q_f={q_gen_3587},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<s, s>(q_gen_3591) -> q_gen_3591
<z, s>(q_gen_3605) -> q_gen_3591
<z, z>() -> q_gen_3591
<s, s, s>(q_gen_3587) -> q_gen_3587
<s, s, s>(q_gen_3604) -> q_gen_3587
<s, z, s>(q_gen_3591) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 38
() -> numnodes([leaf, z]) -> 38
() -> plus([n, z, n]) -> 40
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 38
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 40
(leq([s(nn1), z])) -> BOT -> 39
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 47
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 46
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 43
}
Sat witness: Found: ((numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]), {
_bt -> s(s(s(s(s(s(z))))))  ;  _ct -> s(s(s(s(s(z)))))  ;  e -> b  ;  t1 -> node(b, node(b, leaf, leaf), leaf)  ;  t2 -> node(b, node(b, leaf, leaf), node(b, leaf, leaf))
})

-------------------------------------------
Step 48, which took 0.396230 s (model generation: 0.235061,  model checking: 0.161169):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3607, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3623},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3593
<node>(q_gen_3594, q_gen_3623, q_gen_3623) -> q_gen_3593
<node>(q_gen_3607, q_gen_3623, q_gen_3593) -> q_gen_3593
<b>() -> q_gen_3594
<a>() -> q_gen_3607
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3607, q_gen_3593, q_gen_3593) -> q_gen_3623
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3611) -> q_gen_3588
<node, s>(q_gen_3607, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3607, q_gen_3593, q_gen_3611) -> q_gen_3588
<node, s>(q_gen_3607, q_gen_3623, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3611) -> q_gen_3610
<node, s>(q_gen_3607, q_gen_3623, q_gen_3611) -> q_gen_3610
<leaf, s>(q_gen_3612) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3610) -> q_gen_3611
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3604, q_gen_3605},
Q_f={q_gen_3587},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<s, s>(q_gen_3591) -> q_gen_3591
<z, s>(q_gen_3605) -> q_gen_3591
<z, z>() -> q_gen_3591
<s, s, s>(q_gen_3587) -> q_gen_3587
<s, s, s>(q_gen_3604) -> q_gen_3587
<s, z, s>(q_gen_3591) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 39
() -> numnodes([leaf, z]) -> 39
() -> plus([n, z, n]) -> 41
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 39
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 41
(leq([s(nn1), z])) -> BOT -> 40
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 47
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 49
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 44
}
Sat witness: Found: ((numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]), {
_vs -> s(z)  ;  _ws -> s(z)  ;  _xs -> s(s(z))  ;  e -> b  ;  t1 -> node(b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), leaf)  ;  t2 -> node(b, node(a, node(a, leaf, leaf), node(b, node(a, leaf, leaf), leaf)), leaf)
})

-------------------------------------------
Step 49, which took 0.289578 s (model generation: 0.273968,  model checking: 0.015610):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3607, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3623},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3593
<node>(q_gen_3607, q_gen_3623, q_gen_3593) -> q_gen_3593
<b>() -> q_gen_3594
<a>() -> q_gen_3607
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3623) -> q_gen_3623
<node>(q_gen_3607, q_gen_3593, q_gen_3593) -> q_gen_3623
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3611) -> q_gen_3588
<node, s>(q_gen_3607, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3607, q_gen_3593, q_gen_3611) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3611) -> q_gen_3610
<node, s>(q_gen_3607, q_gen_3623, q_gen_3588) -> q_gen_3610
<leaf, s>(q_gen_3612) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3610) -> q_gen_3611
<node, s>(q_gen_3607, q_gen_3623, q_gen_3611) -> q_gen_3611
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3604, q_gen_3605},
Q_f={q_gen_3587},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<s, s>(q_gen_3591) -> q_gen_3591
<z, s>(q_gen_3605) -> q_gen_3591
<z, z>() -> q_gen_3591
<s, s, s>(q_gen_3587) -> q_gen_3587
<s, s, s>(q_gen_3604) -> q_gen_3587
<s, z, s>(q_gen_3591) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 40
() -> numnodes([leaf, z]) -> 40
() -> plus([n, z, n]) -> 42
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 40
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 42
(leq([s(nn1), z])) -> BOT -> 41
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 50
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 49
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 45
}
Sat witness: Found: ((numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]), {
_bt -> s(s(s(s(s(z)))))  ;  _ct -> s(s(s(s(z))))  ;  e -> a  ;  t1 -> node(b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), leaf)  ;  t2 -> node(a, node(b, leaf, leaf), node(b, node(b, leaf, leaf), node(a, node(b, leaf, leaf), leaf)))
})

-------------------------------------------
Step 50, which took 0.339551 s (model generation: 0.311453,  model checking: 0.028098):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3607, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3623},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3593
<node>(q_gen_3607, q_gen_3623, q_gen_3593) -> q_gen_3593
<b>() -> q_gen_3594
<a>() -> q_gen_3607
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3623) -> q_gen_3623
<node>(q_gen_3607, q_gen_3593, q_gen_3593) -> q_gen_3623
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3611) -> q_gen_3588
<node, s>(q_gen_3607, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3607, q_gen_3593, q_gen_3611) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3611) -> q_gen_3610
<node, s>(q_gen_3607, q_gen_3623, q_gen_3588) -> q_gen_3610
<node, s>(q_gen_3607, q_gen_3623, q_gen_3611) -> q_gen_3610
<leaf, s>(q_gen_3612) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3610) -> q_gen_3611
<node, s>(q_gen_3607, q_gen_3593, q_gen_3610) -> q_gen_3611
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3604, q_gen_3605},
Q_f={q_gen_3587},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<s, s>(q_gen_3591) -> q_gen_3591
<z, s>(q_gen_3605) -> q_gen_3591
<z, z>() -> q_gen_3591
<s, s, s>(q_gen_3587) -> q_gen_3587
<s, s, s>(q_gen_3604) -> q_gen_3587
<s, z, s>(q_gen_3591) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 41
() -> numnodes([leaf, z]) -> 41
() -> plus([n, z, n]) -> 43
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 41
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 43
(leq([s(nn1), z])) -> BOT -> 42
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 50
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 52
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 46
}
Sat witness: Found: ((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 -> a  ;  t1 -> leaf  ;  t2 -> node(b, node(a, node(b, leaf, leaf), leaf), leaf)
})

-------------------------------------------
Step 51, which took 0.478977 s (model generation: 0.438032,  model checking: 0.040945):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3607, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3623},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3593
<node>(q_gen_3607, q_gen_3623, q_gen_3593) -> q_gen_3593
<b>() -> q_gen_3594
<a>() -> q_gen_3607
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3623) -> q_gen_3623
<node>(q_gen_3607, q_gen_3593, q_gen_3593) -> q_gen_3623
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3611) -> q_gen_3588
<node, s>(q_gen_3607, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3607, q_gen_3593, q_gen_3610) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3611) -> q_gen_3610
<node, s>(q_gen_3607, q_gen_3623, q_gen_3588) -> q_gen_3610
<leaf, s>(q_gen_3612) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3610) -> q_gen_3611
<node, s>(q_gen_3607, q_gen_3593, q_gen_3611) -> q_gen_3611
<node, s>(q_gen_3607, q_gen_3623, q_gen_3611) -> q_gen_3611
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3604, q_gen_3605},
Q_f={q_gen_3587},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<s, s>(q_gen_3591) -> q_gen_3591
<z, s>(q_gen_3605) -> q_gen_3591
<z, z>() -> q_gen_3591
<s, s, s>(q_gen_3587) -> q_gen_3587
<s, s, s>(q_gen_3604) -> q_gen_3587
<s, z, s>(q_gen_3591) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 42
() -> numnodes([leaf, z]) -> 42
() -> plus([n, z, n]) -> 44
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 42
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 44
(leq([s(nn1), z])) -> BOT -> 43
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 53
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 52
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 47
}
Sat witness: Found: ((numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]), {
_bt -> s(s(s(z)))  ;  _ct -> s(s(z))  ;  e -> b  ;  t1 -> node(b, node(b, node(a, leaf, leaf), node(a, leaf, leaf)), leaf)  ;  t2 -> node(a, leaf, leaf)
})

-------------------------------------------
Step 52, which took 0.541642 s (model generation: 0.492293,  model checking: 0.049349):

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

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  numnodes -> 
{{{
Q={q_gen_3588, q_gen_3593, q_gen_3594, q_gen_3610, q_gen_3611, q_gen_3612, q_gen_3623, q_gen_3630},
Q_f={q_gen_3588},
Delta=
{
<leaf>() -> q_gen_3593
<a>() -> q_gen_3594
<b>() -> q_gen_3594
<s>(q_gen_3612) -> q_gen_3612
<z>() -> q_gen_3612
<node>(q_gen_3594, q_gen_3593, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3623) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3630) -> q_gen_3623
<node>(q_gen_3594, q_gen_3630, q_gen_3593) -> q_gen_3623
<node>(q_gen_3594, q_gen_3623, q_gen_3593) -> q_gen_3630
<leaf, z>() -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3588) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3610) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3623, q_gen_3611) -> q_gen_3588
<node, s>(q_gen_3594, q_gen_3593, q_gen_3611) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3623, q_gen_3610) -> q_gen_3610
<node, s>(q_gen_3594, q_gen_3630, q_gen_3588) -> q_gen_3610
<leaf, s>(q_gen_3612) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3623, q_gen_3588) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3630, q_gen_3610) -> q_gen_3611
<node, s>(q_gen_3594, q_gen_3630, q_gen_3611) -> q_gen_3611
}

Datatype: <elt_bin_tree, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_3587, q_gen_3591, q_gen_3604, q_gen_3605},
Q_f={q_gen_3587},
Delta=
{
<s>(q_gen_3605) -> q_gen_3605
<z>() -> q_gen_3605
<s, s>(q_gen_3591) -> q_gen_3591
<z, s>(q_gen_3605) -> q_gen_3591
<z, z>() -> q_gen_3591
<s, s, s>(q_gen_3587) -> q_gen_3587
<s, s, s>(q_gen_3604) -> q_gen_3587
<s, z, s>(q_gen_3591) -> q_gen_3587
<z, s, s>(q_gen_3591) -> q_gen_3587
<z, z, z>() -> q_gen_3587
<z, z, s>(q_gen_3605) -> q_gen_3604
}

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

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

Teacher's answer:
New clause system:
{
() -> leq([z, n2]) -> 43
() -> numnodes([leaf, z]) -> 43
() -> plus([n, z, n]) -> 45
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 43
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 45
(leq([s(nn1), z])) -> BOT -> 44
(numnodes([t1, _bt]) /\ numnodes([node(e, t1, t2), _ct])) -> leq([_bt, _ct]) -> 53
(numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]) -> 55
(plus([n, mm, _qs])) -> plus([n, s(mm), s(_qs)]) -> 48
}
Sat witness: Found: ((numnodes([t1, _vs]) /\ numnodes([t2, _ws]) /\ plus([_vs, _ws, _xs])) -> numnodes([node(e, t1, t2), s(_xs)]), {
_vs -> s(s(z))  ;  _ws -> z  ;  _xs -> s(s(z))  ;  e -> b  ;  t1 -> node(a, node(b, node(b, leaf, leaf), node(b, node(b, leaf, leaf), leaf)), leaf)  ;  t2 -> leaf
})

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