Solving ../../benchmarks/smtlib/true/tree_flip_preserves_member.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, _aw, _bw)) <= flip(t1, _bw) /\ flip(t2, _aw)
}
eq_etree(_dw, _ew) <= flip(_cw, _dw) /\ flip(_cw, _ew)
)
(memt_elt, P:
{
memt_elt(e2, node(e2, t1, t2)) <= True
eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1)
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2)
False <= memt_elt(e, leaf)
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2))
}
)
}

properties:
{
memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t)
}


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

Clause system for inference is:

{
flip(leaf, leaf) <= True -> 0
memt_elt(e2, node(e2, t1, t2)) <= True -> 0
memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t) -> 0
flip(node(e, t1, t2), node(e, _aw, _bw)) <= flip(t1, _bw) /\ flip(t2, _aw) -> 0
eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2) -> 0
False <= memt_elt(e, leaf) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2)) -> 0
}


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

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


;
memt_elt ->
[
memt_elt : <elt * etree>
{
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_1)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_2)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_4(x_0_0)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_2)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_0)
  _r_3(a) <= True
  _r_4(b) <= True
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_1)
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_2)
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_1)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_2)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_4(x_1_0)
}
]



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

Clauses:
{
flip(leaf, leaf) <= True -> 0
memt_elt(e2, node(e2, t1, t2)) <= True -> 0
memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t) -> 0
flip(node(e, t1, t2), node(e, _aw, _bw)) <= flip(t1, _bw) /\ flip(t2, _aw) -> 0
eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2) -> 0
False <= memt_elt(e, leaf) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2)) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


;
memt_elt ->
[
memt_elt : <elt * etree>
{
  
}
]



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




Answer of teacher:

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

}

memt_elt(e2, node(e2, t1, t2)) <= True  :
Yes: {
e2 -> b
}

memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t)  :
No: ()

flip(node(e, t1, t2), node(e, _aw, _bw)) <= flip(t1, _bw) /\ flip(t2, _aw)  :
No: ()

eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1)  :
No: ()

eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2)  :
No: ()

False <= memt_elt(e, leaf)  :
No: ()

eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2))  :
No: ()


-------------------------------------------
Step 1, which took 0.006561 s (model generation: 0.006472,  model checking: 0.000089):

Clauses:
{
flip(leaf, leaf) <= True -> 0
memt_elt(e2, node(e2, t1, t2)) <= True -> 0
memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t) -> 0
flip(node(e, t1, t2), node(e, _aw, _bw)) <= flip(t1, _bw) /\ flip(t2, _aw) -> 0
eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2) -> 0
False <= memt_elt(e, leaf) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2)) -> 0
}

Accumulated learning constraints:
{
flip(leaf, leaf) <= True
memt_elt(b, node(b, leaf, leaf)) <= True
}

Current best model:
|_
name: None

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


;
memt_elt ->
[
memt_elt : <elt * etree>
{
  memt_elt(b, 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: ()

memt_elt(e2, node(e2, t1, t2)) <= True  :
Yes: {
e2 -> a
}

memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t)  :
No: ()

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

eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1)  :
No: ()

eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2)  :
No: ()

False <= memt_elt(e, leaf)  :
No: ()

eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2))  :
Yes: {
e -> b  ;  e2 -> a  ;  t1 -> leaf  ;  t2 -> leaf
}


-------------------------------------------
Step 2, which took 0.009390 s (model generation: 0.009303,  model checking: 0.000087):

Clauses:
{
flip(leaf, leaf) <= True -> 0
memt_elt(e2, node(e2, t1, t2)) <= True -> 0
memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t) -> 0
flip(node(e, t1, t2), node(e, _aw, _bw)) <= flip(t1, _bw) /\ flip(t2, _aw) -> 0
eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2) -> 0
False <= memt_elt(e, leaf) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2)) -> 0
}

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


;
memt_elt ->
[
memt_elt : <elt * etree>
{
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= True
  memt_elt(b, leaf) <= True
  memt_elt(b, 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: ()

memt_elt(e2, node(e2, t1, t2)) <= True  :
No: ()

memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t)  :
No: ()

flip(node(e, t1, t2), node(e, _aw, _bw)) <= flip(t1, _bw) /\ flip(t2, _aw)  :
No: ()

eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1)  :
No: ()

eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2)  :
No: ()

False <= memt_elt(e, leaf)  :
Yes: {
e -> b
}

eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2))  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> leaf  ;  t2 -> leaf
}


-------------------------------------------
Step 3, which took 0.011950 s (model generation: 0.011775,  model checking: 0.000175):

Clauses:
{
flip(leaf, leaf) <= True -> 0
memt_elt(e2, node(e2, t1, t2)) <= True -> 0
memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t) -> 0
flip(node(e, t1, t2), node(e, _aw, _bw)) <= flip(t1, _bw) /\ flip(t2, _aw) -> 0
eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2) -> 0
False <= memt_elt(e, leaf) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2)) -> 0
}

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


;
memt_elt ->
[
memt_elt : <elt * etree>
{
  _r_1(b) <= True
  memt_elt(a, leaf) <= True
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= True
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_0)
}
]



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




Answer of teacher:

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

memt_elt(e2, node(e2, t1, t2)) <= True  :
No: ()

memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t)  :
Yes: {
_fw -> node(a, _cmzcp_1, _cmzcp_2)  ;  e -> b  ;  t -> node(b, _emzcp_1, _emzcp_2)
}

flip(node(e, t1, t2), node(e, _aw, _bw)) <= flip(t1, _bw) /\ flip(t2, _aw)  :
No: ()

eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1)  :
Yes: {
e -> b  ;  e2 -> a  ;  t1 -> node(b, _hmzcp_1, _hmzcp_2)
}

eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2)  :
Yes: {
e -> b  ;  e2 -> a  ;  t1 -> node(a, _omzcp_1, _omzcp_2)  ;  t2 -> node(b, _pmzcp_1, _pmzcp_2)
}

False <= memt_elt(e, leaf)  :
Yes: {
e -> a
}

eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2))  :
No: ()


-------------------------------------------
Step 4, which took 0.032169 s (model generation: 0.031335,  model checking: 0.000834):

Clauses:
{
flip(leaf, leaf) <= True -> 0
memt_elt(e2, node(e2, t1, t2)) <= True -> 0
memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t) -> 0
flip(node(e, t1, t2), node(e, _aw, _bw)) <= flip(t1, _bw) /\ flip(t2, _aw) -> 0
eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2) -> 0
False <= memt_elt(e, leaf) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2)) -> 0
}

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

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_3(a) <= 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_3(x_0_0)
}
]


;
memt_elt ->
[
memt_elt : <elt * etree>
{
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= True
  _r_2(b) <= True
  _r_3(a) <= True
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_1)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_0)
}
]



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




Answer of teacher:

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

memt_elt(e2, node(e2, t1, t2)) <= True  :
No: ()

memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t)  :
Yes: {
_fw -> node(a, leaf, _onzcp_2)  ;  e -> b  ;  t -> node(a, node(_przcp_0, _przcp_1, _przcp_2), _qnzcp_2)
}

flip(node(e, t1, t2), node(e, _aw, _bw)) <= flip(t1, _bw) /\ flip(t2, _aw)  :
Yes: {
_aw -> node(_ynzcp_0, _ynzcp_1, _ynzcp_2)  ;  _bw -> leaf  ;  e -> b  ;  t1 -> leaf  ;  t2 -> node(a, _bozcp_1, _bozcp_2)
}

eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1)  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> node(a, _mozcp_1, _mozcp_2)
}

eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2)  :
Yes: {
e -> b  ;  e2 -> a  ;  t1 -> leaf  ;  t2 -> node(_epzcp_0, node(_przcp_0, _przcp_1, _przcp_2), _epzcp_2)
}

False <= memt_elt(e, leaf)  :
No: ()

eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2))  :
Yes: {
e -> b  ;  e2 -> a  ;  t1 -> node(a, leaf, _zqzcp_2)  ;  t2 -> leaf
}


-------------------------------------------
Step 5, which took 0.123309 s (model generation: 0.121018,  model checking: 0.002291):

Clauses:
{
flip(leaf, leaf) <= True -> 0
memt_elt(e2, node(e2, t1, t2)) <= True -> 0
memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t) -> 0
flip(node(e, t1, t2), node(e, _aw, _bw)) <= flip(t1, _bw) /\ flip(t2, _aw) -> 0
eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2) -> 0
False <= memt_elt(e, leaf) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2)) -> 0
}

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

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_3(a) <= True
  _r_4(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_3(x_0_0)
  flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_4(x_1_0)
}
]


;
memt_elt ->
[
memt_elt : <elt * etree>
{
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_4(x_0_0)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= True
  _r_3(a) <= True
  _r_4(b) <= True
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_1)
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_1)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_2)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_4(x_1_0)
}
]



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




Answer of teacher:

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

memt_elt(e2, node(e2, t1, t2)) <= True  :
No: ()

memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t)  :
Yes: {
_fw -> node(b, leaf, _yrzcp_2)  ;  e -> a  ;  t -> node(a, node(_xzzcp_0, _xzzcp_1, _xzzcp_2), _aszcp_2)
}

flip(node(e, t1, t2), node(e, _aw, _bw)) <= flip(t1, _bw) /\ flip(t2, _aw)  :
No: ()

eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1)  :
Yes: {
e -> b  ;  e2 -> a  ;  t1 -> node(a, _xuzcp_1, node(_aaadp_0, _aaadp_1, _aaadp_2))  ;  t2 -> leaf
}

eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2)  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> leaf  ;  t2 -> node(_evzcp_0, node(_xzzcp_0, _xzzcp_1, _xzzcp_2), _evzcp_2)
}

False <= memt_elt(e, leaf)  :
No: ()

eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2))  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> node(b, leaf, _pxzcp_2)  ;  t2 -> node(b, leaf, _qxzcp_2)
}


-------------------------------------------
Step 6, which took 0.198105 s (model generation: 0.196332,  model checking: 0.001773):

Clauses:
{
flip(leaf, leaf) <= True -> 0
memt_elt(e2, node(e2, t1, t2)) <= True -> 0
memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t) -> 0
flip(node(e, t1, t2), node(e, _aw, _bw)) <= flip(t1, _bw) /\ flip(t2, _aw) -> 0
eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2) -> 0
False <= memt_elt(e, leaf) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2)) -> 0
}

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

Current best model:
|_
name: None

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


;
memt_elt ->
[
memt_elt : <elt * etree>
{
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_4(x_0_0)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_0)
  _r_3(b) <= True
  _r_4(a) <= True
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_1)
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_2)
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_4(x_1_0)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_1)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_2)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
}
]



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




Answer of teacher:

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

memt_elt(e2, node(e2, t1, t2)) <= True  :
No: ()

memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t)  :
Yes: {
_fw -> node(a, leaf, leaf)  ;  e -> b  ;  t -> node(a, _mbadp_1, node(b, _xkadp_1, _xkadp_2))
}

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

eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1)  :
Yes: {
e -> b  ;  e2 -> a  ;  t1 -> node(a, node(b, _fladp_1, _fladp_2), _veadp_2)  ;  t2 -> leaf
}

eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2)  :
Yes: {
e -> b  ;  e2 -> a  ;  t1 -> leaf  ;  t2 -> node(a, node(b, _fladp_1, _fladp_2), _dgadp_2)
}

False <= memt_elt(e, leaf)  :
No: ()

eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2))  :
No: ()


-------------------------------------------
Step 7, which took 0.237146 s (model generation: 0.234423,  model checking: 0.002723):

Clauses:
{
flip(leaf, leaf) <= True -> 0
memt_elt(e2, node(e2, t1, t2)) <= True -> 0
memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t) -> 0
flip(node(e, t1, t2), node(e, _aw, _bw)) <= flip(t1, _bw) /\ flip(t2, _aw) -> 0
eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2) -> 0
False <= memt_elt(e, leaf) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2)) -> 0
}

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

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_3(a) <= True
  _r_4(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_3(x_0_0) /\ _r_3(x_1_0) /\ 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_4(x_0_0) /\ _r_4(x_1_0)
}
]


;
memt_elt ->
[
memt_elt : <elt * etree>
{
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_1)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_4(x_0_0)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_0)
  _r_3(a) <= True
  _r_4(b) <= True
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_1)
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_2)
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_1)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_2)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_4(x_1_0)
}
]



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




Answer of teacher:

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

memt_elt(e2, node(e2, t1, t2)) <= True  :
No: ()

memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t)  :
Yes: {
_fw -> node(b, leaf, leaf)  ;  e -> a  ;  t -> node(b, _hnadp_1, node(a, _qcbdp_1, _qcbdp_2))
}

flip(node(e, t1, t2), node(e, _aw, _bw)) <= flip(t1, _bw) /\ flip(t2, _aw)  :
No: ()

eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1)  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> node(b, _hwadp_1, node(a, _idbdp_1, _idbdp_2))  ;  t2 -> leaf
}

eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2)  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> leaf  ;  t2 -> node(b, node(a, _hdbdp_1, _hdbdp_2), _xwadp_2)
}

False <= memt_elt(e, leaf)  :
No: ()

eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2))  :
No: ()


-------------------------------------------
Step 8, which took 0.313375 s (model generation: 0.308767,  model checking: 0.004608):

Clauses:
{
flip(leaf, leaf) <= True -> 0
memt_elt(e2, node(e2, t1, t2)) <= True -> 0
memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t) -> 0
flip(node(e, t1, t2), node(e, _aw, _bw)) <= flip(t1, _bw) /\ flip(t2, _aw) -> 0
eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2) -> 0
False <= memt_elt(e, leaf) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2)) -> 0
}

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

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_3(a) <= True
  _r_4(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_3(x_0_0) /\ _r_3(x_1_0) /\ 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_4(x_0_0) /\ _r_4(x_1_0) /\ flip(x_0_2, x_1_1)
}
]


;
memt_elt ->
[
memt_elt : <elt * etree>
{
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_1)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_4(x_0_0)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_2)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_0)
  _r_3(a) <= True
  _r_4(b) <= True
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_1)
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_2)
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_1)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_2)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_4(x_1_0)
}
]



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




Answer of teacher:

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

memt_elt(e2, node(e2, t1, t2)) <= True  :
No: ()

memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t)  :
Yes: {
_fw -> node(a, leaf, leaf)  ;  e -> b  ;  t -> node(a, node(b, _jecdp_1, _jecdp_2), leaf)
}

flip(node(e, t1, t2), node(e, _aw, _bw)) <= flip(t1, _bw) /\ flip(t2, _aw)  :
No: ()

eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1)  :
Yes: {
e -> b  ;  e2 -> a  ;  t1 -> node(a, leaf, node(b, _tecdp_1, _tecdp_2))  ;  t2 -> leaf
}

eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2)  :
Yes: {
e -> b  ;  e2 -> a  ;  t1 -> leaf  ;  t2 -> node(a, leaf, node(b, _tecdp_1, _tecdp_2))
}

False <= memt_elt(e, leaf)  :
No: ()

eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2))  :
No: ()


-------------------------------------------
Step 9, which took 0.358438 s (model generation: 0.353078,  model checking: 0.005360):

Clauses:
{
flip(leaf, leaf) <= True -> 0
memt_elt(e2, node(e2, t1, t2)) <= True -> 0
memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t) -> 0
flip(node(e, t1, t2), node(e, _aw, _bw)) <= flip(t1, _bw) /\ flip(t2, _aw) -> 0
eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2) -> 0
False <= memt_elt(e, leaf) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2)) -> 0
}

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

Current best model:
|_
name: None

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


;
memt_elt ->
[
memt_elt : <elt * etree>
{
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_1)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_2)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_4(x_0_0)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_2)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_0)
  _r_3(a) <= True
  _r_4(b) <= True
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_1)
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_2)
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_1)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_2)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_4(x_1_0)
}
]



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




Answer of teacher:

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

memt_elt(e2, node(e2, t1, t2)) <= True  :
No: ()

memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t)  :
Yes: {
_fw -> node(b, leaf, leaf)  ;  e -> a  ;  t -> node(a, leaf, leaf)
}

flip(node(e, t1, t2), node(e, _aw, _bw)) <= flip(t1, _bw) /\ flip(t2, _aw)  :
Yes: {
_aw -> node(a, _xqddp_1, _xqddp_2)  ;  _bw -> node(b, node(_seedp_0, _seedp_1, _seedp_2), _yqddp_2)  ;  e -> b  ;  t1 -> node(b, leaf, leaf)  ;  t2 -> leaf
}

eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1)  :
No: ()

eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2)  :
No: ()

False <= memt_elt(e, leaf)  :
No: ()

eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2))  :
No: ()


-------------------------------------------
Step 10, which took 0.711336 s (model generation: 0.705237,  model checking: 0.006099):

Clauses:
{
flip(leaf, leaf) <= True -> 0
memt_elt(e2, node(e2, t1, t2)) <= True -> 0
memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t) -> 0
flip(node(e, t1, t2), node(e, _aw, _bw)) <= flip(t1, _bw) /\ flip(t2, _aw) -> 0
eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2) -> 0
False <= memt_elt(e, leaf) -> 0
eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2)) -> 0
}

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

Current best model:
|_
name: None

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


;
memt_elt ->
[
memt_elt : <elt * etree>
{
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_1)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_2)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_0)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_2)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_4(x_0_0)
  _r_3(b) <= True
  _r_4(a) <= True
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_1)
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_2)
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_4(x_1_0)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_1)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_2)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
}
]



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




Answer of teacher:

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

memt_elt(e2, node(e2, t1, t2)) <= True  :
No: ()

memt_elt(e, _fw) <= flip(t, _fw) /\ memt_elt(e, t)  :
Yes: {
_fw -> node(b, leaf, leaf)  ;  e -> a  ;  t -> node(b, node(a, _yagdp_1, _yagdp_2), leaf)
}

flip(node(e, t1, t2), node(e, _aw, _bw)) <= flip(t1, _bw) /\ flip(t2, _aw)  :
Yes: {
_aw -> node(a, _xgfdp_1, _xgfdp_2)  ;  _bw -> node(b, node(_vfgdp_0, _vfgdp_1, _vfgdp_2), _ygfdp_2)  ;  e -> a  ;  t1 -> node(b, _zgfdp_1, leaf)  ;  t2 -> leaf
}

eq_elt(e, e2) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t1)  :
No: ()

eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, node(e2, t1, t2)) <= memt_elt(e, t2)  :
No: ()

False <= memt_elt(e, leaf)  :
No: ()

eq_elt(e, e2) \/ memt_elt(e, t1) \/ memt_elt(e, t2) <= memt_elt(e, node(e2, t1, t2))  :
No: ()


Total time: 2.966887
Learner time: 1.984009
Teacher time: 0.024152
Reasons for stopping: Yes: |_
name: None

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


;
memt_elt ->
[
memt_elt : <elt * etree>
{
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_1)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_2)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_4(x_0_0)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_2)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_0)
  _r_3(a) <= True
  _r_4(b) <= True
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_1)
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_2)
  memt_elt(a, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_1)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_2)
  memt_elt(b, node(x_1_0, x_1_1, x_1_2)) <= _r_4(x_1_0)
}
]



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