Solving ../../benchmarks/false/append_equal.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: 60s
Convolution: left


Learning problem is:

env: {
nat -> {s, z}  ;  natlist -> {cons, nil}
}
definition:
{
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _wla])) -> append([cons(h1, t1), l2, cons(h1, _wla)])}
(append([_xla, _yla, _ama]) /\ append([_xla, _yla, _zla])) -> eq_natlist([_zla, _ama])
)
}

properties:
{(append([l1, cons(i, nil), _bma])) -> eq_natlist([l1, _bma])}


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
(append([l1, cons(i, nil), _bma])) -> eq_natlist([l1, _bma]) -> 0
(append([t1, l2, _wla])) -> append([cons(h1, t1), l2, cons(h1, _wla)]) -> 0
}


Solving took 0.129291 seconds.
Disproved
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.017052 s (model generation: 0.015799,  model checking: 0.001253):

Model:
|_
{
append -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
(append([l1, cons(i, nil), _bma])) -> eq_natlist([l1, _bma]) -> 1
(append([t1, l2, _wla])) -> append([cons(h1, t1), l2, cons(h1, _wla)]) -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 1, which took 0.016748 s (model generation: 0.016224,  model checking: 0.000524):

Model:
|_
{
append -> 
{{{
Q={q_gen_9040},
Q_f={q_gen_9040},
Delta=
{
<nil, nil, nil>() -> q_gen_9040
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
(append([l1, cons(i, nil), _bma])) -> eq_natlist([l1, _bma]) -> 1
(append([t1, l2, _wla])) -> append([cons(h1, t1), l2, cons(h1, _wla)]) -> 4
}
Sat witness: Found: ((append([t1, l2, _wla])) -> append([cons(h1, t1), l2, cons(h1, _wla)]), {
_wla -> nil  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 2, which took 0.017706 s (model generation: 0.016947,  model checking: 0.000759):

Model:
|_
{
append -> 
{{{
Q={q_gen_9040, q_gen_9042, q_gen_9043},
Q_f={q_gen_9040},
Delta=
{
<nil, nil>() -> q_gen_9042
<z, z>() -> q_gen_9043
<cons, nil, cons>(q_gen_9043, q_gen_9042) -> q_gen_9040
<nil, nil, nil>() -> q_gen_9040
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
(append([l1, cons(i, nil), _bma])) -> eq_natlist([l1, _bma]) -> 2
(append([t1, l2, _wla])) -> append([cons(h1, t1), l2, cons(h1, _wla)]) -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(s(z), cons(s(z), nil))
})

-------------------------------------------
Step 3, which took 0.018349 s (model generation: 0.018050,  model checking: 0.000299):

Model:
|_
{
append -> 
{{{
Q={q_gen_9040, q_gen_9042, q_gen_9043},
Q_f={q_gen_9040},
Delta=
{
<cons, cons>(q_gen_9043, q_gen_9042) -> q_gen_9042
<nil, nil>() -> q_gen_9042
<s, s>(q_gen_9043) -> q_gen_9043
<z, z>() -> q_gen_9043
<cons, nil, cons>(q_gen_9043, q_gen_9042) -> q_gen_9040
<nil, cons, cons>(q_gen_9043, q_gen_9042) -> q_gen_9040
<nil, nil, nil>() -> q_gen_9040
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
(append([l1, cons(i, nil), _bma])) -> eq_natlist([l1, _bma]) -> 5
(append([t1, l2, _wla])) -> append([cons(h1, t1), l2, cons(h1, _wla)]) -> 4
}
Sat witness: Found: ((append([l1, cons(i, nil), _bma])) -> eq_natlist([l1, _bma]), {
_bma -> cons(z, nil)  ;  i -> z  ;  l1 -> nil
})

-------------------------------------------
Step 4, which took 0.020053 s (model generation: 0.018610,  model checking: 0.001443):

Model:
|_
{
append -> 
{{{
Q={q_gen_9040, q_gen_9042, q_gen_9043, q_gen_9045, q_gen_9047},
Q_f={q_gen_9040},
Delta=
{
<nil, nil>() -> q_gen_9042
<s, s>(q_gen_9043) -> q_gen_9043
<z, z>() -> q_gen_9043
<cons, cons>(q_gen_9043, q_gen_9042) -> q_gen_9045
<cons, nil, cons>(q_gen_9043, q_gen_9042) -> q_gen_9040
<nil, cons, cons>(q_gen_9043, q_gen_9045) -> q_gen_9040
<nil, nil, nil>() -> q_gen_9040
<nil, cons, cons>(q_gen_9043, q_gen_9042) -> q_gen_9047
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
(append([l1, cons(i, nil), _bma])) -> eq_natlist([l1, _bma]) -> 5
(append([t1, l2, _wla])) -> append([cons(h1, t1), l2, cons(h1, _wla)]) -> 7
}
Sat witness: Found: ((append([t1, l2, _wla])) -> append([cons(h1, t1), l2, cons(h1, _wla)]), {
_wla -> cons(z, nil)  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 5, which took 0.020549 s (model generation: 0.019688,  model checking: 0.000861):

Model:
|_
{
append -> 
{{{
Q={q_gen_9040, q_gen_9042, q_gen_9043, q_gen_9045, q_gen_9047},
Q_f={q_gen_9040},
Delta=
{
<nil, nil>() -> q_gen_9042
<s, s>(q_gen_9043) -> q_gen_9043
<z, z>() -> q_gen_9043
<cons, cons>(q_gen_9043, q_gen_9042) -> q_gen_9045
<cons, nil, cons>(q_gen_9043, q_gen_9042) -> q_gen_9040
<cons, nil, cons>(q_gen_9043, q_gen_9045) -> q_gen_9040
<nil, cons, cons>(q_gen_9043, q_gen_9045) -> q_gen_9040
<nil, nil, nil>() -> q_gen_9040
<nil, cons, cons>(q_gen_9043, q_gen_9042) -> q_gen_9047
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9
(append([l1, cons(i, nil), _bma])) -> eq_natlist([l1, _bma]) -> 6
(append([t1, l2, _wla])) -> append([cons(h1, t1), l2, cons(h1, _wla)]) -> 7
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(z, nil)
})

Total time: 0.129291
Reason for stopping: Disproved