Solving ../../benchmarks/smtlib/true/swap_swap_eq_nat.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_nat, F:
{
swap_nat(npairc(fst, snd), npairc(snd, fst)) <= True
}
eq_npair(_rd, _sd) <= swap_nat(_qd, _rd) /\ swap_nat(_qd, _sd)
)
}

properties:
{
eq_npair(p, _ud) <= swap_nat(_td, _ud) /\ swap_nat(p, _td)
}


over-approximation: {swap_nat}
under-approximation: {}

Clause system for inference is:

{
swap_nat(npairc(fst, snd), npairc(snd, fst)) <= True -> 0
eq_npair(p, _ud) <= swap_nat(_td, _ud) /\ swap_nat(p, _td) -> 0
}


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

swap_nat ->
[
swap_nat : <npair * npair>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= True
  swap_nat(npairc(x_0_0, x_0_1), npairc(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.012655 s (model generation: 0.012574,  model checking: 0.000081):

Clauses:
{
swap_nat(npairc(fst, snd), npairc(snd, fst)) <= True -> 0
eq_npair(p, _ud) <= swap_nat(_td, _ud) /\ swap_nat(p, _td) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

swap_nat ->
[
swap_nat : <npair * npair>
{
  
}
]



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




Answer of teacher:

swap_nat(npairc(fst, snd), npairc(snd, fst)) <= True  :
Yes: {

}

eq_npair(p, _ud) <= swap_nat(_td, _ud) /\ swap_nat(p, _td)  :
No: ()


-------------------------------------------
Step 1, which took 0.018914 s (model generation: 0.018775,  model checking: 0.000139):

Clauses:
{
swap_nat(npairc(fst, snd), npairc(snd, fst)) <= True -> 0
eq_npair(p, _ud) <= swap_nat(_td, _ud) /\ swap_nat(p, _td) -> 0
}

Accumulated learning constraints:
{
swap_nat(npairc(z, z), npairc(z, z)) <= True
}

Current best model:
|_
name: None

swap_nat ->
[
swap_nat : <npair * npair>
{
  swap_nat(npairc(x_0_0, x_0_1), npairc(x_1_0, x_1_1)) <= True
}
]



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




Answer of teacher:

swap_nat(npairc(fst, snd), npairc(snd, fst)) <= True  :
No: ()

eq_npair(p, _ud) <= swap_nat(_td, _ud) /\ swap_nat(p, _td)  :
Yes: {
_td -> npairc(_qgnad_0, _qgnad_1)  ;  _ud -> npairc(_rgnad_0, s(_ygnad_0))  ;  p -> npairc(_sgnad_0, z)
}


-------------------------------------------
Step 2, which took 0.013415 s (model generation: 0.013333,  model checking: 0.000082):

Clauses:
{
swap_nat(npairc(fst, snd), npairc(snd, fst)) <= True -> 0
eq_npair(p, _ud) <= swap_nat(_td, _ud) /\ swap_nat(p, _td) -> 0
}

Accumulated learning constraints:
{
swap_nat(npairc(z, z), npairc(z, z)) <= True
False <= swap_nat(npairc(z, z), npairc(z, s(z)))
}

Current best model:
|_
name: None

swap_nat ->
[
swap_nat : <npair * npair>
{
  _r_1(z) <= True
  swap_nat(npairc(x_0_0, x_0_1), npairc(x_1_0, x_1_1)) <= _r_1(x_1_1)
}
]



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




Answer of teacher:

swap_nat(npairc(fst, snd), npairc(snd, fst)) <= True  :
Yes: {
fst -> s(_fhnad_0)
}

eq_npair(p, _ud) <= swap_nat(_td, _ud) /\ swap_nat(p, _td)  :
Yes: {
_td -> npairc(_zgnad_0, z)  ;  _ud -> npairc(s(_mhnad_0), z)  ;  p -> npairc(z, _bhnad_1)
}


-------------------------------------------
Step 3, which took 0.011168 s (model generation: 0.011056,  model checking: 0.000112):

Clauses:
{
swap_nat(npairc(fst, snd), npairc(snd, fst)) <= True -> 0
eq_npair(p, _ud) <= swap_nat(_td, _ud) /\ swap_nat(p, _td) -> 0
}

Accumulated learning constraints:
{
swap_nat(npairc(s(z), z), npairc(z, s(z))) <= True
swap_nat(npairc(z, z), npairc(z, z)) <= True
False <= swap_nat(npairc(z, z), npairc(s(z), z))
False <= swap_nat(npairc(z, z), npairc(z, s(z)))
}

Current best model:
|_
name: None

swap_nat ->
[
swap_nat : <npair * npair>
{
  _r_1(s(x_0_0), s(x_1_0)) <= True
  _r_1(z, z) <= True
  swap_nat(npairc(x_0_0, x_0_1), npairc(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}
_|




Answer of teacher:

swap_nat(npairc(fst, snd), npairc(snd, fst)) <= True  :
No: ()

eq_npair(p, _ud) <= swap_nat(_td, _ud) /\ swap_nat(p, _td)  :
Yes: {
_td -> npairc(s(_ainad_0), z)  ;  _ud -> npairc(z, s(s(_hinad_0)))  ;  p -> npairc(z, s(z))
}


-------------------------------------------
Step 4, which took 0.011216 s (model generation: 0.011081,  model checking: 0.000135):

Clauses:
{
swap_nat(npairc(fst, snd), npairc(snd, fst)) <= True -> 0
eq_npair(p, _ud) <= swap_nat(_td, _ud) /\ swap_nat(p, _td) -> 0
}

Accumulated learning constraints:
{
swap_nat(npairc(s(z), z), npairc(z, s(z))) <= True
swap_nat(npairc(z, z), npairc(z, z)) <= True
False <= swap_nat(npairc(s(z), z), npairc(z, s(s(z)))) /\ swap_nat(npairc(z, s(z)), npairc(s(z), z))
False <= swap_nat(npairc(z, z), npairc(s(z), z))
False <= swap_nat(npairc(z, z), npairc(z, s(z)))
}

Current best model:
|_
name: None

swap_nat ->
[
swap_nat : <npair * npair>
{
  _r_1(s(x_0_0), s(x_1_0)) <= True
  _r_1(s(x_0_0), z) <= True
  _r_1(z, z) <= True
  swap_nat(npairc(x_0_0, x_0_1), npairc(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_1(x_0_0, x_1_1)
}
]



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




Answer of teacher:

swap_nat(npairc(fst, snd), npairc(snd, fst)) <= True  :
Yes: {
fst -> z  ;  snd -> s(_nknad_0)
}

eq_npair(p, _ud) <= swap_nat(_td, _ud) /\ swap_nat(p, _td)  :
Yes: {
_td -> npairc(s(_vinad_0), s(_uinad_0))  ;  _ud -> npairc(z, s(_winad_0))  ;  p -> npairc(s(_tinad_0), _kinad_1)
}


Total time: 0.079753
Learner time: 0.066819
Teacher time: 0.000549
Reasons for stopping: Yes: |_
name: None

swap_nat ->
[
swap_nat : <npair * npair>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= True
  swap_nat(npairc(x_0_0, x_0_1), npairc(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}
_|