Solving ../../benchmarks/smtlib/true/tree_nat_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: {
nat -> {s, z}  ;  nattree -> {leaf, node}
}
definition:
{
(flip, F:
{
flip(leaf, leaf) <= True
flip(node(e, t1, t2), node(e, _nha, _oha)) <= flip(t1, _oha) /\ flip(t2, _nha)
}
eq_nattree(_qha, _rha) <= flip(_pha, _qha) /\ flip(_pha, _rha)
)
}

properties:
{
eq_nattree(_tha, t) <= flip(_sha, _tha) /\ flip(t, _sha)
}


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

Clause system for inference is:

{
flip(leaf, leaf) <= True -> 0
eq_nattree(_tha, t) <= flip(_sha, _tha) /\ flip(t, _sha) -> 0
flip(node(e, t1, t2), node(e, _nha, _oha)) <= flip(t1, _oha) /\ flip(t2, _nha) -> 0
}


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

flip ->
[
flip : <nattree * nattree>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= 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: {nat, nattree}
_|
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006538 s (model generation: 0.006495,  model checking: 0.000043):

Clauses:
{
flip(leaf, leaf) <= True -> 0
eq_nattree(_tha, t) <= flip(_sha, _tha) /\ flip(t, _sha) -> 0
flip(node(e, t1, t2), node(e, _nha, _oha)) <= flip(t1, _oha) /\ flip(t2, _nha) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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



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




Answer of teacher:

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

}

eq_nattree(_tha, t) <= flip(_sha, _tha) /\ flip(t, _sha)  :
No: ()

flip(node(e, t1, t2), node(e, _nha, _oha)) <= flip(t1, _oha) /\ flip(t2, _nha)  :
No: ()


-------------------------------------------
Step 1, which took 0.006313 s (model generation: 0.006270,  model checking: 0.000043):

Clauses:
{
flip(leaf, leaf) <= True -> 0
eq_nattree(_tha, t) <= flip(_sha, _tha) /\ flip(t, _sha) -> 0
flip(node(e, t1, t2), node(e, _nha, _oha)) <= flip(t1, _oha) /\ flip(t2, _nha) -> 0
}

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

Current best model:
|_
name: None

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



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




Answer of teacher:

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

eq_nattree(_tha, t) <= flip(_sha, _tha) /\ flip(t, _sha)  :
No: ()

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


-------------------------------------------
Step 2, which took 0.008686 s (model generation: 0.008595,  model checking: 0.000091):

Clauses:
{
flip(leaf, leaf) <= True -> 0
eq_nattree(_tha, t) <= flip(_sha, _tha) /\ flip(t, _sha) -> 0
flip(node(e, t1, t2), node(e, _nha, _oha)) <= flip(t1, _oha) /\ flip(t2, _nha) -> 0
}

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

Current best model:
|_
name: None

flip ->
[
flip : <nattree * nattree>
{
  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: {nat, nattree}
_|




Answer of teacher:

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

eq_nattree(_tha, t) <= flip(_sha, _tha) /\ flip(t, _sha)  :
Yes: {
_sha -> node(_hcjmw_0, _hcjmw_1, _hcjmw_2)  ;  _tha -> node(z, _icjmw_1, _icjmw_2)  ;  t -> node(s(_vcjmw_0), _jcjmw_1, _jcjmw_2)
}

flip(node(e, t1, t2), node(e, _nha, _oha)) <= flip(t1, _oha) /\ flip(t2, _nha)  :
No: ()


-------------------------------------------
Step 3, which took 0.010924 s (model generation: 0.010772,  model checking: 0.000152):

Clauses:
{
flip(leaf, leaf) <= True -> 0
eq_nattree(_tha, t) <= flip(_sha, _tha) /\ flip(t, _sha) -> 0
flip(node(e, t1, t2), node(e, _nha, _oha)) <= flip(t1, _oha) /\ flip(t2, _nha) -> 0
}

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

Current best model:
|_
name: None

flip ->
[
flip : <nattree * nattree>
{
  _r_1(z) <= 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)
}
]



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




Answer of teacher:

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

eq_nattree(_tha, t) <= flip(_sha, _tha) /\ flip(t, _sha)  :
Yes: {
_sha -> node(z, _zcjmw_1, _zcjmw_2)  ;  _tha -> node(_adjmw_0, node(_zdjmw_0, _zdjmw_1, _zdjmw_2), _adjmw_2)  ;  t -> node(z, leaf, _bdjmw_2)
}

flip(node(e, t1, t2), node(e, _nha, _oha)) <= flip(t1, _oha) /\ flip(t2, _nha)  :
Yes: {
_nha -> node(_rdjmw_0, _rdjmw_1, _rdjmw_2)  ;  _oha -> node(_sdjmw_0, _sdjmw_1, _sdjmw_2)  ;  e -> s(_wdjmw_0)  ;  t1 -> node(z, _tdjmw_1, _tdjmw_2)  ;  t2 -> node(z, _udjmw_1, _udjmw_2)
}


-------------------------------------------
Step 4, which took 0.017779 s (model generation: 0.017608,  model checking: 0.000171):

Clauses:
{
flip(leaf, leaf) <= True -> 0
eq_nattree(_tha, t) <= flip(_sha, _tha) /\ flip(t, _sha) -> 0
flip(node(e, t1, t2), node(e, _nha, _oha)) <= flip(t1, _oha) /\ flip(t2, _nha) -> 0
}

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

Current best model:
|_
name: None

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



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




Answer of teacher:

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

eq_nattree(_tha, t) <= flip(_sha, _tha) /\ flip(t, _sha)  :
Yes: {
_sha -> node(z, leaf, _nejmw_2)  ;  _tha -> node(_oejmw_0, leaf, node(_nfjmw_0, _nfjmw_1, _nfjmw_2))  ;  t -> node(z, _pejmw_1, leaf)
}

flip(node(e, t1, t2), node(e, _nha, _oha)) <= flip(t1, _oha) /\ flip(t2, _nha)  :
Yes: {
_nha -> leaf  ;  _oha -> node(_zejmw_0, leaf, _zejmw_2)  ;  e -> s(_kfjmw_0)  ;  t1 -> node(z, _afjmw_1, _afjmw_2)  ;  t2 -> leaf
}


-------------------------------------------
Step 5, which took 0.020986 s (model generation: 0.020664,  model checking: 0.000322):

Clauses:
{
flip(leaf, leaf) <= True -> 0
eq_nattree(_tha, t) <= flip(_sha, _tha) /\ flip(t, _sha) -> 0
flip(node(e, t1, t2), node(e, _nha, _oha)) <= flip(t1, _oha) /\ flip(t2, _nha) -> 0
}

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

Current best model:
|_
name: None

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



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




Answer of teacher:

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

eq_nattree(_tha, t) <= flip(_sha, _tha) /\ flip(t, _sha)  :
Yes: {
_sha -> leaf  ;  _tha -> leaf  ;  t -> node(_xfjmw_0, _xfjmw_1, _xfjmw_2)
}

flip(node(e, t1, t2), node(e, _nha, _oha)) <= flip(t1, _oha) /\ flip(t2, _nha)  :
Yes: {
_nha -> leaf  ;  _oha -> leaf  ;  e -> s(_ejjmw_0)  ;  t1 -> node(_ygjmw_0, _ygjmw_1, _ygjmw_2)  ;  t2 -> leaf
}


-------------------------------------------
Step 6, which took 0.021921 s (model generation: 0.021589,  model checking: 0.000332):

Clauses:
{
flip(leaf, leaf) <= True -> 0
eq_nattree(_tha, t) <= flip(_sha, _tha) /\ flip(t, _sha) -> 0
flip(node(e, t1, t2), node(e, _nha, _oha)) <= flip(t1, _oha) /\ flip(t2, _nha) -> 0
}

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

Current best model:
|_
name: None

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



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




Answer of teacher:

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

eq_nattree(_tha, t) <= flip(_sha, _tha) /\ flip(t, _sha)  :
Yes: {
_sha -> node(z, node(_cmjmw_0, leaf, leaf), leaf)  ;  _tha -> node(_mjjmw_0, leaf, leaf)  ;  t -> node(z, _njjmw_1, node(z, _bmjmw_1, leaf))
}

flip(node(e, t1, t2), node(e, _nha, _oha)) <= flip(t1, _oha) /\ flip(t2, _nha)  :
Yes: {
_nha -> leaf  ;  _oha -> leaf  ;  e -> s(_ykjmw_0)  ;  t1 -> leaf  ;  t2 -> leaf
}


-------------------------------------------
Step 7, which took 0.025395 s (model generation: 0.024153,  model checking: 0.001242):

Clauses:
{
flip(leaf, leaf) <= True -> 0
eq_nattree(_tha, t) <= flip(_sha, _tha) /\ flip(t, _sha) -> 0
flip(node(e, t1, t2), node(e, _nha, _oha)) <= flip(t1, _oha) /\ flip(t2, _nha) -> 0
}

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

Current best model:
|_
name: None

flip ->
[
flip : <nattree * nattree>
{
  _r_1(s(x_0_0), s(x_1_0)) <= True
  _r_1(z, z) <= 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: {nat, nattree}
_|




Answer of teacher:

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

eq_nattree(_tha, t) <= flip(_sha, _tha) /\ flip(t, _sha)  :
Yes: {
_sha -> node(s(_dpjmw_0), leaf, leaf)  ;  _tha -> node(s(z), leaf, leaf)  ;  t -> node(s(s(_kpjmw_0)), leaf, leaf)
}

flip(node(e, t1, t2), node(e, _nha, _oha)) <= flip(t1, _oha) /\ flip(t2, _nha)  :
No: ()


Total time: 0.148856
Learner time: 0.116146
Teacher time: 0.002396
Reasons for stopping: Yes: |_
name: None

flip ->
[
flip : <nattree * nattree>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= 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: {nat, nattree}
_|