Solving ../../benchmarks/smtlib/true/swap_swap_eq_elt.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: {
elist -> {econs, enil}  ;  elt -> {a, b}  ;  epair -> {epairc}  ;  etree -> {leaf, node}  ;  nat -> {s, z}  ;  nlist -> {ncons, nnil}  ;  npair -> {npairc}
}
definition:
{
(swap_elt, F:
{
swap_elt(epairc(fst, snd), epairc(snd, fst)) <= True
}
eq_epair(_wc, _xc) <= swap_elt(_vc, _wc) /\ swap_elt(_vc, _xc)
)
}

properties:
{
eq_epair(p, _zc) <= swap_elt(_yc, _zc) /\ swap_elt(p, _yc)
}


over-approximation: {swap_elt}
under-approximation: {}

Clause system for inference is:

{
swap_elt(epairc(fst, snd), epairc(snd, fst)) <= True -> 0
eq_epair(p, _zc) <= swap_elt(_yc, _zc) /\ swap_elt(p, _yc) -> 0
}


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

swap_elt ->
[
swap_elt : <epair * epair>
{
  _r_1(a, a) <= True
  _r_1(b, b) <= True
  swap_elt(epairc(x_0_0, x_0_1), epairc(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_1(x_0_1, x_1_0)
}
]



--
Equality automata are defined for: {elist, elt, epair, etree, nat, nlist, npair}
_|
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006075 s (model generation: 0.006036,  model checking: 0.000039):

Clauses:
{
swap_elt(epairc(fst, snd), epairc(snd, fst)) <= True -> 0
eq_epair(p, _zc) <= swap_elt(_yc, _zc) /\ swap_elt(p, _yc) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

swap_elt ->
[
swap_elt : <epair * epair>
{
  
}
]



--
Equality automata are defined for: {elist, elt, epair, etree, nat, nlist, npair}
_|




Answer of teacher:

swap_elt(epairc(fst, snd), epairc(snd, fst)) <= True  :
Yes: {

}

eq_epair(p, _zc) <= swap_elt(_yc, _zc) /\ swap_elt(p, _yc)  :
No: ()


-------------------------------------------
Step 1, which took 0.006742 s (model generation: 0.006689,  model checking: 0.000053):

Clauses:
{
swap_elt(epairc(fst, snd), epairc(snd, fst)) <= True -> 0
eq_epair(p, _zc) <= swap_elt(_yc, _zc) /\ swap_elt(p, _yc) -> 0
}

Accumulated learning constraints:
{
swap_elt(epairc(a, a), epairc(a, a)) <= True
}

Current best model:
|_
name: None

swap_elt ->
[
swap_elt : <epair * epair>
{
  swap_elt(epairc(x_0_0, x_0_1), epairc(x_1_0, x_1_1)) <= True
}
]



--
Equality automata are defined for: {elist, elt, epair, etree, nat, nlist, npair}
_|




Answer of teacher:

swap_elt(epairc(fst, snd), epairc(snd, fst)) <= True  :
No: ()

eq_epair(p, _zc) <= swap_elt(_yc, _zc) /\ swap_elt(p, _yc)  :
Yes: {
_yc -> epairc(_zenad_0, _zenad_1)  ;  _zc -> epairc(a, _afnad_1)  ;  p -> epairc(b, _bfnad_1)
}


-------------------------------------------
Step 2, which took 0.011882 s (model generation: 0.010276,  model checking: 0.001606):

Clauses:
{
swap_elt(epairc(fst, snd), epairc(snd, fst)) <= True -> 0
eq_epair(p, _zc) <= swap_elt(_yc, _zc) /\ swap_elt(p, _yc) -> 0
}

Accumulated learning constraints:
{
swap_elt(epairc(a, a), epairc(a, a)) <= True
False <= swap_elt(epairc(b, a), epairc(a, a))
}

Current best model:
|_
name: None

swap_elt ->
[
swap_elt : <epair * epair>
{
  _r_1(a) <= True
  swap_elt(epairc(x_0_0, x_0_1), epairc(x_1_0, x_1_1)) <= _r_1(x_0_0)
}
]



--
Equality automata are defined for: {elist, elt, epair, etree, nat, nlist, npair}
_|




Answer of teacher:

swap_elt(epairc(fst, snd), epairc(snd, fst)) <= True  :
Yes: {
fst -> b
}

eq_epair(p, _zc) <= swap_elt(_yc, _zc) /\ swap_elt(p, _yc)  :
Yes: {
_yc -> epairc(a, _mfnad_1)  ;  _zc -> epairc(_nfnad_0, a)  ;  p -> epairc(a, b)
}


Total time: 0.043341
Learner time: 0.023001
Teacher time: 0.001698
Reasons for stopping: Yes: |_
name: None

swap_elt ->
[
swap_elt : <epair * epair>
{
  _r_1(a, a) <= True
  _r_1(b, b) <= True
  swap_elt(epairc(x_0_0, x_0_1), epairc(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_1(x_0_1, x_1_0)
}
]



--
Equality automata are defined for: {elist, elt, epair, etree, nat, nlist, npair}
_|