Solving ../../benchmarks/smtlib/false/prefix_append.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}  ;  eltlist -> {cons, nil}
}
definition:
{
(prefix, P:
{
prefix(nil, y) <= True
prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys)
prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys))
eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys))
False <= prefix(cons(z, zs), nil)
}
)
(append, F:
{
append(nil, l2, l2) <= True
append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb)
}
eq_eltlist(_qfb, _rfb) <= append(_ofb, _pfb, _qfb) /\ append(_ofb, _pfb, _rfb)
)
}

properties:
{
prefix(l2, _sfb) <= append(l1, l2, _sfb)
}


over-approximation: {append}
under-approximation: {prefix}

Clause system for inference is:

{
append(nil, l2, l2) <= True -> 0
prefix(l2, _sfb) <= append(l1, l2, _sfb) -> 0
append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb) -> 0
prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0
prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0
eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys)) -> 0
False <= prefix(cons(z, zs), nil) -> 0
}


Solving took 0.681375 seconds.
No: Contradictory set of ground constraints:
{
False <= True
append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True
append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True
append(cons(a, nil), nil, cons(a, nil)) <= True
append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True
append(nil, cons(a, nil), cons(a, nil)) <= True
append(nil, cons(b, nil), cons(b, nil)) <= True
append(nil, nil, nil) <= True
prefix(cons(a, nil), cons(a, nil)) <= True
prefix(cons(b, nil), cons(b, nil)) <= True
prefix(nil, cons(a, nil)) <= True
prefix(nil, nil) <= True
append(cons(b, cons(a, nil)), cons(a, cons(a, nil)), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil))
False <= append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil)))
False <= append(cons(a, nil), cons(b, nil), cons(a, nil))
False <= append(cons(b, nil), cons(b, nil), cons(a, nil))
False <= append(nil, cons(a, cons(a, nil)), cons(a, nil))
append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) <= append(nil, cons(a, cons(b, nil)), cons(a, cons(b, nil)))
False <= append(nil, cons(a, nil), cons(b, nil))
prefix(cons(b, cons(a, nil)), cons(b, nil)) <= append(nil, cons(b, cons(a, nil)), cons(b, nil))
False <= prefix(cons(a, cons(a, nil)), cons(a, cons(b, nil)))
False <= prefix(cons(a, cons(a, nil)), cons(a, nil))
False <= prefix(cons(a, nil), cons(b, cons(a, nil)))
False <= prefix(cons(a, nil), cons(b, nil))
False <= prefix(cons(a, nil), nil)
False <= prefix(cons(b, cons(b, nil)), cons(b, cons(a, nil)))
False <= prefix(cons(b, nil), cons(a, cons(a, nil)))
False <= prefix(cons(b, nil), cons(a, nil))
}
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006357 s (model generation: 0.006283,  model checking: 0.000074):

Clauses:
{
append(nil, l2, l2) <= True -> 0
prefix(l2, _sfb) <= append(l1, l2, _sfb) -> 0
append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb) -> 0
prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0
prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0
eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys)) -> 0
False <= prefix(cons(z, zs), nil) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

append ->
[
append : <eltlist * eltlist * eltlist>
{
  
}
]


;
prefix ->
[
prefix : <eltlist * eltlist>
{
  
}
]



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




Answer of teacher:

append(nil, l2, l2) <= True  :
Yes: {
l2 -> nil
}

prefix(l2, _sfb) <= append(l1, l2, _sfb)  :
No: ()

append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb)  :
No: ()

prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys)  :
No: ()

prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys))  :
No: ()

eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys))  :
No: ()

False <= prefix(cons(z, zs), nil)  :
No: ()


-------------------------------------------
Step 1, which took 0.006136 s (model generation: 0.006059,  model checking: 0.000077):

Clauses:
{
append(nil, l2, l2) <= True -> 0
prefix(l2, _sfb) <= append(l1, l2, _sfb) -> 0
append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb) -> 0
prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0
prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0
eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys)) -> 0
False <= prefix(cons(z, zs), nil) -> 0
}

Accumulated learning constraints:
{
append(nil, nil, nil) <= True
}

Current best model:
|_
name: None

append ->
[
append : <eltlist * eltlist * eltlist>
{
  append(nil, nil, nil) <= True
}
]


;
prefix ->
[
prefix : <eltlist * eltlist>
{
  
}
]



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




Answer of teacher:

append(nil, l2, l2) <= True  :
Yes: {
l2 -> cons(_zgpqw_0, _zgpqw_1)
}

prefix(l2, _sfb) <= append(l1, l2, _sfb)  :
Yes: {
_sfb -> nil  ;  l1 -> nil  ;  l2 -> nil
}

append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb)  :
Yes: {
_nfb -> nil  ;  l2 -> nil  ;  t1 -> nil
}

prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys)  :
No: ()

prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys))  :
No: ()

eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys))  :
No: ()

False <= prefix(cons(z, zs), nil)  :
No: ()


-------------------------------------------
Step 2, which took 0.007975 s (model generation: 0.007895,  model checking: 0.000080):

Clauses:
{
append(nil, l2, l2) <= True -> 0
prefix(l2, _sfb) <= append(l1, l2, _sfb) -> 0
append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb) -> 0
prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0
prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0
eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys)) -> 0
False <= prefix(cons(z, zs), nil) -> 0
}

Accumulated learning constraints:
{
append(cons(a, nil), nil, cons(a, nil)) <= True
append(nil, cons(a, nil), cons(a, nil)) <= True
append(nil, nil, nil) <= True
prefix(nil, nil) <= True
}

Current best model:
|_
name: None

append ->
[
append : <eltlist * eltlist * eltlist>
{
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(nil, nil, nil) <= True
}
]


;
prefix ->
[
prefix : <eltlist * eltlist>
{
  prefix(nil, nil) <= True
}
]



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




Answer of teacher:

append(nil, l2, l2) <= True  :
No: ()

prefix(l2, _sfb) <= append(l1, l2, _sfb)  :
Yes: {
_sfb -> cons(_jhpqw_0, _jhpqw_1)  ;  l1 -> nil  ;  l2 -> cons(_lhpqw_0, _lhpqw_1)
}

append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb)  :
Yes: {
_nfb -> cons(_mhpqw_0, _mhpqw_1)  ;  l2 -> cons(_nhpqw_0, _nhpqw_1)  ;  t1 -> nil
}

prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys)  :
Yes: {
ys -> nil  ;  zs -> nil
}

prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys))  :
No: ()

eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys))  :
No: ()

False <= prefix(cons(z, zs), nil)  :
No: ()


-------------------------------------------
Step 3, which took 0.011935 s (model generation: 0.011015,  model checking: 0.000920):

Clauses:
{
append(nil, l2, l2) <= True -> 0
prefix(l2, _sfb) <= append(l1, l2, _sfb) -> 0
append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb) -> 0
prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0
prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0
eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys)) -> 0
False <= prefix(cons(z, zs), nil) -> 0
}

Accumulated learning constraints:
{
append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True
append(cons(a, nil), nil, cons(a, nil)) <= True
append(nil, cons(a, nil), cons(a, nil)) <= True
append(nil, nil, nil) <= True
prefix(cons(a, nil), cons(a, nil)) <= True
prefix(nil, nil) <= True
}

Current best model:
|_
name: None

append ->
[
append : <eltlist * eltlist * eltlist>
{
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(nil, nil, nil) <= True
}
]


;
prefix ->
[
prefix : <eltlist * eltlist>
{
  prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True
  prefix(nil, nil) <= True
}
]



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




Answer of teacher:

append(nil, l2, l2) <= True  :
No: ()

prefix(l2, _sfb) <= append(l1, l2, _sfb)  :
Yes: {
_sfb -> cons(_rhpqw_0, _rhpqw_1)  ;  l1 -> cons(_shpqw_0, _shpqw_1)  ;  l2 -> nil
}

append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb)  :
No: ()

prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys)  :
No: ()

prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys))  :
Yes: {
ys -> nil  ;  zs -> cons(_vhpqw_0, _vhpqw_1)
}

eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys))  :
Yes: {
y2 -> b  ;  z -> a
}

False <= prefix(cons(z, zs), nil)  :
No: ()


-------------------------------------------
Step 4, which took 0.018461 s (model generation: 0.018327,  model checking: 0.000134):

Clauses:
{
append(nil, l2, l2) <= True -> 0
prefix(l2, _sfb) <= append(l1, l2, _sfb) -> 0
append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb) -> 0
prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0
prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0
eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys)) -> 0
False <= prefix(cons(z, zs), nil) -> 0
}

Accumulated learning constraints:
{
append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True
append(cons(a, nil), nil, cons(a, nil)) <= True
append(nil, cons(a, nil), cons(a, nil)) <= True
append(nil, nil, nil) <= True
prefix(cons(a, nil), cons(a, nil)) <= True
prefix(nil, cons(a, nil)) <= True
prefix(nil, nil) <= True
prefix(cons(a, nil), nil) <= prefix(cons(a, cons(a, nil)), cons(a, nil))
False <= prefix(cons(a, nil), cons(b, nil))
}

Current best model:
|_
name: None

append ->
[
append : <eltlist * eltlist * eltlist>
{
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(nil, nil, nil) <= True
}
]


;
prefix ->
[
prefix : <eltlist * eltlist>
{
  _r_1(a) <= True
  prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_0)
  prefix(cons(x_0_0, x_0_1), nil) <= True
  prefix(nil, cons(x_1_0, x_1_1)) <= True
  prefix(nil, nil) <= True
}
]



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




Answer of teacher:

append(nil, l2, l2) <= True  :
No: ()

prefix(l2, _sfb) <= append(l1, l2, _sfb)  :
Yes: {
_sfb -> cons(b, _fipqw_1)  ;  l1 -> nil  ;  l2 -> cons(_hipqw_0, _hipqw_1)
}

append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb)  :
No: ()

prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys)  :
Yes: {
y2 -> b  ;  ys -> nil  ;  zs -> nil
}

prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys))  :
Yes: {
y2 -> a  ;  ys -> cons(b, _qipqw_1)  ;  zs -> cons(_ripqw_0, _ripqw_1)
}

eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys))  :
Yes: {
y2 -> a  ;  z -> b
}

False <= prefix(cons(z, zs), nil)  :
Yes: {

}


-------------------------------------------
Step 5, which took 0.021217 s (model generation: 0.020769,  model checking: 0.000448):

Clauses:
{
append(nil, l2, l2) <= True -> 0
prefix(l2, _sfb) <= append(l1, l2, _sfb) -> 0
append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb) -> 0
prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0
prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0
eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys)) -> 0
False <= prefix(cons(z, zs), nil) -> 0
}

Accumulated learning constraints:
{
append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True
append(cons(a, nil), nil, cons(a, nil)) <= True
append(nil, cons(a, nil), cons(a, nil)) <= True
append(nil, nil, nil) <= True
prefix(cons(a, nil), cons(a, nil)) <= True
prefix(cons(b, nil), cons(b, nil)) <= True
prefix(nil, cons(a, nil)) <= True
prefix(nil, nil) <= True
False <= append(nil, cons(a, nil), cons(b, nil))
False <= prefix(cons(a, cons(a, nil)), cons(a, cons(b, nil)))
False <= prefix(cons(a, cons(a, nil)), cons(a, nil))
False <= prefix(cons(a, nil), cons(b, nil))
False <= prefix(cons(a, nil), nil)
False <= prefix(cons(b, nil), cons(a, nil))
}

Current best model:
|_
name: None

append ->
[
append : <eltlist * eltlist * eltlist>
{
  _r_1(a, a) <= True
  _r_1(b, b) <= True
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_0)
  append(nil, nil, nil) <= True
}
]


;
prefix ->
[
prefix : <eltlist * eltlist>
{
  _r_1(a, a) <= True
  _r_1(b, b) <= True
  prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ prefix(x_0_1, x_1_1)
  prefix(nil, cons(x_1_0, x_1_1)) <= True
  prefix(nil, nil) <= True
}
]



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




Answer of teacher:

append(nil, l2, l2) <= True  :
No: ()

prefix(l2, _sfb) <= append(l1, l2, _sfb)  :
Yes: {
_sfb -> cons(a, _zipqw_1)  ;  l1 -> cons(_ajpqw_0, _ajpqw_1)  ;  l2 -> cons(b, _bjpqw_1)
}

append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb)  :
No: ()

prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys)  :
No: ()

prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys))  :
No: ()

eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys))  :
No: ()

False <= prefix(cons(z, zs), nil)  :
No: ()


-------------------------------------------
Step 6, which took 0.023700 s (model generation: 0.023190,  model checking: 0.000510):

Clauses:
{
append(nil, l2, l2) <= True -> 0
prefix(l2, _sfb) <= append(l1, l2, _sfb) -> 0
append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb) -> 0
prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0
prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0
eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys)) -> 0
False <= prefix(cons(z, zs), nil) -> 0
}

Accumulated learning constraints:
{
append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True
append(cons(a, nil), nil, cons(a, nil)) <= True
append(nil, cons(a, nil), cons(a, nil)) <= True
append(nil, nil, nil) <= True
prefix(cons(a, nil), cons(a, nil)) <= True
prefix(cons(b, nil), cons(b, nil)) <= True
prefix(nil, cons(a, nil)) <= True
prefix(nil, nil) <= True
False <= append(cons(a, nil), cons(b, nil), cons(a, nil))
False <= append(nil, cons(a, nil), cons(b, nil))
False <= prefix(cons(a, cons(a, nil)), cons(a, cons(b, nil)))
False <= prefix(cons(a, cons(a, nil)), cons(a, nil))
False <= prefix(cons(a, nil), cons(b, nil))
False <= prefix(cons(a, nil), nil)
False <= prefix(cons(b, nil), cons(a, nil))
}

Current best model:
|_
name: None

append ->
[
append : <eltlist * eltlist * eltlist>
{
  _r_1(a, a) <= True
  _r_1(b, b) <= True
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_0)
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_0)
  append(nil, nil, nil) <= True
}
]


;
prefix ->
[
prefix : <eltlist * eltlist>
{
  _r_1(a, a) <= True
  _r_1(b, b) <= True
  prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ prefix(x_0_1, x_1_1)
  prefix(nil, cons(x_1_0, x_1_1)) <= True
  prefix(nil, nil) <= True
}
]



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




Answer of teacher:

append(nil, l2, l2) <= True  :
No: ()

prefix(l2, _sfb) <= append(l1, l2, _sfb)  :
Yes: {
_sfb -> cons(b, nil)  ;  l1 -> nil  ;  l2 -> cons(b, cons(_qppqw_0, _qppqw_1))
}

append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb)  :
Yes: {
_nfb -> cons(b, _xnpqw_1)  ;  h1 -> a  ;  l2 -> cons(b, _ynpqw_1)  ;  t1 -> nil
}

prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys)  :
No: ()

prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys))  :
No: ()

eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys))  :
No: ()

False <= prefix(cons(z, zs), nil)  :
No: ()


-------------------------------------------
Step 7, which took 0.064077 s (model generation: 0.063556,  model checking: 0.000521):

Clauses:
{
append(nil, l2, l2) <= True -> 0
prefix(l2, _sfb) <= append(l1, l2, _sfb) -> 0
append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb) -> 0
prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0
prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0
eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys)) -> 0
False <= prefix(cons(z, zs), nil) -> 0
}

Accumulated learning constraints:
{
append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True
append(cons(a, nil), nil, cons(a, nil)) <= True
append(nil, cons(a, nil), cons(a, nil)) <= True
append(nil, nil, nil) <= True
prefix(cons(a, nil), cons(a, nil)) <= True
prefix(cons(b, nil), cons(b, nil)) <= True
prefix(nil, cons(a, nil)) <= True
prefix(nil, nil) <= True
False <= append(cons(a, nil), cons(b, nil), cons(a, nil))
False <= append(nil, cons(a, nil), cons(b, nil))
prefix(cons(b, cons(a, nil)), cons(b, nil)) <= append(nil, cons(b, cons(a, nil)), cons(b, nil))
append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, nil))
False <= prefix(cons(a, cons(a, nil)), cons(a, cons(b, nil)))
False <= prefix(cons(a, cons(a, nil)), cons(a, nil))
False <= prefix(cons(a, nil), cons(b, nil))
False <= prefix(cons(a, nil), nil)
False <= prefix(cons(b, nil), cons(a, nil))
}

Current best model:
|_
name: None

append ->
[
append : <eltlist * eltlist * eltlist>
{
  _r_1(a, a) <= True
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_0)
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_0)
  append(nil, nil, nil) <= True
}
]


;
prefix ->
[
prefix : <eltlist * eltlist>
{
  _r_2(a, a) <= True
  _r_2(b, b) <= True
  prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_0, x_1_0) /\ prefix(x_0_1, x_1_1)
  prefix(nil, cons(x_1_0, x_1_1)) <= True
  prefix(nil, nil) <= True
}
]



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




Answer of teacher:

append(nil, l2, l2) <= True  :
Yes: {
l2 -> cons(b, _espqw_1)
}

prefix(l2, _sfb) <= append(l1, l2, _sfb)  :
Yes: {
_sfb -> cons(a, nil)  ;  l1 -> nil  ;  l2 -> cons(a, cons(_jupqw_0, _jupqw_1))
}

append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb)  :
Yes: {
_nfb -> cons(a, _uspqw_1)  ;  h1 -> b  ;  l2 -> cons(a, _vspqw_1)  ;  t1 -> nil
}

prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys)  :
No: ()

prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys))  :
No: ()

eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys))  :
No: ()

False <= prefix(cons(z, zs), nil)  :
No: ()


-------------------------------------------
Step 8, which took 0.087719 s (model generation: 0.087079,  model checking: 0.000640):

Clauses:
{
append(nil, l2, l2) <= True -> 0
prefix(l2, _sfb) <= append(l1, l2, _sfb) -> 0
append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb) -> 0
prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0
prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0
eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys)) -> 0
False <= prefix(cons(z, zs), nil) -> 0
}

Accumulated learning constraints:
{
append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True
append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True
append(cons(a, nil), nil, cons(a, nil)) <= True
append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True
append(nil, cons(a, nil), cons(a, nil)) <= True
append(nil, cons(b, nil), cons(b, nil)) <= True
append(nil, nil, nil) <= True
prefix(cons(a, nil), cons(a, nil)) <= True
prefix(cons(b, nil), cons(b, nil)) <= True
prefix(nil, cons(a, nil)) <= True
prefix(nil, nil) <= True
False <= append(cons(a, nil), cons(b, nil), cons(a, nil))
False <= append(nil, cons(a, cons(a, nil)), cons(a, nil))
False <= append(nil, cons(a, nil), cons(b, nil))
prefix(cons(b, cons(a, nil)), cons(b, nil)) <= append(nil, cons(b, cons(a, nil)), cons(b, nil))
False <= prefix(cons(a, cons(a, nil)), cons(a, cons(b, nil)))
False <= prefix(cons(a, cons(a, nil)), cons(a, nil))
False <= prefix(cons(a, nil), cons(b, nil))
False <= prefix(cons(a, nil), nil)
False <= prefix(cons(b, nil), cons(a, nil))
}

Current best model:
|_
name: None

append ->
[
append : <eltlist * eltlist * eltlist>
{
  _r_1(nil, cons(x_1_0, x_1_1)) <= True
  _r_2(a, a) <= True
  _r_2(b, b) <= True
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0) /\ prefix(x_1_1, x_2_1)
  append(nil, nil, nil) <= True
  prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_0, x_1_0) /\ prefix(x_0_1, x_1_1)
  prefix(nil, cons(x_1_0, x_1_1)) <= True
  prefix(nil, nil) <= True
}
]


;
prefix ->
[
prefix : <eltlist * eltlist>
{
  _r_2(a, a) <= True
  _r_2(b, b) <= True
  prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_0, x_1_0) /\ prefix(x_0_1, x_1_1)
  prefix(nil, cons(x_1_0, x_1_1)) <= True
  prefix(nil, nil) <= True
}
]



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




Answer of teacher:

append(nil, l2, l2) <= True  :
No: ()

prefix(l2, _sfb) <= append(l1, l2, _sfb)  :
Yes: {
_sfb -> cons(a, cons(_oypqw_0, _oypqw_1))  ;  l1 -> cons(_axpqw_0, _axpqw_1)  ;  l2 -> cons(b, nil)
}

append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb)  :
Yes: {
_nfb -> cons(a, cons(b, nil))  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
}

prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys)  :
No: ()

prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys))  :
No: ()

eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys))  :
No: ()

False <= prefix(cons(z, zs), nil)  :
No: ()


-------------------------------------------
Step 9, which took 0.165188 s (model generation: 0.163964,  model checking: 0.001224):

Clauses:
{
append(nil, l2, l2) <= True -> 0
prefix(l2, _sfb) <= append(l1, l2, _sfb) -> 0
append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb) -> 0
prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0
prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0
eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys)) -> 0
False <= prefix(cons(z, zs), nil) -> 0
}

Accumulated learning constraints:
{
append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True
append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True
append(cons(a, nil), nil, cons(a, nil)) <= True
append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True
append(nil, cons(a, nil), cons(a, nil)) <= True
append(nil, cons(b, nil), cons(b, nil)) <= True
append(nil, nil, nil) <= True
prefix(cons(a, nil), cons(a, nil)) <= True
prefix(cons(b, nil), cons(b, nil)) <= True
prefix(nil, cons(a, nil)) <= True
prefix(nil, nil) <= True
prefix(cons(b, nil), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil)))
False <= append(cons(a, nil), cons(b, nil), cons(a, nil))
False <= append(nil, cons(a, cons(a, nil)), cons(a, nil))
append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) <= append(nil, cons(a, cons(b, nil)), cons(a, cons(b, nil)))
False <= append(nil, cons(a, nil), cons(b, nil))
prefix(cons(b, cons(a, nil)), cons(b, nil)) <= append(nil, cons(b, cons(a, nil)), cons(b, nil))
False <= prefix(cons(a, cons(a, nil)), cons(a, cons(b, nil)))
False <= prefix(cons(a, cons(a, nil)), cons(a, nil))
False <= prefix(cons(a, nil), cons(b, nil))
False <= prefix(cons(a, nil), nil)
False <= prefix(cons(b, nil), cons(a, nil))
}

Current best model:
|_
name: None

append ->
[
append : <eltlist * eltlist * eltlist>
{
  _r_1(nil, cons(x_1_0, x_1_1)) <= True
  _r_2(a, a) <= True
  _r_2(b, b) <= True
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1)
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_0, x_1_0)
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0) /\ prefix(x_1_1, x_2_1)
  append(nil, nil, nil) <= True
  prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1)
  prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_0, x_1_0) /\ prefix(x_0_1, x_1_1)
  prefix(nil, cons(x_1_0, x_1_1)) <= True
  prefix(nil, nil) <= True
}
]


;
prefix ->
[
prefix : <eltlist * eltlist>
{
  _r_1(nil, cons(x_1_0, x_1_1)) <= True
  _r_2(a, a) <= True
  _r_2(b, b) <= True
  prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1)
  prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_0, x_1_0) /\ prefix(x_0_1, x_1_1)
  prefix(nil, cons(x_1_0, x_1_1)) <= True
  prefix(nil, nil) <= True
}
]



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




Answer of teacher:

append(nil, l2, l2) <= True  :
No: ()

prefix(l2, _sfb) <= append(l1, l2, _sfb)  :
Yes: {
_sfb -> cons(a, nil)  ;  l1 -> cons(b, _ocqqw_1)  ;  l2 -> cons(b, nil)
}

append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb)  :
Yes: {
_nfb -> cons(_cdqqw_0, _cdqqw_1)  ;  h1 -> b  ;  l2 -> cons(a, cons(_yeqqw_0, _yeqqw_1))  ;  t1 -> cons(a, _edqqw_1)
}

prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys)  :
No: ()

prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys))  :
No: ()

eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys))  :
Yes: {
y2 -> b  ;  ys -> cons(_afqqw_0, _afqqw_1)  ;  z -> a  ;  zs -> nil
}

False <= prefix(cons(z, zs), nil)  :
No: ()


-------------------------------------------
Step 10, which took 0.239079 s (model generation: 0.236921,  model checking: 0.002158):

Clauses:
{
append(nil, l2, l2) <= True -> 0
prefix(l2, _sfb) <= append(l1, l2, _sfb) -> 0
append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb) -> 0
prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0
prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0
eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys)) -> 0
False <= prefix(cons(z, zs), nil) -> 0
}

Accumulated learning constraints:
{
append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True
append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True
append(cons(a, nil), nil, cons(a, nil)) <= True
append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True
append(nil, cons(a, nil), cons(a, nil)) <= True
append(nil, cons(b, nil), cons(b, nil)) <= True
append(nil, nil, nil) <= True
prefix(cons(a, nil), cons(a, nil)) <= True
prefix(cons(b, nil), cons(b, nil)) <= True
prefix(nil, cons(a, nil)) <= True
prefix(nil, nil) <= True
append(cons(b, cons(a, nil)), cons(a, cons(a, nil)), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil))
prefix(cons(b, nil), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil)))
False <= append(cons(a, nil), cons(b, nil), cons(a, nil))
False <= append(cons(b, nil), cons(b, nil), cons(a, nil))
False <= append(nil, cons(a, cons(a, nil)), cons(a, nil))
append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) <= append(nil, cons(a, cons(b, nil)), cons(a, cons(b, nil)))
False <= append(nil, cons(a, nil), cons(b, nil))
prefix(cons(b, cons(a, nil)), cons(b, nil)) <= append(nil, cons(b, cons(a, nil)), cons(b, nil))
False <= prefix(cons(a, cons(a, nil)), cons(a, cons(b, nil)))
False <= prefix(cons(a, cons(a, nil)), cons(a, nil))
False <= prefix(cons(a, nil), cons(b, cons(a, nil)))
False <= prefix(cons(a, nil), cons(b, nil))
False <= prefix(cons(a, nil), nil)
False <= prefix(cons(b, nil), cons(a, nil))
}

Current best model:
|_
name: None

append ->
[
append : <eltlist * eltlist * eltlist>
{
  _r_1(b, cons(x_1_0, x_1_1)) <= True
  _r_2(a, a) <= True
  _r_2(b, b) <= True
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1)
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1)
  append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0)
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0) /\ prefix(x_1_1, x_2_1)
  append(nil, nil, nil) <= True
  prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1)
  prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_0, x_1_0) /\ prefix(x_0_1, x_1_1)
  prefix(nil, cons(x_1_0, x_1_1)) <= True
  prefix(nil, nil) <= True
}
]


;
prefix ->
[
prefix : <eltlist * eltlist>
{
  _r_1(b, cons(x_1_0, x_1_1)) <= True
  _r_2(a, a) <= True
  _r_2(b, b) <= True
  prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1)
  prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_0, x_1_0) /\ prefix(x_0_1, x_1_1)
  prefix(nil, cons(x_1_0, x_1_1)) <= True
  prefix(nil, nil) <= True
}
]



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




Answer of teacher:

append(nil, l2, l2) <= True  :
No: ()

prefix(l2, _sfb) <= append(l1, l2, _sfb)  :
Yes: {
_sfb -> cons(b, cons(_bqqqw_0, _bqqqw_1))  ;  l1 -> cons(b, _anqqw_1)  ;  l2 -> cons(a, _bnqqw_1)
}

append(cons(h1, t1), l2, cons(h1, _nfb)) <= append(t1, l2, _nfb)  :
No: ()

prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys)  :
No: ()

prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys))  :
Yes: {
y2 -> b  ;  ys -> cons(a, nil)  ;  zs -> cons(b, _apqqw_1)
}

eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys))  :
Yes: {
y2 -> a  ;  ys -> cons(_zpqqw_0, _zpqqw_1)  ;  z -> b
}

False <= prefix(cons(z, zs), nil)  :
No: ()


Total time: 0.681375
Learner time: 0.645058
Teacher time: 0.006786
Reasons for stopping: No: Contradictory set of ground constraints:
{
False <= True
append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True
append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True
append(cons(a, nil), nil, cons(a, nil)) <= True
append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True
append(nil, cons(a, nil), cons(a, nil)) <= True
append(nil, cons(b, nil), cons(b, nil)) <= True
append(nil, nil, nil) <= True
prefix(cons(a, nil), cons(a, nil)) <= True
prefix(cons(b, nil), cons(b, nil)) <= True
prefix(nil, cons(a, nil)) <= True
prefix(nil, nil) <= True
append(cons(b, cons(a, nil)), cons(a, cons(a, nil)), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil))
False <= append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil)))
False <= append(cons(a, nil), cons(b, nil), cons(a, nil))
False <= append(cons(b, nil), cons(b, nil), cons(a, nil))
False <= append(nil, cons(a, cons(a, nil)), cons(a, nil))
append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) <= append(nil, cons(a, cons(b, nil)), cons(a, cons(b, nil)))
False <= append(nil, cons(a, nil), cons(b, nil))
prefix(cons(b, cons(a, nil)), cons(b, nil)) <= append(nil, cons(b, cons(a, nil)), cons(b, nil))
False <= prefix(cons(a, cons(a, nil)), cons(a, cons(b, nil)))
False <= prefix(cons(a, cons(a, nil)), cons(a, nil))
False <= prefix(cons(a, nil), cons(b, cons(a, nil)))
False <= prefix(cons(a, nil), cons(b, nil))
False <= prefix(cons(a, nil), nil)
False <= prefix(cons(b, cons(b, nil)), cons(b, cons(a, nil)))
False <= prefix(cons(b, nil), cons(a, cons(a, nil)))
False <= prefix(cons(b, nil), cons(a, nil))
}