Solving ../../benchmarks/smtlib/true/tree_flip_preserves_subtree.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, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa)
}
eq_etree(_qxa, _rxa) <= flip(_pxa, _qxa) /\ flip(_pxa, _rxa)
)
(subtree, P:
{
subtree(leaf, t) <= True
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))
False <= subtree(node(ea, ta1, ta2), leaf)
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))
}
)
}

properties:
{
subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t)
}


over-approximation: {flip}
under-approximation: {}

Clause system for inference is:

{
flip(leaf, leaf) <= True -> 0
subtree(leaf, t) <= True -> 0
subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t) -> 0
flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= subtree(node(ea, ta1, ta2), leaf) -> 0
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}


Solving took 3.428622 seconds.
Yes: |_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_1(a, a) <= True
  _r_1(b, b) <= 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_1(x_0_0, x_1_0) /\ flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1)
}
]


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



--
Equality automata are defined for: {elt, etree, nat}
_|
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.008089 s (model generation: 0.008002,  model checking: 0.000087):

Clauses:
{
flip(leaf, leaf) <= True -> 0
subtree(leaf, t) <= True -> 0
subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t) -> 0
flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= subtree(node(ea, ta1, ta2), leaf) -> 0
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


;
subtree ->
[
subtree : <etree * etree>
{
  
}
]



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




Answer of teacher:

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

}

subtree(leaf, t) <= True  :
Yes: {
t -> node(_jzpgp_0, _jzpgp_1, _jzpgp_2)
}

subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t)  :
No: ()

flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa)  :
No: ()

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
No: ()

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

False <= subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()


-------------------------------------------
Step 1, which took 0.006727 s (model generation: 0.006654,  model checking: 0.000073):

Clauses:
{
flip(leaf, leaf) <= True -> 0
subtree(leaf, t) <= True -> 0
subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t) -> 0
flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= subtree(node(ea, ta1, ta2), leaf) -> 0
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
}

Current best model:
|_
name: None

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


;
subtree ->
[
subtree : <etree * etree>
{
  subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
}
]



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




Answer of teacher:

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

subtree(leaf, t) <= True  :
Yes: {
t -> leaf
}

subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t)  :
No: ()

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

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
Yes: {
ta1 -> leaf  ;  ta2 -> leaf  ;  tb1 -> node(_rzpgp_0, _rzpgp_1, _rzpgp_2)  ;  tb2 -> node(_szpgp_0, _szpgp_1, _szpgp_2)
}

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

False <= subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()


-------------------------------------------
Step 2, which took 0.008676 s (model generation: 0.008574,  model checking: 0.000102):

Clauses:
{
flip(leaf, leaf) <= True -> 0
subtree(leaf, t) <= True -> 0
subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t) -> 0
flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= subtree(node(ea, ta1, ta2), leaf) -> 0
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) <= 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
}
]


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



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




Answer of teacher:

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

subtree(leaf, t) <= True  :
No: ()

subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t)  :
No: ()

flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa)  :
No: ()

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
No: ()

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ta1 -> node(_baqgp_0, _baqgp_1, _baqgp_2)  ;  ta2 -> node(_caqgp_0, _caqgp_1, _caqgp_2)  ;  tb1 -> node(_daqgp_0, _daqgp_1, _daqgp_2)  ;  tb2 -> leaf
}

False <= subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ea -> b  ;  eb -> a
}

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ta1 -> node(_jaqgp_0, _jaqgp_1, _jaqgp_2)  ;  tb1 -> leaf
}


-------------------------------------------
Step 3, which took 0.017554 s (model generation: 0.017259,  model checking: 0.000295):

Clauses:
{
flip(leaf, leaf) <= True -> 0
subtree(leaf, t) <= True -> 0
subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t) -> 0
flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= subtree(node(ea, ta1, ta2), leaf) -> 0
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) <= True
subtree(node(a, leaf, leaf), leaf) <= subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, leaf, leaf), leaf) <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= subtree(node(b, leaf, leaf), node(a, leaf, leaf))
}

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
}
]


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



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




Answer of teacher:

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

subtree(leaf, t) <= True  :
No: ()

subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t)  :
Yes: {
_sxa -> node(b, _laqgp_1, _laqgp_2)  ;  _txa -> node(_maqgp_0, _maqgp_1, _maqgp_2)  ;  s -> node(a, _naqgp_1, _naqgp_2)  ;  t -> node(_oaqgp_0, _oaqgp_1, _oaqgp_2)
}

flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa)  :
No: ()

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
Yes: {
eb -> b  ;  ta1 -> node(_zbqgp_0, _zbqgp_1, _zbqgp_2)  ;  ta2 -> leaf  ;  tb1 -> leaf  ;  tb2 -> node(_ccqgp_0, _ccqgp_1, _ccqgp_2)
}

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
eb -> a  ;  ta1 -> node(_jdqgp_0, _jdqgp_1, _jdqgp_2)  ;  ta2 -> node(b, _kdqgp_1, _kdqgp_2)  ;  tb1 -> leaf  ;  tb2 -> node(_mdqgp_0, _mdqgp_1, _mdqgp_2)
}

False <= subtree(node(ea, ta1, ta2), leaf)  :
Yes: {

}

eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ea -> a  ;  eb -> b
}

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
eb -> a  ;  ta1 -> node(b, _vdqgp_1, _vdqgp_2)  ;  tb1 -> node(_wdqgp_0, _wdqgp_1, _wdqgp_2)
}


-------------------------------------------
Step 4, which took 0.017522 s (model generation: 0.017191,  model checking: 0.000331):

Clauses:
{
flip(leaf, leaf) <= True -> 0
subtree(leaf, t) <= True -> 0
subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t) -> 0
flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= subtree(node(ea, ta1, ta2), leaf) -> 0
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) <= True
False <= flip(node(a, leaf, leaf), node(b, leaf, leaf)) /\ subtree(node(a, leaf, leaf), node(a, leaf, leaf))
False <= subtree(node(a, leaf, leaf), leaf)
False <= subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(a, leaf, leaf), node(b, leaf, leaf))
False <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
False <= subtree(node(a, node(b, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(b, leaf, leaf), node(a, leaf, leaf))
}

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
}
]


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



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




Answer of teacher:

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

subtree(leaf, t) <= True  :
No: ()

subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t)  :
Yes: {
_sxa -> node(_zdqgp_0, _zdqgp_1, _zdqgp_2)  ;  _txa -> node(_aeqgp_0, _aeqgp_1, leaf)  ;  s -> node(_beqgp_0, _beqgp_1, _beqgp_2)  ;  t -> node(_ceqgp_0, _ceqgp_1, node(_ugqgp_0, _ugqgp_1, _ugqgp_2))
}

flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa)  :
No: ()

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
Yes: {
ta1 -> node(_bfqgp_0, _bfqgp_1, _bfqgp_2)  ;  ta2 -> leaf  ;  tb1 -> node(_dfqgp_0, _dfqgp_1, node(_ugqgp_0, _ugqgp_1, _ugqgp_2))  ;  tb2 -> leaf
}

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ta1 -> node(_hgqgp_0, _hgqgp_1, _hgqgp_2)  ;  ta2 -> node(_igqgp_0, _igqgp_1, _igqgp_2)  ;  tb1 -> node(_jgqgp_0, _jgqgp_1, node(_ugqgp_0, _ugqgp_1, _ugqgp_2))  ;  tb2 -> node(_kgqgp_0, _kgqgp_1, leaf)
}

False <= subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ea -> b  ;  eb -> a  ;  tb2 -> node(_ugqgp_0, _ugqgp_1, _ugqgp_2)
}

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ta1 -> node(_rgqgp_0, _rgqgp_1, _rgqgp_2)  ;  tb1 -> node(_sgqgp_0, _sgqgp_1, leaf)  ;  tb2 -> node(_ugqgp_0, _ugqgp_1, _ugqgp_2)
}


-------------------------------------------
Step 5, which took 0.038022 s (model generation: 0.037690,  model checking: 0.000332):

Clauses:
{
flip(leaf, leaf) <= True -> 0
subtree(leaf, t) <= True -> 0
subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t) -> 0
flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= subtree(node(ea, ta1, ta2), leaf) -> 0
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) <= True
False <= flip(node(a, leaf, leaf), node(b, leaf, leaf)) /\ subtree(node(a, leaf, leaf), node(a, leaf, leaf))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) /\ subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= subtree(node(a, leaf, leaf), leaf)
False <= subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)))
False <= subtree(node(a, leaf, leaf), node(b, leaf, leaf))
False <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= subtree(node(a, node(b, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(b, leaf, leaf), node(a, leaf, leaf))
False <= subtree(node(b, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
}

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
}
]


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



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




Answer of teacher:

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

subtree(leaf, t) <= True  :
No: ()

subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t)  :
Yes: {
_sxa -> node(_wgqgp_0, node(_ujqgp_0, _ujqgp_1, _ujqgp_2), _wgqgp_2)  ;  _txa -> node(_xgqgp_0, node(_vjqgp_0, _vjqgp_1, _vjqgp_2), _xgqgp_2)  ;  s -> node(_ygqgp_0, leaf, _ygqgp_2)  ;  t -> node(_zgqgp_0, node(_xjqgp_0, _xjqgp_1, _xjqgp_2), _zgqgp_2)
}

flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa)  :
No: ()

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
Yes: {
ta1 -> leaf  ;  ta2 -> node(_jhqgp_0, leaf, _jhqgp_2)  ;  tb1 -> leaf  ;  tb2 -> node(_lhqgp_0, node(_xjqgp_0, _xjqgp_1, _xjqgp_2), _lhqgp_2)
}

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ta1 -> leaf  ;  ta2 -> node(_piqgp_0, _piqgp_1, _piqgp_2)  ;  tb1 -> node(_qiqgp_0, _qiqgp_1, _qiqgp_2)  ;  tb2 -> leaf
}

False <= subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ea -> b  ;  eb -> a  ;  ta1 -> leaf  ;  tb1 -> node(_xjqgp_0, _xjqgp_1, _xjqgp_2)
}

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()


-------------------------------------------
Step 6, which took 0.081458 s (model generation: 0.080763,  model checking: 0.000695):

Clauses:
{
flip(leaf, leaf) <= True -> 0
subtree(leaf, t) <= True -> 0
subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t) -> 0
flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= subtree(node(ea, ta1, ta2), leaf) -> 0
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) <= True
subtree(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)) <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) /\ flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)) /\ subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))
False <= flip(node(a, leaf, leaf), node(b, leaf, leaf)) /\ subtree(node(a, leaf, leaf), node(a, leaf, leaf))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) /\ subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= subtree(node(a, leaf, leaf), leaf)
False <= subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)))
subtree(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) <= subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(a, leaf, leaf), node(b, leaf, leaf))
False <= subtree(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= subtree(node(a, node(b, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(b, leaf, leaf), node(a, leaf, leaf))
False <= subtree(node(b, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= subtree(node(b, leaf, leaf), node(a, node(a, leaf, leaf), leaf))
}

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
}
]


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



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




Answer of teacher:

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

subtree(leaf, t) <= True  :
No: ()

subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t)  :
Yes: {
_sxa -> node(_ckqgp_0, _ckqgp_1, node(_yoqgp_0, _yoqgp_1, _yoqgp_2))  ;  _txa -> node(_dkqgp_0, node(_zoqgp_0, _zoqgp_1, _zoqgp_2), _dkqgp_2)  ;  s -> node(_ekqgp_0, leaf, leaf)  ;  t -> node(_fkqgp_0, node(_bpqgp_0, _bpqgp_1, _bpqgp_2), node(_bpqgp_0, _bpqgp_1, _bpqgp_2))
}

flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa)  :
No: ()

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
Yes: {
ta1 -> leaf  ;  ta2 -> leaf  ;  tb1 -> node(_ukqgp_0, _ukqgp_1, _ukqgp_2)  ;  tb2 -> leaf
}

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

False <= subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ea -> b  ;  eb -> a  ;  ta1 -> leaf  ;  ta2 -> leaf  ;  tb1 -> node(_bpqgp_0, _bpqgp_1, _bpqgp_2)  ;  tb2 -> node(_bpqgp_0, _bpqgp_1, _bpqgp_2)
}

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()


-------------------------------------------
Step 7, which took 0.682441 s (model generation: 0.085010,  model checking: 0.597431):

Clauses:
{
flip(leaf, leaf) <= True -> 0
subtree(leaf, t) <= True -> 0
subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t) -> 0
flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= subtree(node(ea, ta1, ta2), leaf) -> 0
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) <= True
subtree(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) <= True
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))) /\ flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)) <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) /\ flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))
False <= flip(node(a, leaf, leaf), node(b, leaf, leaf)) /\ subtree(node(a, leaf, leaf), node(a, leaf, leaf))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) /\ subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= subtree(node(a, leaf, leaf), leaf)
False <= subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)))
False <= subtree(node(a, leaf, leaf), node(b, leaf, leaf))
False <= subtree(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= subtree(node(a, node(b, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(b, leaf, leaf), node(a, leaf, leaf))
False <= subtree(node(b, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= subtree(node(b, leaf, leaf), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(b, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_1(a, node(x_1_0, x_1_1, x_1_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)) <= subtree(x_0_1, x_1_1) /\ subtree(x_0_2, x_1_2)
  subtree(leaf, leaf) <= True
  subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
  subtree(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_0_0, x_1_1) /\ subtree(x_0_1, x_1_1) /\ subtree(x_0_2, x_1_2)
  subtree(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_0_0, x_1_2) /\ subtree(x_0_1, x_1_1) /\ subtree(x_0_2, x_1_2)
}
]


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



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




Answer of teacher:

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

subtree(leaf, t) <= True  :
No: ()

subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t)  :
Yes: {
_sxa -> node(_uqqgp_0, node(_josgp_0, _josgp_1, _josgp_2), node(_bksgp_0, _bksgp_1, _bksgp_2))  ;  _txa -> node(_vqqgp_0, leaf, node(_zjsgp_0, node(_fcsgp_0, _fcsgp_1, _fcsgp_2), node(_gfsgp_0, _gfsgp_1, _gfsgp_2)))  ;  s -> node(a, leaf, leaf)  ;  t -> node(_xqqgp_0, leaf, node(a, leaf, leaf))
}

flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa)  :
Yes: {
_nxa -> node(_isqgp_0, leaf, node(_qcsgp_0, _qcsgp_1, _qcsgp_2))  ;  _oxa -> leaf  ;  t1 -> leaf  ;  t2 -> node(_lsqgp_0, leaf, leaf)
}

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
Yes: {
eb -> b  ;  ta1 -> leaf  ;  ta2 -> leaf  ;  tb1 -> leaf  ;  tb2 -> leaf
}

False <= subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ea -> a  ;  eb -> b  ;  ta1 -> leaf  ;  ta2 -> node(a, leaf, leaf)  ;  tb1 -> node(_xbsgp_0, _xbsgp_1, _xbsgp_2)  ;  tb2 -> node(_sfsgp_0, node(_xbsgp_0, _xbsgp_1, _xbsgp_2), node(_xesgp_0, _xesgp_1, _xesgp_2))
}


-------------------------------------------
Step 8, which took 0.121099 s (model generation: 0.118265,  model checking: 0.002834):

Clauses:
{
flip(leaf, leaf) <= True -> 0
subtree(leaf, t) <= True -> 0
subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t) -> 0
flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= subtree(node(ea, ta1, ta2), leaf) -> 0
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) <= True
subtree(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) <= True
subtree(node(b, leaf, leaf), node(b, leaf, leaf)) <= True
flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))) /\ flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)) <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) /\ flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, leaf, node(a, node(a, leaf, leaf), node(a, leaf, leaf)))) <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, node(a, leaf, leaf), node(a, leaf, leaf)))) /\ subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, leaf), node(b, leaf, leaf)) /\ subtree(node(a, leaf, leaf), node(a, leaf, leaf))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) /\ subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= subtree(node(a, leaf, leaf), leaf)
False <= subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)))
False <= subtree(node(a, leaf, leaf), node(b, leaf, leaf))
False <= subtree(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(a, leaf, node(a, leaf, leaf)), node(b, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))))
False <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= subtree(node(a, node(b, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(b, leaf, leaf), node(a, leaf, leaf))
False <= subtree(node(b, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= subtree(node(b, leaf, leaf), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(b, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))
}

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

subtree(leaf, t) <= True  :
No: ()

subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t)  :
Yes: {
_sxa -> node(b, _xkahp_1, leaf)  ;  _txa -> leaf  ;  s -> node(b, leaf, leaf)  ;  t -> node(b, node(_wuahp_0, _wuahp_1, _wuahp_2), node(_cwahp_0, _cwahp_1, _cwahp_2))
}

flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa)  :
Yes: {
_nxa -> leaf  ;  _oxa -> node(a, _wnahp_1, node(b, _okbhp_1, leaf))  ;  t1 -> node(a, _xnahp_1, node(b, _nkbhp_1, node(_tvahp_0, _tvahp_1, _tvahp_2)))  ;  t2 -> node(b, _ynahp_1, _ynahp_2)
}

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
No: ()

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

False <= subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()


-------------------------------------------
Step 9, which took 0.247238 s (model generation: 0.244548,  model checking: 0.002690):

Clauses:
{
flip(leaf, leaf) <= True -> 0
subtree(leaf, t) <= True -> 0
subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t) -> 0
flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= subtree(node(ea, ta1, ta2), leaf) -> 0
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) <= True
subtree(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) <= True
subtree(node(b, leaf, leaf), node(b, leaf, leaf)) <= True
flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))) /\ flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)) <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) /\ flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, leaf, node(a, node(a, leaf, leaf), node(a, leaf, leaf)))) <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, node(a, leaf, leaf), node(a, leaf, leaf)))) /\ subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, leaf), node(b, leaf, leaf)) /\ subtree(node(a, leaf, leaf), node(a, leaf, leaf))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) /\ subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
flip(node(a, node(a, leaf, node(b, leaf, node(a, leaf, leaf))), node(b, leaf, leaf)), node(a, leaf, node(a, leaf, node(b, leaf, leaf)))) <= flip(node(a, leaf, node(b, leaf, node(a, leaf, leaf))), node(a, leaf, node(b, leaf, leaf))) /\ flip(node(b, leaf, leaf), leaf)
subtree(node(b, leaf, leaf), leaf) <= flip(node(b, leaf, leaf), node(b, leaf, leaf)) /\ flip(node(b, node(a, leaf, leaf), node(a, leaf, leaf)), leaf) /\ subtree(node(b, leaf, leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= subtree(node(a, leaf, leaf), leaf)
False <= subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)))
False <= subtree(node(a, leaf, leaf), node(b, leaf, leaf))
False <= subtree(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(a, leaf, node(a, leaf, leaf)), node(b, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))))
False <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= subtree(node(a, node(b, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(b, leaf, leaf), node(a, leaf, leaf))
False <= subtree(node(b, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= subtree(node(b, leaf, leaf), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(b, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_1(a, a) <= True
  _r_1(b, b) <= 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_1(x_0_0, x_1_0) /\ flip(x_0_2, x_1_2)
}
]


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



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




Answer of teacher:

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

subtree(leaf, t) <= True  :
No: ()

subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t)  :
Yes: {
_sxa -> node(b, node(_qybhp_0, _qybhp_1, _qybhp_2), leaf)  ;  _txa -> node(b, leaf, node(b, _pnchp_1, leaf))  ;  s -> node(b, leaf, leaf)  ;  t -> node(b, node(_dybhp_0, _dybhp_1, _dybhp_2), node(b, _onchp_1, leaf))
}

flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa)  :
Yes: {
_nxa -> node(b, _uqbhp_1, node(b, _bnchp_1, leaf))  ;  _oxa -> leaf  ;  t1 -> leaf  ;  t2 -> node(b, _xqbhp_1, node(b, _anchp_1, leaf))
}

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
No: ()

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

False <= subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()


-------------------------------------------
Step 10, which took 0.500635 s (model generation: 0.497322,  model checking: 0.003313):

Clauses:
{
flip(leaf, leaf) <= True -> 0
subtree(leaf, t) <= True -> 0
subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t) -> 0
flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= subtree(node(ea, ta1, ta2), leaf) -> 0
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) <= True
subtree(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) <= True
subtree(node(b, leaf, leaf), node(b, leaf, leaf)) <= True
flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))) /\ flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)) <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) /\ flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, leaf, node(a, node(a, leaf, leaf), node(a, leaf, leaf)))) <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, node(a, leaf, leaf), node(a, leaf, leaf)))) /\ subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, leaf), node(b, leaf, leaf)) /\ subtree(node(a, leaf, leaf), node(a, leaf, leaf))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) /\ subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
flip(node(a, node(a, leaf, node(b, leaf, node(a, leaf, leaf))), node(b, leaf, leaf)), node(a, leaf, node(a, leaf, node(b, leaf, leaf)))) <= flip(node(a, leaf, node(b, leaf, node(a, leaf, leaf))), node(a, leaf, node(b, leaf, leaf))) /\ flip(node(b, leaf, leaf), leaf)
subtree(node(b, leaf, leaf), leaf) <= flip(node(b, leaf, leaf), node(b, leaf, leaf)) /\ flip(node(b, node(a, leaf, leaf), node(a, leaf, leaf)), leaf) /\ subtree(node(b, leaf, leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
subtree(node(b, node(a, leaf, leaf), leaf), node(b, leaf, node(b, leaf, leaf))) <= flip(node(b, leaf, leaf), node(b, node(a, leaf, leaf), leaf)) /\ flip(node(b, node(a, leaf, leaf), node(b, leaf, leaf)), node(b, leaf, node(b, leaf, leaf))) /\ subtree(node(b, leaf, leaf), node(b, node(a, leaf, leaf), node(b, leaf, leaf)))
flip(node(a, leaf, node(b, leaf, node(b, leaf, leaf))), node(a, node(b, leaf, node(b, leaf, leaf)), leaf)) <= flip(node(b, leaf, node(b, leaf, leaf)), node(b, leaf, node(b, leaf, leaf)))
False <= subtree(node(a, leaf, leaf), leaf)
False <= subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)))
False <= subtree(node(a, leaf, leaf), node(b, leaf, leaf))
False <= subtree(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(a, leaf, node(a, leaf, leaf)), node(b, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))))
False <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= subtree(node(a, node(b, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(b, leaf, leaf), node(a, leaf, leaf))
False <= subtree(node(b, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= subtree(node(b, leaf, leaf), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(b, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_1(a, a) <= True
  _r_1(b, b) <= 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_1(x_0_0, x_1_0) /\ flip(x_0_1, x_1_2)
}
]


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



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




Answer of teacher:

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

subtree(leaf, t) <= True  :
No: ()

subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t)  :
Yes: {
_sxa -> node(b, node(_uadhp_0, _uadhp_1, _uadhp_2), leaf)  ;  _txa -> node(b, leaf, node(b, _jqdhp_1, leaf))  ;  s -> node(b, leaf, leaf)  ;  t -> node(b, node(b, leaf, _iqdhp_2), node(_hadhp_0, _hadhp_1, _hadhp_2))
}

flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa)  :
No: ()

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
No: ()

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

False <= subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()


-------------------------------------------
Step 11, which took 0.485555 s (model generation: 0.482644,  model checking: 0.002911):

Clauses:
{
flip(leaf, leaf) <= True -> 0
subtree(leaf, t) <= True -> 0
subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t) -> 0
flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= subtree(node(ea, ta1, ta2), leaf) -> 0
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) <= True
subtree(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) <= True
subtree(node(b, leaf, leaf), node(b, leaf, leaf)) <= True
flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))) /\ flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)) <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) /\ flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, leaf, node(a, node(a, leaf, leaf), node(a, leaf, leaf)))) <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, node(a, leaf, leaf), node(a, leaf, leaf)))) /\ subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, leaf), node(b, leaf, leaf)) /\ subtree(node(a, leaf, leaf), node(a, leaf, leaf))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) /\ subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
flip(node(a, node(a, leaf, node(b, leaf, node(a, leaf, leaf))), node(b, leaf, leaf)), node(a, leaf, node(a, leaf, node(b, leaf, leaf)))) <= flip(node(a, leaf, node(b, leaf, node(a, leaf, leaf))), node(a, leaf, node(b, leaf, leaf))) /\ flip(node(b, leaf, leaf), leaf)
subtree(node(b, leaf, leaf), leaf) <= flip(node(b, leaf, leaf), node(b, leaf, leaf)) /\ flip(node(b, node(a, leaf, leaf), node(a, leaf, leaf)), leaf) /\ subtree(node(b, leaf, leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
subtree(node(b, node(a, leaf, leaf), leaf), node(b, leaf, node(b, leaf, leaf))) <= flip(node(b, leaf, leaf), node(b, node(a, leaf, leaf), leaf)) /\ flip(node(b, node(a, leaf, leaf), node(b, leaf, leaf)), node(b, leaf, node(b, leaf, leaf))) /\ subtree(node(b, leaf, leaf), node(b, node(a, leaf, leaf), node(b, leaf, leaf)))
subtree(node(b, node(a, leaf, leaf), leaf), node(b, leaf, node(b, leaf, leaf))) <= flip(node(b, leaf, leaf), node(b, node(a, leaf, leaf), leaf)) /\ flip(node(b, node(b, leaf, leaf), node(a, leaf, leaf)), node(b, leaf, node(b, leaf, leaf))) /\ subtree(node(b, leaf, leaf), node(b, node(b, leaf, leaf), node(a, leaf, leaf)))
flip(node(a, leaf, node(b, leaf, node(b, leaf, leaf))), node(a, node(b, leaf, node(b, leaf, leaf)), leaf)) <= flip(node(b, leaf, node(b, leaf, leaf)), node(b, leaf, node(b, leaf, leaf)))
False <= subtree(node(a, leaf, leaf), leaf)
False <= subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)))
False <= subtree(node(a, leaf, leaf), node(b, leaf, leaf))
False <= subtree(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(a, leaf, node(a, leaf, leaf)), node(b, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))))
False <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= subtree(node(a, node(b, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(b, leaf, leaf), node(a, leaf, leaf))
False <= subtree(node(b, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= subtree(node(b, leaf, leaf), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(b, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_1(a, a) <= True
  _r_1(b, b) <= 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_1(x_0_0, x_1_0) /\ flip(x_0_2, x_1_1) /\ flip(x_0_2, x_1_2)
}
]


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



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




Answer of teacher:

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

subtree(leaf, t) <= True  :
No: ()

subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t)  :
No: ()

flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa)  :
Yes: {
_nxa -> node(b, leaf, leaf)  ;  _oxa -> leaf  ;  t1 -> leaf  ;  t2 -> node(b, _dwdhp_1, leaf)
}

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
No: ()

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

False <= subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()


-------------------------------------------
Step 12, which took 0.503743 s (model generation: 0.499137,  model checking: 0.004606):

Clauses:
{
flip(leaf, leaf) <= True -> 0
subtree(leaf, t) <= True -> 0
subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t) -> 0
flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa) -> 0
subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2) -> 0
subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= subtree(node(ea, ta1, ta2), leaf) -> 0
eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True
subtree(leaf, leaf) <= True
subtree(leaf, node(a, leaf, leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) <= True
subtree(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) <= True
subtree(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, node(a, leaf, leaf), leaf))) <= True
subtree(node(b, leaf, leaf), node(b, leaf, leaf)) <= True
flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))) /\ flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)) <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) /\ flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, leaf, node(a, node(a, leaf, leaf), node(a, leaf, leaf)))) <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, node(a, leaf, leaf), node(a, leaf, leaf)))) /\ subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, leaf), node(b, leaf, leaf)) /\ subtree(node(a, leaf, leaf), node(a, leaf, leaf))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) /\ subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
flip(node(a, node(a, leaf, node(b, leaf, node(a, leaf, leaf))), node(b, leaf, leaf)), node(a, leaf, node(a, leaf, node(b, leaf, leaf)))) <= flip(node(a, leaf, node(b, leaf, node(a, leaf, leaf))), node(a, leaf, node(b, leaf, leaf))) /\ flip(node(b, leaf, leaf), leaf)
flip(node(a, leaf, node(b, leaf, leaf)), node(a, node(b, leaf, leaf), leaf)) <= flip(node(b, leaf, leaf), node(b, leaf, leaf))
subtree(node(b, leaf, leaf), leaf) <= flip(node(b, leaf, leaf), node(b, leaf, leaf)) /\ flip(node(b, node(a, leaf, leaf), node(a, leaf, leaf)), leaf) /\ subtree(node(b, leaf, leaf), node(b, node(a, leaf, leaf), node(a, leaf, leaf)))
subtree(node(b, node(a, leaf, leaf), leaf), node(b, leaf, node(b, leaf, leaf))) <= flip(node(b, leaf, leaf), node(b, node(a, leaf, leaf), leaf)) /\ flip(node(b, node(a, leaf, leaf), node(b, leaf, leaf)), node(b, leaf, node(b, leaf, leaf))) /\ subtree(node(b, leaf, leaf), node(b, node(a, leaf, leaf), node(b, leaf, leaf)))
subtree(node(b, node(a, leaf, leaf), leaf), node(b, leaf, node(b, leaf, leaf))) <= flip(node(b, leaf, leaf), node(b, node(a, leaf, leaf), leaf)) /\ flip(node(b, node(b, leaf, leaf), node(a, leaf, leaf)), node(b, leaf, node(b, leaf, leaf))) /\ subtree(node(b, leaf, leaf), node(b, node(b, leaf, leaf), node(a, leaf, leaf)))
flip(node(a, leaf, node(b, leaf, node(b, leaf, leaf))), node(a, node(b, leaf, node(b, leaf, leaf)), leaf)) <= flip(node(b, leaf, node(b, leaf, leaf)), node(b, leaf, node(b, leaf, leaf)))
False <= subtree(node(a, leaf, leaf), leaf)
False <= subtree(node(a, leaf, leaf), node(a, leaf, leaf)) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
subtree(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) <= subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= subtree(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))) /\ subtree(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)))
False <= subtree(node(a, leaf, leaf), node(b, leaf, leaf))
False <= subtree(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(a, leaf, node(a, leaf, leaf)), node(b, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))))
False <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))
subtree(node(a, leaf, leaf), node(a, leaf, leaf)) <= subtree(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))
False <= subtree(node(a, node(b, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(b, leaf, leaf), node(a, leaf, leaf))
False <= subtree(node(b, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= subtree(node(b, leaf, leaf), node(a, node(a, leaf, leaf), leaf))
False <= subtree(node(b, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))
}

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_1(a, a) <= True
  _r_1(b, b) <= 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_1(x_0_0, x_1_0) /\ subtree(x_0_1, x_1_2) /\ subtree(x_0_2, x_1_1)
  subtree(leaf, leaf) <= True
  subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
  subtree(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_0_0, x_1_0) /\ subtree(x_0_1, x_1_1) /\ subtree(x_0_2, x_1_2)
}
]


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



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




Answer of teacher:

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

subtree(leaf, t) <= True  :
No: ()

subtree(_sxa, _txa) <= flip(s, _sxa) /\ flip(t, _txa) /\ subtree(s, t)  :
Yes: {
_sxa -> node(b, node(_lhfhp_0, _lhfhp_1, _lhfhp_2), node(_vifhp_0, _vifhp_1, _vifhp_2))  ;  _txa -> node(b, node(_jhfhp_0, _jhfhp_1, _jhfhp_2), leaf)  ;  s -> node(b, leaf, leaf)  ;  t -> node(b, leaf, leaf)
}

flip(node(e, t1, t2), node(e, _nxa, _oxa)) <= flip(t1, _oxa) /\ flip(t2, _nxa)  :
Yes: {
_nxa -> node(b, node(a, leaf, node(_vlghp_0, _vlghp_1, _vlghp_2)), node(b, _xighp_1, _xighp_2))  ;  _oxa -> leaf  ;  t1 -> leaf  ;  t2 -> node(b, leaf, node(a, leaf, leaf))
}

subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= subtree(ta1, tb1) /\ subtree(ta2, tb2)  :
No: ()

subtree(ta2, tb2) <= subtree(ta1, tb1) /\ subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

False <= subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_elt(ea, eb) <= subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

subtree(ta1, tb1) <= subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()


Total time: 3.428622
Learner time: 2.103059
Teacher time: 0.615700
Reasons for stopping: Yes: |_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_1(a, a) <= True
  _r_1(b, b) <= 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_1(x_0_0, x_1_0) /\ flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1)
}
]


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



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