Solving ../../benchmarks/smtlib/true/insert_not_nil.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}
}
definition:
{
(not_nil_elt, P:
{
not_nil_elt(econs(x, ll)) <= True
False <= not_nil_elt(enil)
}
)
(leq_elt, P:
{
leq_elt(a, e2) <= True
leq_elt(b, b) <= True
False <= leq_elt(b, a)
}
)
(insert_elt, F:
{
insert_elt(x, enil, econs(x, enil)) <= True
insert_elt(x, econs(y, z), econs(y, _qu)) \/ leq_elt(x, y) <= insert_elt(x, z, _qu)
insert_elt(x, econs(y, z), econs(x, econs(y, z))) <= leq_elt(x, y)
}
eq_elist(_tu, _uu) <= insert_elt(_ru, _su, _tu) /\ insert_elt(_ru, _su, _uu)
)
}

properties:
{
not_nil_elt(_vu) <= insert_elt(e, l, _vu)
}


over-approximation: {insert_elt}
under-approximation: {not_nil_elt}

Clause system for inference is:

{
insert_elt(x, enil, econs(x, enil)) <= True -> 0
leq_elt(a, e2) <= True -> 0
leq_elt(b, b) <= True -> 0
not_nil_elt(_vu) <= insert_elt(e, l, _vu) -> 0
insert_elt(x, econs(y, z), econs(y, _qu)) \/ leq_elt(x, y) <= insert_elt(x, z, _qu) -> 0
insert_elt(x, econs(y, z), econs(x, econs(y, z))) <= leq_elt(x, y) -> 0
False <= leq_elt(b, a) -> 0
False <= not_nil_elt(enil) -> 0
}


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

insert_elt ->
[
insert_elt : <elt * elist * elist>
{
  insert_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  insert_elt(a, enil, econs(x_2_0, x_2_1)) <= True
  insert_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  insert_elt(b, enil, econs(x_2_0, x_2_1)) <= True
}
]


;
leq_elt ->
[
leq_elt : <elt * elt>
{
  leq_elt(a, a) <= True
  leq_elt(a, b) <= True
  leq_elt(b, b) <= True
}
]


;
not_nil_elt ->
[
not_nil_elt : <elist>
{
  not_nil_elt(econs(x_0_0, x_0_1)) <= True
}
]



--
Equality automata are defined for: {elist, elt}
_|
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006320 s (model generation: 0.006258,  model checking: 0.000062):

Clauses:
{
insert_elt(x, enil, econs(x, enil)) <= True -> 0
leq_elt(a, e2) <= True -> 0
leq_elt(b, b) <= True -> 0
not_nil_elt(_vu) <= insert_elt(e, l, _vu) -> 0
insert_elt(x, econs(y, z), econs(y, _qu)) \/ leq_elt(x, y) <= insert_elt(x, z, _qu) -> 0
insert_elt(x, econs(y, z), econs(x, econs(y, z))) <= leq_elt(x, y) -> 0
False <= leq_elt(b, a) -> 0
False <= not_nil_elt(enil) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

insert_elt ->
[
insert_elt : <elt * elist * elist>
{
  
}
]


;
leq_elt ->
[
leq_elt : <elt * elt>
{
  
}
]


;
not_nil_elt ->
[
not_nil_elt : <elist>
{
  
}
]



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




Answer of teacher:

insert_elt(x, enil, econs(x, enil)) <= True  :
Yes: {
x -> b
}

leq_elt(a, e2) <= True  :
Yes: {
e2 -> b
}

leq_elt(b, b) <= True  :
Yes: {

}

not_nil_elt(_vu) <= insert_elt(e, l, _vu)  :
No: ()

insert_elt(x, econs(y, z), econs(y, _qu)) \/ leq_elt(x, y) <= insert_elt(x, z, _qu)  :
No: ()

insert_elt(x, econs(y, z), econs(x, econs(y, z))) <= leq_elt(x, y)  :
No: ()

False <= leq_elt(b, a)  :
No: ()

False <= not_nil_elt(enil)  :
No: ()


-------------------------------------------
Step 1, which took 0.007241 s (model generation: 0.007167,  model checking: 0.000074):

Clauses:
{
insert_elt(x, enil, econs(x, enil)) <= True -> 0
leq_elt(a, e2) <= True -> 0
leq_elt(b, b) <= True -> 0
not_nil_elt(_vu) <= insert_elt(e, l, _vu) -> 0
insert_elt(x, econs(y, z), econs(y, _qu)) \/ leq_elt(x, y) <= insert_elt(x, z, _qu) -> 0
insert_elt(x, econs(y, z), econs(x, econs(y, z))) <= leq_elt(x, y) -> 0
False <= leq_elt(b, a) -> 0
False <= not_nil_elt(enil) -> 0
}

Accumulated learning constraints:
{
insert_elt(b, enil, econs(b, enil)) <= True
leq_elt(a, b) <= True
leq_elt(b, b) <= True
}

Current best model:
|_
name: None

insert_elt ->
[
insert_elt : <elt * elist * elist>
{
  insert_elt(b, enil, econs(x_2_0, x_2_1)) <= True
}
]


;
leq_elt ->
[
leq_elt : <elt * elt>
{
  leq_elt(a, b) <= True
  leq_elt(b, b) <= True
}
]


;
not_nil_elt ->
[
not_nil_elt : <elist>
{
  
}
]



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




Answer of teacher:

insert_elt(x, enil, econs(x, enil)) <= True  :
Yes: {
x -> a
}

leq_elt(a, e2) <= True  :
Yes: {
e2 -> a
}

leq_elt(b, b) <= True  :
No: ()

not_nil_elt(_vu) <= insert_elt(e, l, _vu)  :
Yes: {
_vu -> econs(_wioe_0, _wioe_1)  ;  e -> b  ;  l -> enil
}

insert_elt(x, econs(y, z), econs(y, _qu)) \/ leq_elt(x, y) <= insert_elt(x, z, _qu)  :
Yes: {
_qu -> econs(_zioe_0, _zioe_1)  ;  x -> b  ;  y -> a  ;  z -> enil
}

insert_elt(x, econs(y, z), econs(x, econs(y, z))) <= leq_elt(x, y)  :
Yes: {
x -> b  ;  y -> b
}

False <= leq_elt(b, a)  :
No: ()

False <= not_nil_elt(enil)  :
No: ()


-------------------------------------------
Step 2, which took 0.009970 s (model generation: 0.009880,  model checking: 0.000090):

Clauses:
{
insert_elt(x, enil, econs(x, enil)) <= True -> 0
leq_elt(a, e2) <= True -> 0
leq_elt(b, b) <= True -> 0
not_nil_elt(_vu) <= insert_elt(e, l, _vu) -> 0
insert_elt(x, econs(y, z), econs(y, _qu)) \/ leq_elt(x, y) <= insert_elt(x, z, _qu) -> 0
insert_elt(x, econs(y, z), econs(x, econs(y, z))) <= leq_elt(x, y) -> 0
False <= leq_elt(b, a) -> 0
False <= not_nil_elt(enil) -> 0
}

Accumulated learning constraints:
{
insert_elt(a, enil, econs(a, enil)) <= True
insert_elt(b, econs(b, enil), econs(b, econs(b, enil))) <= True
insert_elt(b, enil, econs(b, enil)) <= True
leq_elt(a, a) <= True
leq_elt(a, b) <= True
leq_elt(b, b) <= True
insert_elt(b, econs(a, enil), econs(a, econs(a, enil))) \/ leq_elt(b, a) <= insert_elt(b, enil, econs(a, enil))
not_nil_elt(econs(a, enil)) <= insert_elt(b, enil, econs(a, enil))
}

Current best model:
|_
name: None

insert_elt ->
[
insert_elt : <elt * elist * elist>
{
  insert_elt(a, enil, econs(x_2_0, x_2_1)) <= True
  insert_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  insert_elt(b, enil, econs(x_2_0, x_2_1)) <= True
}
]


;
leq_elt ->
[
leq_elt : <elt * elt>
{
  leq_elt(a, a) <= True
  leq_elt(a, b) <= True
  leq_elt(b, a) <= True
  leq_elt(b, b) <= True
}
]


;
not_nil_elt ->
[
not_nil_elt : <elist>
{
  not_nil_elt(econs(x_0_0, x_0_1)) <= True
}
]



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




Answer of teacher:

insert_elt(x, enil, econs(x, enil)) <= True  :
No: ()

leq_elt(a, e2) <= True  :
No: ()

leq_elt(b, b) <= True  :
No: ()

not_nil_elt(_vu) <= insert_elt(e, l, _vu)  :
No: ()

insert_elt(x, econs(y, z), econs(y, _qu)) \/ leq_elt(x, y) <= insert_elt(x, z, _qu)  :
No: ()

insert_elt(x, econs(y, z), econs(x, econs(y, z))) <= leq_elt(x, y)  :
Yes: {
x -> a  ;  y -> b
}

False <= leq_elt(b, a)  :
Yes: {

}

False <= not_nil_elt(enil)  :
No: ()


Total time: 0.040513
Learner time: 0.023305
Teacher time: 0.000226
Reasons for stopping: Yes: |_
name: None

insert_elt ->
[
insert_elt : <elt * elist * elist>
{
  insert_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  insert_elt(a, enil, econs(x_2_0, x_2_1)) <= True
  insert_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True
  insert_elt(b, enil, econs(x_2_0, x_2_1)) <= True
}
]


;
leq_elt ->
[
leq_elt : <elt * elt>
{
  leq_elt(a, a) <= True
  leq_elt(a, b) <= True
  leq_elt(b, b) <= True
}
]


;
not_nil_elt ->
[
not_nil_elt : <elist>
{
  not_nil_elt(econs(x_0_0, x_0_1)) <= True
}
]



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