Solving ../../benchmarks/smtlib/true/tree_flip_twice.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, _pb, _qb)) <= flip(t1, _qb) /\ flip(t2, _pb)
}
eq_etree(_sb, _tb) <= flip(_rb, _sb) /\ flip(_rb, _tb)
)
}

properties:
{
eq_etree(_vb, t) <= flip(_ub, _vb) /\ flip(t, _ub)
}


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

Clause system for inference is:

{
flip(leaf, leaf) <= True -> 0
eq_etree(_vb, t) <= flip(_ub, _vb) /\ flip(t, _ub) -> 0
flip(node(e, t1, t2), node(e, _pb, _qb)) <= flip(t1, _qb) /\ flip(t2, _pb) -> 0
}


Solving took 0.236281 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)
}
]



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

Clauses:
{
flip(leaf, leaf) <= True -> 0
eq_etree(_vb, t) <= flip(_ub, _vb) /\ flip(t, _ub) -> 0
flip(node(e, t1, t2), node(e, _pb, _qb)) <= flip(t1, _qb) /\ flip(t2, _pb) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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



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




Answer of teacher:

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

}

eq_etree(_vb, t) <= flip(_ub, _vb) /\ flip(t, _ub)  :
No: ()

flip(node(e, t1, t2), node(e, _pb, _qb)) <= flip(t1, _qb) /\ flip(t2, _pb)  :
No: ()


-------------------------------------------
Step 1, which took 0.006532 s (model generation: 0.006484,  model checking: 0.000048):

Clauses:
{
flip(leaf, leaf) <= True -> 0
eq_etree(_vb, t) <= flip(_ub, _vb) /\ flip(t, _ub) -> 0
flip(node(e, t1, t2), node(e, _pb, _qb)) <= flip(t1, _qb) /\ flip(t2, _pb) -> 0
}

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

Current best model:
|_
name: None

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



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




Answer of teacher:

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

eq_etree(_vb, t) <= flip(_ub, _vb) /\ flip(t, _ub)  :
No: ()

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


-------------------------------------------
Step 2, which took 0.009928 s (model generation: 0.009854,  model checking: 0.000074):

Clauses:
{
flip(leaf, leaf) <= True -> 0
eq_etree(_vb, t) <= flip(_ub, _vb) /\ flip(t, _ub) -> 0
flip(node(e, t1, t2), node(e, _pb, _qb)) <= flip(t1, _qb) /\ flip(t2, _pb) -> 0
}

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



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




Answer of teacher:

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

eq_etree(_vb, t) <= flip(_ub, _vb) /\ flip(t, _ub)  :
Yes: {
_ub -> node(_zhihp_0, _zhihp_1, _zhihp_2)  ;  _vb -> node(b, _aiihp_1, _aiihp_2)  ;  t -> node(a, _biihp_1, _biihp_2)
}

flip(node(e, t1, t2), node(e, _pb, _qb)) <= flip(t1, _qb) /\ flip(t2, _pb)  :
No: ()


-------------------------------------------
Step 3, which took 0.013455 s (model generation: 0.013311,  model checking: 0.000144):

Clauses:
{
flip(leaf, leaf) <= True -> 0
eq_etree(_vb, t) <= flip(_ub, _vb) /\ flip(t, _ub) -> 0
flip(node(e, t1, t2), node(e, _pb, _qb)) <= flip(t1, _qb) /\ flip(t2, _pb) -> 0
}

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

Current best model:
|_
name: None

flip ->
[
flip : <etree * etree>
{
  _r_1(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_0)
}
]



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




Answer of teacher:

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

eq_etree(_vb, t) <= flip(_ub, _vb) /\ flip(t, _ub)  :
Yes: {
_ub -> node(a, _siihp_1, _siihp_2)  ;  _vb -> node(a, _tiihp_1, node(_ojihp_0, _ojihp_1, _ojihp_2))  ;  t -> node(_uiihp_0, _uiihp_1, leaf)
}

flip(node(e, t1, t2), node(e, _pb, _qb)) <= flip(t1, _qb) /\ flip(t2, _pb)  :
Yes: {
_pb -> node(a, _ziihp_1, _ziihp_2)  ;  _qb -> leaf  ;  e -> b  ;  t1 -> leaf  ;  t2 -> node(_cjihp_0, _cjihp_1, _cjihp_2)
}


-------------------------------------------
Step 4, which took 0.017557 s (model generation: 0.016803,  model checking: 0.000754):

Clauses:
{
flip(leaf, leaf) <= True -> 0
eq_etree(_vb, t) <= flip(_ub, _vb) /\ flip(t, _ub) -> 0
flip(node(e, t1, t2), node(e, _pb, _qb)) <= flip(t1, _qb) /\ flip(t2, _pb) -> 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
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, leaf), node(b, 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)
}
]



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




Answer of teacher:

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

eq_etree(_vb, t) <= flip(_ub, _vb) /\ flip(t, _ub)  :
Yes: {
_ub -> leaf  ;  _vb -> leaf  ;  t -> node(_zjihp_0, _zjihp_1, _zjihp_2)
}

flip(node(e, t1, t2), node(e, _pb, _qb)) <= flip(t1, _qb) /\ flip(t2, _pb)  :
Yes: {
_pb -> leaf  ;  _qb -> node(a, _vmihp_1, node(b, _joihp_1, leaf))  ;  t1 -> node(a, _wmihp_1, node(b, _ioihp_1, node(_mnihp_0, _mnihp_1, _mnihp_2)))  ;  t2 -> node(b, _xmihp_1, _xmihp_2)
}


-------------------------------------------
Step 5, which took 0.044565 s (model generation: 0.044139,  model checking: 0.000426):

Clauses:
{
flip(leaf, leaf) <= True -> 0
eq_etree(_vb, t) <= flip(_ub, _vb) /\ flip(t, _ub) -> 0
flip(node(e, t1, t2), node(e, _pb, _qb)) <= flip(t1, _qb) /\ flip(t2, _pb) -> 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
False <= flip(node(a, leaf, leaf), leaf)
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, leaf), node(b, 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)
}

Current best model:
|_
name: None

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



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




Answer of teacher:

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

eq_etree(_vb, t) <= flip(_ub, _vb) /\ flip(t, _ub)  :
Yes: {
_ub -> node(b, leaf, node(b, _orihp_1, leaf))  ;  _vb -> node(b, _upihp_1, leaf)  ;  t -> node(_vpihp_0, node(_qrihp_0, leaf, node(_erihp_0, _erihp_1, _erihp_2)), node(_vrihp_0, _vrihp_1, _vrihp_2))
}

flip(node(e, t1, t2), node(e, _pb, _qb)) <= flip(t1, _qb) /\ flip(t2, _pb)  :
Yes: {
_pb -> leaf  ;  _qb -> node(b, _nqihp_1, leaf)  ;  e -> b  ;  t1 -> node(_oqihp_0, leaf, node(_erihp_0, _erihp_1, _erihp_2))  ;  t2 -> leaf
}


-------------------------------------------
Step 6, which took 0.065423 s (model generation: 0.064976,  model checking: 0.000447):

Clauses:
{
flip(leaf, leaf) <= True -> 0
eq_etree(_vb, t) <= flip(_ub, _vb) /\ flip(t, _ub) -> 0
flip(node(e, t1, t2), node(e, _pb, _qb)) <= flip(t1, _qb) /\ flip(t2, _pb) -> 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
False <= flip(node(a, leaf, leaf), leaf)
False <= flip(node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))
False <= flip(node(a, leaf, leaf), node(b, leaf, leaf))
flip(node(b, node(a, leaf, node(a, leaf, leaf)), leaf), node(b, leaf, node(b, leaf, leaf))) <= flip(node(a, leaf, node(a, leaf, leaf)), node(b, 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)
False <= flip(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), node(b, leaf, node(b, leaf, leaf))) /\ flip(node(b, leaf, node(b, leaf, leaf)), node(b, 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)
}
]



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




Answer of teacher:

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

eq_etree(_vb, t) <= flip(_ub, _vb) /\ flip(t, _ub)  :
Yes: {
_ub -> node(b, node(b, leaf, _luihp_2), leaf)  ;  _vb -> node(b, _ssihp_1, node(b, _muihp_1, leaf))  ;  t -> node(b, leaf, leaf)
}

flip(node(e, t1, t2), node(e, _pb, _qb)) <= flip(t1, _qb) /\ flip(t2, _pb)  :
No: ()


Total time: 0.236281
Learner time: 0.161757
Teacher time: 0.001937
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)
}
]



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