Solving ../../benchmarks/smtlib/true/tree_flip_preserves_size.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: Some(60.) (sec)
Teacher_type: Checks all clauses every time
Approximation method: remove every clause that can be safely removed



Learning problem is:

env: {
elt -> {a, b}  ;  etree -> {leaf, node}  ;  nat -> {s, z}
}
definition:
{
(flip, F:
{
flip(leaf, leaf) <= True
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)
}
eq_etree(_uda, _vda) <= flip(_tda, _uda) /\ flip(_tda, _vda)
)
(plus, F:
{
plus(n, z, n) <= True
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)
}
eq_nat(_zda, _aea) <= plus(_xda, _yda, _aea) /\ plus(_xda, _yda, _zda)
)
(numnodes, F:
{
numnodes(leaf, z) <= True
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)
}
eq_nat(_fea, _gea) <= numnodes(_eea, _fea) /\ numnodes(_eea, _gea)
)
}

properties:
{
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)
}


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

Clause system for inference is:

{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}


Solving took 60.235544 seconds.
Maybe:  timeout during learnerLast solver state:

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) <= True
flip(node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)) <= True
flip(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= True
flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True
flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) <= True
flip(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))) <= True
flip(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))) <= True
flip(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf)))) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= True
plus(s(s(z)), s(z), s(s(s(z)))) <= True
plus(s(s(z)), z, s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))
flip(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf))
flip(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, node(a, node(a, leaf, leaf), leaf), leaf))) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, node(a, leaf, leaf), leaf), leaf))
flip(node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), node(a, node(a, node(a, leaf, leaf), leaf), leaf)) <= flip(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), leaf)), node(a, node(a, leaf, node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(z))
False <= numnodes(node(a, leaf, leaf), s(s(s(s(z)))))
False <= numnodes(node(a, leaf, leaf), s(s(z)))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z))))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(s(z)))))
False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
numnodes(node(a, leaf, node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z)))
numnodes(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(s(z)))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(s(z)))
False <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(z))
numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z))
numnodes(node(a, leaf, node(a, node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))), s(s(s(z)))) <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(s(z)))
False <= plus(s(z), z, s(s(z)))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z))))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_2(leaf) <= True
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_1)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_2)
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1) /\ _r_2(x_0_2)
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_1) /\ _r_3(x_0_2)
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_0_1) /\ flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1)
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_0_2) /\ flip(x_0_1, x_1_2)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  _r_2(leaf) <= True
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_1)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_2)
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1) /\ _r_2(x_0_2)
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_1) /\ _r_3(x_0_2)
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1) /\ _r_3(x_0_2)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1) /\ numnodes(x_0_1, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_2) /\ numnodes(x_0_2, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|






-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006547 s (model generation: 0.006485,  model checking: 0.000062):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
Yes: {

}

numnodes(leaf, z) <= True  :
Yes: {

}

plus(n, z, n) <= True  :
Yes: {
n -> z
}

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
No: ()

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
No: ()

numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)  :
No: ()

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
No: ()


-------------------------------------------
Step 1, which took 0.006821 s (model generation: 0.006738,  model checking: 0.000083):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
numnodes(leaf, z) <= True
plus(z, z, z) <= True
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  flip(leaf, leaf) <= True
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  numnodes(leaf, z) <= True
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
Yes: {
n -> s(_xyqdp_0)
}

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
No: ()

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
Yes: {
_rda -> leaf  ;  _sda -> leaf  ;  t1 -> leaf  ;  t2 -> leaf
}

numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)  :
Yes: {
_bea -> z  ;  _cea -> z  ;  _dea -> z  ;  t1 -> leaf  ;  t2 -> leaf
}

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
Yes: {
_wda -> z  ;  mm -> z  ;  n -> z
}


-------------------------------------------
Step 2, which took 0.009474 s (model generation: 0.009370,  model checking: 0.000104):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  plus(s(x_0_0), z, s(x_2_0)) <= True
  plus(z, s(x_1_0), s(x_2_0)) <= True
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
Yes: {
_hea -> s(z)  ;  _iea -> node(_lzqdp_0, _lzqdp_1, _lzqdp_2)  ;  _jea -> s(s(_wzqdp_0))  ;  t -> node(_nzqdp_0, _nzqdp_1, _nzqdp_2)
}

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
No: ()

numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)  :
No: ()

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
Yes: {
_wda -> s(_ozqdp_0)  ;  mm -> z  ;  n -> s(_qzqdp_0)
}


-------------------------------------------
Step 3, which took 0.010769 s (model generation: 0.010580,  model checking: 0.000189):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= numnodes(node(a, leaf, leaf), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_2, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  plus(s(x_0_0), z, s(x_2_0)) <= True
  plus(z, s(x_1_0), s(x_2_0)) <= True
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
Yes: {
_hea -> s(z)  ;  _iea -> node(_yzqdp_0, _yzqdp_1, node(_zardp_0, _zardp_1, leaf))  ;  _jea -> s(s(z))  ;  t -> node(_aardp_0, _aardp_1, leaf)
}

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
No: ()

numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)  :
Yes: {
_bea -> s(z)  ;  _cea -> z  ;  _dea -> s(_nardp_0)  ;  t1 -> node(_oardp_0, _oardp_1, leaf)  ;  t2 -> leaf
}

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
No: ()


-------------------------------------------
Step 4, which took 0.011485 s (model generation: 0.011295,  model checking: 0.000190):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))) /\ numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z)))
False <= numnodes(node(a, leaf, leaf), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  plus(s(x_0_0), z, s(x_2_0)) <= True
  plus(z, s(x_1_0), s(x_2_0)) <= True
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
Yes: {
_hea -> s(s(z))  ;  _iea -> node(_mbrdp_0, leaf, _mbrdp_2)  ;  _jea -> s(z)  ;  t -> node(_obrdp_0, node(_ncrdp_0, leaf, _ncrdp_2), _obrdp_2)
}

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
No: ()

numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)  :
Yes: {
_bea -> z  ;  _cea -> s(z)  ;  _dea -> s(_wbrdp_0)  ;  t1 -> leaf  ;  t2 -> node(_ybrdp_0, leaf, _ybrdp_2)
}

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
No: ()


-------------------------------------------
Step 5, which took 0.012984 s (model generation: 0.012161,  model checking: 0.000823):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= numnodes(node(a, leaf, leaf), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_2)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_2, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  plus(s(x_0_0), z, s(x_2_0)) <= True
  plus(z, s(x_1_0), s(x_2_0)) <= True
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
Yes: {
_hea -> s(s(z))  ;  _iea -> node(_edrdp_0, leaf, leaf)  ;  _jea -> s(z)  ;  t -> node(_gdrdp_0, leaf, node(_wgrdp_0, leaf, _wgrdp_2))
}

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
No: ()

numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)  :
Yes: {
_bea -> z  ;  _cea -> s(z)  ;  _dea -> s(s(_zhrdp_0))  ;  t1 -> leaf  ;  t2 -> node(_terdp_0, leaf, leaf)
}

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
No: ()


-------------------------------------------
Step 6, which took 0.027281 s (model generation: 0.025785,  model checking: 0.001496):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= numnodes(node(a, leaf, leaf), s(s(z)))
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  _r_1(leaf, z) <= True
  _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  plus(s(x_0_0), z, s(x_2_0)) <= True
  plus(z, s(x_1_0), s(x_2_0)) <= True
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
Yes: {
_hea -> s(s(z))  ;  _iea -> node(_rirdp_0, leaf, node(_dmrdp_0, leaf, leaf))  ;  _jea -> s(s(s(_qnrdp_0)))  ;  t -> node(_tirdp_0, node(_bmrdp_0, leaf, leaf), leaf)
}

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
No: ()

numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)  :
No: ()

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
No: ()


-------------------------------------------
Step 7, which took 0.026593 s (model generation: 0.025953,  model checking: 0.000640):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) /\ numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
False <= numnodes(node(a, leaf, leaf), s(s(z)))
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_2)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  _r_1(leaf, z) <= True
  _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  plus(s(x_0_0), z, s(x_2_0)) <= True
  plus(z, s(x_1_0), s(x_2_0)) <= True
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
Yes: {
_hea -> s(s(z))  ;  _iea -> node(_aordp_0, _aordp_1, node(_irrdp_0, _irrdp_1, leaf))  ;  _jea -> s(s(s(_urrdp_0)))  ;  t -> node(_cordp_0, node(_grrdp_0, leaf, leaf), node(_krrdp_0, leaf, leaf))
}

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
Yes: {
_rda -> leaf  ;  _sda -> node(_cprdp_0, _cprdp_1, leaf)  ;  t1 -> node(_dprdp_0, leaf, leaf)  ;  t2 -> leaf
}

numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)  :
No: ()

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
No: ()


-------------------------------------------
Step 8, which took 0.027636 s (model generation: 0.026641,  model checking: 0.000995):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= numnodes(node(a, leaf, leaf), s(s(z)))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_2, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  plus(s(x_0_0), z, s(x_2_0)) <= True
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_2_0)
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
Yes: {
_hea -> s(s(z))  ;  _iea -> node(_asrdp_0, leaf, node(_ywrdp_0, leaf, leaf))  ;  _jea -> s(z)  ;  t -> node(_csrdp_0, node(_xwrdp_0, leaf, leaf), leaf)
}

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
No: ()

numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)  :
Yes: {
_bea -> s(z)  ;  _cea -> z  ;  _dea -> s(s(_mwrdp_0))  ;  t1 -> node(_cvrdp_0, leaf, leaf)  ;  t2 -> leaf
}

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
Yes: {
_wda -> s(z)  ;  mm -> s(_pvrdp_0)  ;  n -> z
}


-------------------------------------------
Step 9, which took 0.073258 s (model generation: 0.071969,  model checking: 0.001289):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= numnodes(node(a, leaf, leaf), s(s(z)))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= plus(s(z), z, s(s(z)))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= True
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_2, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= True
  _r_1(z, z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  plus(s(x_0_0), z, s(x_2_0)) <= True
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
Yes: {
_hea -> s(z)  ;  _iea -> node(_basdp_0, node(_nfsdp_0, leaf, leaf), node(_gesdp_0, leaf, leaf))  ;  _jea -> s(s(_eesdp_0))  ;  t -> node(_dasdp_0, node(_fesdp_0, leaf, leaf), node(_ofsdp_0, leaf, leaf))
}

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
No: ()

numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)  :
Yes: {
_bea -> z  ;  _cea -> s(s(z))  ;  _dea -> s(s(s(_xfsdp_0)))  ;  t1 -> leaf  ;  t2 -> node(_kcsdp_0, leaf, node(_jgsdp_0, leaf, leaf))
}

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
No: ()


-------------------------------------------
Step 10, which took 0.102623 s (model generation: 0.101081,  model checking: 0.001542):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, leaf, leaf), s(s(z)))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= plus(s(z), z, s(s(z)))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z))))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  _r_2(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_2, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  plus(s(x_0_0), z, s(x_2_0)) <= True
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
Yes: {
_hea -> s(s(s(_ansdp_0)))  ;  _iea -> node(_wgsdp_0, leaf, node(_kmsdp_0, leaf, leaf))  ;  _jea -> s(s(z))  ;  t -> node(_ygsdp_0, node(_imsdp_0, leaf, leaf), leaf)
}

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
No: ()

numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)  :
No: ()

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
No: ()


-------------------------------------------
Step 11, which took 0.093288 s (model generation: 0.091890,  model checking: 0.001398):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, leaf, leaf), s(s(z)))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z))))
False <= plus(s(z), z, s(s(z)))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z))))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  _r_2(leaf, s(x_1_0)) <= True
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ numnodes(x_0_1, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_2, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
Yes: {
_hea -> s(s(z))  ;  _iea -> node(_yosdp_0, node(_tusdp_0, leaf, leaf), leaf)  ;  _jea -> s(z)  ;  t -> node(_apsdp_0, leaf, node(_susdp_0, leaf, leaf))
}

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
No: ()

numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)  :
Yes: {
_bea -> s(z)  ;  _cea -> s(z)  ;  _dea -> s(s(_sysdp_0))  ;  t1 -> node(_mtsdp_0, _mtsdp_1, leaf)  ;  t2 -> node(_ntsdp_0, leaf, leaf)
}

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
No: ()


-------------------------------------------
Step 12, which took 0.272250 s (model generation: 0.270269,  model checking: 0.001981):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, leaf, leaf), s(s(z)))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z))))
False <= plus(s(z), z, s(s(z)))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z))))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  _r_2(leaf, z) <= True
  _r_2(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
  _r_3(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0)
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ _r_2(x_0_2, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_2, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= True
  _r_1(z, z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
Yes: {
_hea -> s(s(s(_hktdp_0)))  ;  _iea -> node(_xzsdp_0, node(_dktdp_0, leaf, leaf), node(_bktdp_0, leaf, leaf))  ;  _jea -> s(s(z))  ;  t -> node(_zzsdp_0, node(_aktdp_0, leaf, leaf), node(_yjtdp_0, leaf, leaf))
}

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
No: ()

numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)  :
Yes: {
_bea -> z  ;  _cea -> s(s(s(_altdp_0)))  ;  _dea -> s(s(_uktdp_0))  ;  t1 -> leaf  ;  t2 -> node(_cctdp_0, node(_vktdp_0, _vktdp_1, node(_zktdp_0, _zktdp_1, _zktdp_2)), leaf)
}

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
No: ()


-------------------------------------------
Step 13, which took 0.419567 s (model generation: 0.407901,  model checking: 0.011666):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, leaf, leaf), s(s(z)))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z))))
numnodes(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(s(z)))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(s(z)))
False <= plus(s(z), z, s(s(z)))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z))))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_2(leaf) <= True
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_0_2) /\ flip(x_0_1, x_1_2)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= True
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1) /\ _r_3(x_0_2)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1) /\ numnodes(x_0_1, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_2, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
Yes: {
_hea -> s(z)  ;  _iea -> node(_lltdp_0, node(_maudp_0, _maudp_1, _maudp_2), node(_icudp_0, _icudp_1, leaf))  ;  _jea -> s(s(_kgudp_0))  ;  t -> node(_nltdp_0, node(_jcudp_0, leaf, leaf), leaf)
}

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
Yes: {
_rda -> node(_umtdp_0, _umtdp_1, node(_idudp_0, _idudp_1, leaf))  ;  _sda -> leaf  ;  t1 -> leaf  ;  t2 -> node(_xmtdp_0, node(_hdudp_0, leaf, leaf), leaf)
}

numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)  :
No: ()

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
No: ()


-------------------------------------------
Step 14, which took 0.837997 s (model generation: 0.599579,  model checking: 0.238418):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
flip(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= True
flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, leaf, leaf), s(s(z)))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z))))
numnodes(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(s(z)))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(s(z)))
False <= plus(s(z), z, s(s(z)))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z))))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_2(leaf, leaf) <= True
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1)
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_0_2, x_1_1) /\ flip(x_0_1, x_1_2)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= True
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1) /\ _r_3(x_0_2)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1) /\ numnodes(x_0_1, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_2) /\ numnodes(x_0_2, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
No: ()

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
Yes: {
_rda -> node(_duvdp_0, leaf, node(_auxdp_0, leaf, leaf))  ;  _sda -> node(_euvdp_0, leaf, node(_auxdp_0, leaf, leaf))  ;  t1 -> node(_fuvdp_0, node(_ztxdp_0, leaf, leaf), leaf)  ;  t2 -> node(_guvdp_0, node(_ztxdp_0, leaf, leaf), leaf)
}

numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)  :
No: ()

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
No: ()


-------------------------------------------
Step 15, which took 0.727732 s (model generation: 0.654732,  model checking: 0.073000):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
flip(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= True
flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True
flip(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf)))) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, leaf, leaf), s(s(z)))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z))))
numnodes(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(s(z)))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(s(z)))
False <= plus(s(z), z, s(s(z)))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z))))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  _r_2(leaf, s(x_1_0)) <= True
  _r_3(leaf, z) <= True
  _r_3(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0)
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ numnodes(x_0_1, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1, x_1_0) /\ _r_3(x_0_2, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
Yes: {
_hea -> s(s(s(z)))  ;  _iea -> node(_zafep_0, node(_bdgep_0, leaf, leaf), node(_zcgep_0, leaf, leaf))  ;  _jea -> s(s(s(s(_degep_0))))  ;  t -> node(_bbfep_0, node(_edgep_0, leaf, leaf), node(_cdgep_0, leaf, leaf))
}

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
No: ()

numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)  :
Yes: {
_bea -> s(s(s(z)))  ;  _cea -> s(z)  ;  _dea -> s(z)  ;  t1 -> node(_jtfep_0, node(_wawep_0, node(_xdgep_0, leaf, leaf), leaf), leaf)  ;  t2 -> node(_ktfep_0, leaf, leaf)
}

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
No: ()


-------------------------------------------
Step 16, which took 1.182908 s (model generation: 1.170405,  model checking: 0.012503):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
flip(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= True
flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True
flip(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf)))) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(s(z)))))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, leaf, leaf), s(s(z)))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z))))
numnodes(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(s(z)))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(s(z)))
numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z))
False <= plus(s(z), z, s(s(z)))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z))))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_2(leaf, leaf) <= True
  _r_2(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_0_1)
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= True
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_0_1, x_1_2) /\ _r_2(x_0_2, x_1_1)
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_0_2, x_1_1) /\ flip(x_0_1, x_1_2)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= True
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1) /\ _r_3(x_0_2)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1) /\ numnodes(x_0_1, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_2, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
Yes: {
_hea -> s(z)  ;  _iea -> node(_zbwep_0, node(_wexep_0, _wexep_1, _wexep_2), node(_wexep_0, _wexep_1, _wexep_2))  ;  _jea -> s(s(_oxwep_0))  ;  t -> node(_bcwep_0, node(_vexep_0, node(_vywep_0, _vywep_1, _vywep_2), _vexep_2), node(_vexep_0, node(_vywep_0, _vywep_1, _vywep_2), _vexep_2))
}

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
Yes: {
_rda -> node(_qfwep_0, node(_hcxep_0, _hcxep_1, _hcxep_2), leaf)  ;  _sda -> leaf  ;  t1 -> leaf  ;  t2 -> node(_tfwep_0, leaf, node(_gcxep_0, node(_vywep_0, _vywep_1, _vywep_2), _gcxep_2))
}

numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)  :
No: ()

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
No: ()


-------------------------------------------
Step 17, which took 1.951296 s (model generation: 1.938737,  model checking: 0.012559):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
flip(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= True
flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True
flip(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf)))) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
flip(node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), node(a, node(a, node(a, leaf, leaf), leaf), leaf)) <= flip(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(s(z)))))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= flip(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(z))
False <= numnodes(node(a, leaf, leaf), s(s(z)))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z))))
numnodes(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(s(z)))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(s(z)))
numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z))
False <= plus(s(z), z, s(s(z)))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z))))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_2(leaf, leaf) <= True
  _r_2(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_2)
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= True
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_0_1, x_1_2) /\ _r_2(x_0_2, x_1_1)
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_0_2, x_1_1) /\ flip(x_0_1, x_1_2)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= True
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1) /\ _r_3(x_0_2)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1) /\ numnodes(x_0_1, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_2, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
Yes: {
_hea -> s(z)  ;  _iea -> node(_nkyep_0, node(_amzep_0, _amzep_1, node(_zfzep_0, _zfzep_1, _zfzep_2)), node(_xlzep_0, leaf, leaf))  ;  _jea -> s(s(_sezep_0))  ;  t -> node(_pkyep_0, node(_wlzep_0, leaf, leaf), node(_zlzep_0, _zlzep_1, _zlzep_2))
}

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
Yes: {
_rda -> node(_umyep_0, node(_ljzep_0, _ljzep_1, node(_zfzep_0, _zfzep_1, _zfzep_2)), leaf)  ;  _sda -> leaf  ;  t1 -> leaf  ;  t2 -> node(_xmyep_0, leaf, node(_kjzep_0, _kjzep_1, _kjzep_2))
}

numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)  :
No: ()

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
No: ()


-------------------------------------------
Step 18, which took 3.143302 s (model generation: 3.131062,  model checking: 0.012240):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
flip(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= True
flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True
flip(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf)))) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
flip(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf))
flip(node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), node(a, node(a, node(a, leaf, leaf), leaf), leaf)) <= flip(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(s(z)))))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(z))
False <= numnodes(node(a, leaf, leaf), s(s(z)))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z))))
numnodes(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(s(z)))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(s(z)))
numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z))
False <= plus(s(z), z, s(s(z)))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z))))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_2(leaf) <= True
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_1)
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= True
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_0_2) /\ flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= True
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1) /\ _r_3(x_0_2)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1) /\ numnodes(x_0_1, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_2, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
Yes: {
_hea -> s(z)  ;  _iea -> node(_hqafp_0, node(_fnbfp_0, leaf, node(_iibfp_0, leaf, leaf)), node(_qkbfp_0, leaf, leaf))  ;  _jea -> s(s(_ogbfp_0))  ;  t -> node(_jqafp_0, node(_pkbfp_0, leaf, leaf), node(_enbfp_0, node(_hibfp_0, leaf, leaf), leaf))
}

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
Yes: {
_rda -> node(_csafp_0, node(_blbfp_0, leaf, node(_iibfp_0, leaf, leaf)), leaf)  ;  _sda -> leaf  ;  t1 -> leaf  ;  t2 -> node(_fsafp_0, leaf, node(_zkbfp_0, node(_hibfp_0, leaf, leaf), leaf))
}

numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)  :
No: ()

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
No: ()


-------------------------------------------
Step 19, which took 3.653218 s (model generation: 3.639375,  model checking: 0.013843):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
flip(node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)) <= True
flip(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= True
flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True
flip(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf)))) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
flip(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf))
flip(node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), node(a, node(a, node(a, leaf, leaf), leaf), leaf)) <= flip(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(s(z)))))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(z))
False <= numnodes(node(a, leaf, leaf), s(s(z)))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z))))
numnodes(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(s(z)))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(s(z)))
numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z))
False <= plus(s(z), z, s(s(z)))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z))))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= True
  _r_3(leaf) <= True
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1)
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_0_1) /\ _r_3(x_0_2) /\ flip(x_0_1, x_1_2)
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_1) /\ flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= True
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1) /\ _r_2(x_0_2)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1) /\ numnodes(x_0_1, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_2, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
Yes: {
_hea -> s(z)  ;  _iea -> node(_urcfp_0, node(_gtdfp_0, _gtdfp_1, _gtdfp_2), node(_tgefp_0, leaf, node(_wydfp_0, leaf, leaf)))  ;  _jea -> s(s(_zydfp_0))  ;  t -> node(_wrcfp_0, node(_ugefp_0, node(_vydfp_0, leaf, leaf), leaf), leaf)
}

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
Yes: {
_rda -> node(_hvcfp_0, leaf, leaf)  ;  _sda -> node(_ivcfp_0, node(_qbefp_0, node(_fvdfp_0, _fvdfp_1, _fvdfp_2), leaf), leaf)  ;  t1 -> node(_jvcfp_0, leaf, node(_pbefp_0, leaf, leaf))  ;  t2 -> node(_kvcfp_0, leaf, leaf)
}

numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)  :
No: ()

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
No: ()


-------------------------------------------
Step 20, which took 4.724367 s (model generation: 4.293218,  model checking: 0.431149):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
flip(node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)) <= True
flip(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= True
flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True
flip(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf)))) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
flip(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf))
flip(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, node(a, node(a, leaf, leaf), leaf), leaf))) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, node(a, leaf, leaf), leaf), leaf))
flip(node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), node(a, node(a, node(a, leaf, leaf), leaf), leaf)) <= flip(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(s(z)))))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(z))
False <= flip(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(z))
False <= numnodes(node(a, leaf, leaf), s(s(z)))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z))))
numnodes(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(s(z)))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(s(z)))
numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z))
False <= plus(s(z), z, s(s(z)))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z))))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= True
  _r_3(leaf) <= True
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1)
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_0_1) /\ _r_3(x_0_2) /\ flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1)
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_1) /\ flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= True
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1) /\ _r_2(x_0_2)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1) /\ numnodes(x_0_1, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2) /\ numnodes(x_0_2, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
Yes: {
_hea -> s(z)  ;  _iea -> node(_dgffp_0, node(_bkkfp_0, leaf, node(_hkhfp_0, leaf, leaf)), node(_bkkfp_0, leaf, node(_hkhfp_0, leaf, leaf)))  ;  _jea -> s(s(_djhfp_0))  ;  t -> node(_fgffp_0, node(_akkfp_0, node(_gkhfp_0, leaf, leaf), leaf), node(_akkfp_0, node(_gkhfp_0, leaf, leaf), leaf))
}

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
Yes: {
_rda -> node(_gmffp_0, leaf, node(_yvifp_0, leaf, leaf))  ;  _sda -> node(_hmffp_0, leaf, leaf)  ;  t1 -> node(_imffp_0, leaf, leaf)  ;  t2 -> node(_jmffp_0, node(_awifp_0, leaf, leaf), leaf)
}

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
Yes: {
_wda -> s(s(z))  ;  mm -> z  ;  n -> s(s(z))
}


-------------------------------------------
Step 21, which took 5.200997 s (model generation: 5.197703,  model checking: 0.003294):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
flip(node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)) <= True
flip(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= True
flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True
flip(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))) <= True
flip(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf)))) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
flip(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf))
flip(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, node(a, node(a, leaf, leaf), leaf), leaf))) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, node(a, leaf, leaf), leaf), leaf))
flip(node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), node(a, node(a, node(a, leaf, leaf), leaf), leaf)) <= flip(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(s(z)))))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(z))
False <= flip(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(z))
False <= numnodes(node(a, leaf, leaf), s(s(z)))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z))))
False <= numnodes(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z)))
numnodes(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(s(z)))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(s(z)))
False <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(z))
numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z))
plus(s(s(z)), s(z), s(s(s(z)))) <= plus(s(s(z)), z, s(s(z)))
False <= plus(s(z), z, s(s(z)))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z))))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_2(leaf) <= True
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_1)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_2)
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1)
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_1) /\ flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  _r_2(leaf) <= True
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_1)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_2)
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1)
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1) /\ _r_3(x_0_2)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1) /\ numnodes(x_0_1, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_2, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
Yes: {
_hea -> s(z)  ;  _iea -> node(_cbufp_0, node(_nzufp_0, leaf, node(_gavfp_0, node(_twufp_0, node(_bavfp_0, leaf, node(_mtufp_0, leaf, leaf)), leaf), leaf)), node(_zwufp_0, leaf, leaf))  ;  _jea -> s(s(_jrufp_0))  ;  t -> node(_ebufp_0, node(_ywufp_0, leaf, leaf), node(_ozufp_0, node(_favfp_0, leaf, node(_uwufp_0, leaf, node(_cavfp_0, node(_ntufp_0, leaf, leaf), leaf))), leaf))
}

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
Yes: {
_rda -> node(_xcufp_0, leaf, leaf)  ;  _sda -> leaf  ;  t1 -> leaf  ;  t2 -> node(_adufp_0, leaf, leaf)
}

numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)  :
Yes: {
_bea -> s(z)  ;  _cea -> s(z)  ;  _dea -> s(s(_myufp_0))  ;  t1 -> node(_iqufp_0, node(_otufp_0, leaf, leaf), leaf)  ;  t2 -> node(_jqufp_0, leaf, leaf)
}

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
No: ()


-------------------------------------------
Step 22, which took 7.052244 s (model generation: 6.977071,  model checking: 0.075173):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) <= True
flip(node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)) <= True
flip(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= True
flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True
flip(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))) <= True
flip(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf)))) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))
flip(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf))
flip(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, node(a, node(a, leaf, leaf), leaf), leaf))) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, node(a, leaf, leaf), leaf), leaf))
flip(node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), node(a, node(a, node(a, leaf, leaf), leaf), leaf)) <= flip(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(s(z)))))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), leaf)), node(a, node(a, leaf, node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(z))
False <= flip(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(z))
False <= numnodes(node(a, leaf, leaf), s(s(z)))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z))))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z)))
numnodes(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(s(z)))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(s(z)))
False <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(z))
numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z))
plus(s(s(z)), s(z), s(s(s(z)))) <= plus(s(s(z)), z, s(s(z)))
False <= plus(s(z), z, s(s(z)))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z))))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_1)
  _r_3(leaf) <= True
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1)
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_0_1) /\ flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1)
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_0_2) /\ flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_1)
  _r_3(leaf) <= True
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1)
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1) /\ _r_2(x_0_2)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1) /\ numnodes(x_0_1, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2) /\ numnodes(x_0_2, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
Yes: {
_hea -> s(s(z))  ;  _iea -> node(_zcvfp_0, node(_pcyfp_0, leaf, node(_vzwfp_0, leaf, leaf)), node(_ppyfp_0, leaf, leaf))  ;  _jea -> s(z)  ;  t -> node(_bdvfp_0, node(_qpyfp_0, leaf, leaf), node(_qcyfp_0, node(_uzwfp_0, leaf, leaf), leaf))
}

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
Yes: {
_rda -> node(_wfvfp_0, node(_ozxfp_0, leaf, leaf), leaf)  ;  _sda -> node(_xfvfp_0, node(_ozxfp_0, leaf, leaf), leaf)  ;  t1 -> node(_yfvfp_0, leaf, node(_nzxfp_0, leaf, leaf))  ;  t2 -> node(_zfvfp_0, leaf, node(_nzxfp_0, leaf, leaf))
}

numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)  :
Yes: {
_bea -> z  ;  _cea -> s(z)  ;  _dea -> s(z)  ;  t1 -> leaf  ;  t2 -> node(_sowfp_0, node(_syxfp_0, leaf, _syxfp_2), node(_tyxfp_0, leaf, _tyxfp_2))
}

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
No: ()


-------------------------------------------
Step 23, which took 12.440460 s (model generation: 12.422116,  model checking: 0.018344):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) <= True
flip(node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)) <= True
flip(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= True
flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True
flip(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))) <= True
flip(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))) <= True
flip(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf)))) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))
flip(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf))
flip(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, node(a, node(a, leaf, leaf), leaf), leaf))) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, node(a, leaf, leaf), leaf), leaf))
flip(node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), node(a, node(a, node(a, leaf, leaf), leaf), leaf)) <= flip(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(s(z)))))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), leaf)), node(a, node(a, leaf, node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(z))
False <= flip(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(z))
False <= numnodes(node(a, leaf, leaf), s(s(z)))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z))))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
numnodes(node(a, leaf, node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z)))
numnodes(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(s(z)))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(s(z)))
False <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(z))
numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z))
plus(s(s(z)), s(z), s(s(s(z)))) <= plus(s(s(z)), z, s(s(z)))
False <= plus(s(z), z, s(s(z)))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z))))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  _r_1(leaf, s(x_1_0)) <= _r_2(x_1_0)
  _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0)
  _r_2(s(x_0_0)) <= _r_3(x_0_0)
  _r_2(z) <= True
  _r_3(s(x_0_0)) <= True
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_1(x_0_2, x_1_0) /\ _r_2(x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ numnodes(x_0_1, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_1_0) /\ numnodes(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_2(s(x_0_0)) <= _r_3(x_0_0)
  _r_2(z) <= True
  _r_3(s(x_0_0)) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  plus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_2(x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_3(x_1_0)
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
Yes: {
n -> s(s(z))
}

eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea)  :
Yes: {
_hea -> s(s(s(s(_fhngp_0))))  ;  _iea -> node(_idjgp_0, leaf, leaf)  ;  _jea -> s(z)  ;  t -> node(_kdjgp_0, leaf, leaf)
}

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
No: ()

numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea)  :
Yes: {
_bea -> z  ;  _cea -> s(s(s(z)))  ;  _dea -> s(s(z))  ;  t1 -> leaf  ;  t2 -> node(_bzkgp_0, node(_aingp_0, node(_qwmgp_0, leaf, leaf), leaf), node(_yhngp_0, _yhngp_1, leaf))
}

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
No: ()


-------------------------------------------
Step 24, which took 17.201260 s (model generation: 17.191756,  model checking: 0.009504):

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) <= True
flip(node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)) <= True
flip(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= True
flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True
flip(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))) <= True
flip(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))) <= True
flip(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf)))) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= True
plus(s(s(z)), s(z), s(s(s(z)))) <= True
plus(s(s(z)), z, s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))
flip(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf))
flip(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, node(a, node(a, leaf, leaf), leaf), leaf))) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, node(a, leaf, leaf), leaf), leaf))
flip(node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), node(a, node(a, node(a, leaf, leaf), leaf), leaf)) <= flip(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(s(z)))))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), leaf)), node(a, node(a, leaf, node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(z))
False <= flip(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(z))
False <= numnodes(node(a, leaf, leaf), s(s(s(s(z)))))
False <= numnodes(node(a, leaf, leaf), s(s(z)))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z))))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
numnodes(node(a, leaf, node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z)))
numnodes(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(s(z)))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(s(z)))
False <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(z))
numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z))
numnodes(node(a, leaf, node(a, node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))), s(s(s(z)))) <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(s(z)))
False <= plus(s(z), z, s(s(z)))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z))))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_2(leaf) <= True
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_1)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_2)
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1) /\ _r_2(x_0_2)
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_1) /\ _r_3(x_0_2)
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_0_1) /\ flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1)
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_0_2) /\ flip(x_0_1, x_1_2)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  _r_2(leaf) <= True
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_1)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_2)
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1) /\ _r_2(x_0_2)
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_1) /\ _r_3(x_0_2)
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1) /\ _r_3(x_0_2)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1) /\ numnodes(x_0_1, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_2) /\ numnodes(x_0_2, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|




Answer of teacher:

flip(leaf, leaf) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

plus(n, z, n) <= True  :
No: ()

flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda)  :
Yes: {
_rda -> node(_sungp_0, _sungp_1, leaf)  ;  _sda -> node(_tungp_0, _tungp_1, leaf)  ;  t1 -> node(_uungp_0, leaf, leaf)  ;  t2 -> node(_vungp_0, leaf, leaf)
}

plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda)  :
No: ()


Total time: 60.235544
Learner time: 58.293871
Teacher time: 0.922486
Reasons for stopping: Maybe:  timeout during learnerLast solver state:

Clauses:
{
flip(leaf, leaf) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_hea, _jea) <= flip(t, _iea) /\ numnodes(_iea, _jea) /\ numnodes(t, _hea) -> 0
flip(node(e, t1, t2), node(e, _rda, _sda)) <= flip(t1, _sda) /\ flip(t2, _rda) -> 0
numnodes(node(e, t1, t2), s(_dea)) <= numnodes(t1, _bea) /\ numnodes(t2, _cea) /\ plus(_bea, _cea, _dea) -> 0
plus(n, s(mm), s(_wda)) <= plus(n, mm, _wda) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) <= True
flip(node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)) <= True
flip(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= True
flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True
flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) <= True
flip(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))) <= True
flip(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))) <= True
flip(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf)))) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True
numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= True
plus(s(s(z)), s(z), s(s(s(z)))) <= True
plus(s(s(z)), z, s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(s(z)), s(s(z))) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))
flip(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf))
flip(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, node(a, node(a, leaf, leaf), leaf), leaf))) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, node(a, leaf, leaf), leaf), leaf))
flip(node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), node(a, node(a, node(a, leaf, leaf), leaf), leaf)) <= flip(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), leaf))
False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, leaf, leaf), node(a, node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), leaf)), node(a, node(a, leaf, node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)), node(a, leaf, leaf))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, node(a, leaf, node(a, leaf, node(a, node(a, leaf, leaf), leaf))), leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), leaf)), node(a, leaf, leaf)), s(s(z)))
False <= flip(node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(z))
False <= numnodes(node(a, leaf, leaf), s(s(s(s(z)))))
False <= numnodes(node(a, leaf, leaf), s(s(z)))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z))))
False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z))))
False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(s(z)))))
False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z)))
numnodes(node(a, leaf, node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z))
False <= numnodes(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z)))
numnodes(node(a, leaf, node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(s(z)))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(s(z)))
False <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(z))
numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z))
numnodes(node(a, leaf, node(a, node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))), s(s(s(z)))) <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(s(z)))
False <= plus(s(z), z, s(s(z)))
numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z))))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_2(leaf) <= True
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_1)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_2)
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1) /\ _r_2(x_0_2)
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_1) /\ _r_3(x_0_2)
  flip(leaf, leaf) <= True
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_0_1) /\ flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1)
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_0_2) /\ flip(x_0_1, x_1_2)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  _r_2(leaf) <= True
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_1)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_2)
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1) /\ _r_2(x_0_2)
  _r_3(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_1) /\ _r_3(x_0_2)
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1) /\ _r_3(x_0_2)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1) /\ numnodes(x_0_1, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_2) /\ numnodes(x_0_2, x_1_0)
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0)
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



--
Equality automata are defined for: {elt, etree, nat}
_|