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

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


Learning problem is:

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

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


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

Clause system for inference is:

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


Solving took 0.081905 seconds.
Disproved
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.010658 s (model generation: 0.009973,  model checking: 0.000685):

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

}

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

}
--
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), _dma])) -> eq_natlist([l1, _dma]) -> 1
(append([t1, l2, _yla])) -> append([cons(h1, t1), l2, cons(h1, _yla)]) -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 1, which took 0.012085 s (model generation: 0.009932,  model checking: 0.002153):

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

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

}
--
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), _dma])) -> eq_natlist([l1, _dma]) -> 1
(append([t1, l2, _yla])) -> append([cons(h1, t1), l2, cons(h1, _yla)]) -> 4
}
Sat witness: Found: ((append([t1, l2, _yla])) -> append([cons(h1, t1), l2, cons(h1, _yla)]), {
_yla -> nil  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 2, which took 0.011216 s (model generation: 0.010376,  model checking: 0.000840):

Model:
|_
{
append -> 
{{{
Q={q_gen_6850, q_gen_6852, q_gen_6853},
Q_f={q_gen_6850},
Delta=
{
<nil, nil>() -> q_gen_6852
<z, z>() -> q_gen_6853
<cons, nil, cons>(q_gen_6853, q_gen_6852) -> q_gen_6850
<nil, nil, nil>() -> q_gen_6850
}

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

}
--
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), _dma])) -> eq_natlist([l1, _dma]) -> 2
(append([t1, l2, _yla])) -> append([cons(h1, t1), l2, cons(h1, _yla)]) -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(s(z), cons(s(z), nil))
})

-------------------------------------------
Step 3, which took 0.011055 s (model generation: 0.010789,  model checking: 0.000266):

Model:
|_
{
append -> 
{{{
Q={q_gen_6850, q_gen_6852, q_gen_6853},
Q_f={q_gen_6850},
Delta=
{
<cons, cons>(q_gen_6853, q_gen_6852) -> q_gen_6852
<nil, nil>() -> q_gen_6852
<s, s>(q_gen_6853) -> q_gen_6853
<z, z>() -> q_gen_6853
<cons, nil, cons>(q_gen_6853, q_gen_6852) -> q_gen_6850
<nil, cons, cons>(q_gen_6853, q_gen_6852) -> q_gen_6850
<nil, nil, nil>() -> q_gen_6850
}

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

}
--
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), _dma])) -> eq_natlist([l1, _dma]) -> 5
(append([t1, l2, _yla])) -> append([cons(h1, t1), l2, cons(h1, _yla)]) -> 4
}
Sat witness: Found: ((append([l1, cons(i, nil), _dma])) -> eq_natlist([l1, _dma]), {
_dma -> cons(z, nil)  ;  i -> z  ;  l1 -> nil
})

-------------------------------------------
Step 4, which took 0.012958 s (model generation: 0.011314,  model checking: 0.001644):

Model:
|_
{
append -> 
{{{
Q={q_gen_6850, q_gen_6852, q_gen_6853, q_gen_6855, q_gen_6857},
Q_f={q_gen_6850},
Delta=
{
<nil, nil>() -> q_gen_6852
<s, s>(q_gen_6853) -> q_gen_6853
<z, z>() -> q_gen_6853
<cons, cons>(q_gen_6853, q_gen_6852) -> q_gen_6855
<cons, nil, cons>(q_gen_6853, q_gen_6852) -> q_gen_6850
<nil, cons, cons>(q_gen_6853, q_gen_6855) -> q_gen_6850
<nil, nil, nil>() -> q_gen_6850
<nil, cons, cons>(q_gen_6853, q_gen_6852) -> q_gen_6857
}

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

}
--
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), _dma])) -> eq_natlist([l1, _dma]) -> 5
(append([t1, l2, _yla])) -> append([cons(h1, t1), l2, cons(h1, _yla)]) -> 7
}
Sat witness: Found: ((append([t1, l2, _yla])) -> append([cons(h1, t1), l2, cons(h1, _yla)]), {
_yla -> cons(z, nil)  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 5, which took 0.012489 s (model generation: 0.011628,  model checking: 0.000861):

Model:
|_
{
append -> 
{{{
Q={q_gen_6850, q_gen_6852, q_gen_6853, q_gen_6855, q_gen_6857},
Q_f={q_gen_6850},
Delta=
{
<nil, nil>() -> q_gen_6852
<s, s>(q_gen_6853) -> q_gen_6853
<z, z>() -> q_gen_6853
<cons, cons>(q_gen_6853, q_gen_6852) -> q_gen_6855
<cons, nil, cons>(q_gen_6853, q_gen_6852) -> q_gen_6850
<cons, nil, cons>(q_gen_6853, q_gen_6855) -> q_gen_6850
<nil, cons, cons>(q_gen_6853, q_gen_6855) -> q_gen_6850
<nil, nil, nil>() -> q_gen_6850
<nil, cons, cons>(q_gen_6853, q_gen_6852) -> q_gen_6857
}

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

}
--
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), _dma])) -> eq_natlist([l1, _dma]) -> 6
(append([t1, l2, _yla])) -> append([cons(h1, t1), l2, cons(h1, _yla)]) -> 7
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(z, nil)
})

Total time: 0.081905
Reason for stopping: Disproved