Solving ../../benchmarks/smtlib/true/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, _aca)) <= append(t1, l2, _aca)
}
eq_eltlist(_dca, _eca) <= append(_bca, _cca, _dca) /\ append(_bca, _cca, _eca)
)
}

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


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

Clause system for inference is:

{
append(nil, l2, l2) <= True -> 0
prefix(l1, _fca) <= append(l1, l2, _fca) -> 0
append(cons(h1, t1), l2, cons(h1, _aca)) <= append(t1, l2, _aca) -> 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.233762 seconds.
Yes: |_
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_2_0) /\ prefix(x_0_1, x_2_1)
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ prefix(x_0_1, x_2_1)
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  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_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(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}
_|
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.014038 s (model generation: 0.013878,  model checking: 0.000160):

Clauses:
{
append(nil, l2, l2) <= True -> 0
prefix(l1, _fca) <= append(l1, l2, _fca) -> 0
append(cons(h1, t1), l2, cons(h1, _aca)) <= append(t1, l2, _aca) -> 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(l1, _fca) <= append(l1, l2, _fca)  :
No: ()

append(cons(h1, t1), l2, cons(h1, _aca)) <= append(t1, l2, _aca)  :
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.018037 s (model generation: 0.017859,  model checking: 0.000178):

Clauses:
{
append(nil, l2, l2) <= True -> 0
prefix(l1, _fca) <= append(l1, l2, _fca) -> 0
append(cons(h1, t1), l2, cons(h1, _aca)) <= append(t1, l2, _aca) -> 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(_oxsba_0, _oxsba_1)
}

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

append(cons(h1, t1), l2, cons(h1, _aca)) <= append(t1, l2, _aca)  :
Yes: {
_aca -> 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.014960 s (model generation: 0.014878,  model checking: 0.000082):

Clauses:
{
append(nil, l2, l2) <= True -> 0
prefix(l1, _fca) <= append(l1, l2, _fca) -> 0
append(cons(h1, t1), l2, cons(h1, _aca)) <= append(t1, l2, _aca) -> 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(l1, _fca) <= append(l1, l2, _fca)  :
Yes: {
_fca -> cons(_yxsba_0, _yxsba_1)  ;  l1 -> nil  ;  l2 -> cons(_aysba_0, _aysba_1)
}

append(cons(h1, t1), l2, cons(h1, _aca)) <= append(t1, l2, _aca)  :
Yes: {
_aca -> cons(_bysba_0, _bysba_1)  ;  l2 -> cons(_cysba_0, _cysba_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.016547 s (model generation: 0.016454,  model checking: 0.000093):

Clauses:
{
append(nil, l2, l2) <= True -> 0
prefix(l1, _fca) <= append(l1, l2, _fca) -> 0
append(cons(h1, t1), l2, cons(h1, _aca)) <= append(t1, l2, _aca) -> 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
}

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, 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(l1, _fca) <= append(l1, l2, _fca)  :
No: ()

append(cons(h1, t1), l2, cons(h1, _aca)) <= append(t1, l2, _aca)  :
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(_hysba_0, _hysba_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.027774 s (model generation: 0.027605,  model checking: 0.000169):

Clauses:
{
append(nil, l2, l2) <= True -> 0
prefix(l1, _fca) <= append(l1, l2, _fca) -> 0
append(cons(h1, t1), l2, cons(h1, _aca)) <= append(t1, l2, _aca) -> 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(l1, _fca) <= append(l1, l2, _fca)  :
Yes: {
_fca -> cons(b, _pysba_1)  ;  l1 -> cons(_qysba_0, _qysba_1)  ;  l2 -> nil
}

append(cons(h1, t1), l2, cons(h1, _aca)) <= append(t1, l2, _aca)  :
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, _azsba_1)  ;  zs -> cons(_bzsba_0, _bzsba_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.019903 s (model generation: 0.019490,  model checking: 0.000413):

Clauses:
{
append(nil, l2, l2) <= True -> 0
prefix(l1, _fca) <= append(l1, l2, _fca) -> 0
append(cons(h1, t1), l2, cons(h1, _aca)) <= append(t1, l2, _aca) -> 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), 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)) <= _r_1(x_0_0, x_2_0)
  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, 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(l1, _fca) <= append(l1, l2, _fca)  :
Yes: {
_fca -> cons(a, _izsba_1)  ;  l1 -> cons(b, _jzsba_1)  ;  l2 -> cons(_kzsba_0, _kzsba_1)
}

append(cons(h1, t1), l2, cons(h1, _aca)) <= append(t1, l2, _aca)  :
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.022564 s (model generation: 0.022104,  model checking: 0.000460):

Clauses:
{
append(nil, l2, l2) <= True -> 0
prefix(l1, _fca) <= append(l1, l2, _fca) -> 0
append(cons(h1, t1), l2, cons(h1, _aca)) <= append(t1, l2, _aca) -> 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), nil, cons(b, nil))
False <= append(cons(b, nil), cons(a, nil), cons(a, 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_2_0)
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0)
  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, 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(l1, _fca) <= append(l1, l2, _fca)  :
Yes: {
_fca -> cons(b, nil)  ;  l1 -> cons(b, cons(_egtba_0, _egtba_1))  ;  l2 -> cons(_betba_0, _betba_1)
}

append(cons(h1, t1), l2, cons(h1, _aca)) <= append(t1, l2, _aca)  :
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 7, which took 0.023699 s (model generation: 0.023219,  model checking: 0.000480):

Clauses:
{
append(nil, l2, l2) <= True -> 0
prefix(l1, _fca) <= append(l1, l2, _fca) -> 0
append(cons(h1, t1), l2, cons(h1, _aca)) <= append(t1, l2, _aca) -> 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), nil, cons(b, nil))
prefix(cons(b, cons(a, nil)), cons(b, nil)) <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, nil))
False <= append(cons(b, nil), cons(a, nil), cons(a, 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)) <= _r_1(x_0_0, x_2_0)
  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, 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(l1, _fca) <= append(l1, l2, _fca)  :
Yes: {
_fca -> cons(_vitba_0, nil)  ;  l1 -> cons(b, cons(_altba_0, _altba_1))  ;  l2 -> cons(b, _xitba_1)
}

append(cons(h1, t1), l2, cons(h1, _aca)) <= append(t1, l2, _aca)  :
Yes: {
_aca -> cons(_kjtba_0, _kjtba_1)  ;  h1 -> b  ;  l2 -> cons(a, _ljtba_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.033384 s (model generation: 0.032818,  model checking: 0.000566):

Clauses:
{
append(nil, l2, l2) <= True -> 0
prefix(l1, _fca) <= append(l1, l2, _fca) -> 0
append(cons(h1, t1), l2, cons(h1, _aca)) <= append(t1, l2, _aca) -> 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(cons(b, nil), cons(a, nil), cons(b, 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), nil, cons(b, nil))
prefix(cons(b, cons(a, nil)), cons(b, nil)) <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, nil))
prefix(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(b, cons(a, nil)), cons(b, nil), cons(a, nil))
False <= append(cons(b, nil), cons(a, nil), cons(a, 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_2_0) /\ prefix(x_0_1, x_1_1)
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0)
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  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_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(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(l1, _fca) <= append(l1, l2, _fca)  :
Yes: {
_fca -> cons(b, nil)  ;  l1 -> cons(b, cons(_yqtba_0, _yqtba_1))  ;  l2 -> nil
}

append(cons(h1, t1), l2, cons(h1, _aca)) <= append(t1, l2, _aca)  :
Yes: {
_aca -> cons(b, _hotba_1)  ;  l2 -> cons(_iotba_0, nil)  ;  t1 -> cons(b, 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: ()


Total time: 0.233762
Learner time: 0.188305
Teacher time: 0.002601
Reasons for stopping: Yes: |_
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_2_0) /\ prefix(x_0_1, x_2_1)
  append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ prefix(x_0_1, x_2_1)
  append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True
  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_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(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}
_|