Solving ../../benchmarks/true/append_equal.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: 30s
Convolution: complete


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}
}
definition:
{
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)])}
(append([_jca, _kca, _lca]) /\ append([_jca, _kca, _mca])) -> eq_eltlist([_lca, _mca])
)
}

properties:
{(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j])}


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0  ;  (append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 0  ;  (append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 0
}


Solving took 30.000035 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_0, q_gen_1, q_gen_10, q_gen_11, q_gen_12, q_gen_13, q_gen_14, q_gen_15, q_gen_16, q_gen_17, q_gen_18, q_gen_19, q_gen_2, q_gen_20, q_gen_21, q_gen_22, q_gen_23, q_gen_24, q_gen_25, q_gen_26, q_gen_27, q_gen_28, q_gen_29, q_gen_3, q_gen_30, q_gen_31, q_gen_32, q_gen_33, q_gen_34, q_gen_35, q_gen_36, q_gen_37, q_gen_38, q_gen_39, q_gen_4, q_gen_40, q_gen_41, q_gen_42, q_gen_43, q_gen_44, q_gen_45, q_gen_46, q_gen_47, q_gen_48, q_gen_49, q_gen_5, q_gen_50, q_gen_51, q_gen_52, q_gen_53, q_gen_54, q_gen_55, q_gen_56, q_gen_57, q_gen_58, q_gen_59, q_gen_6, q_gen_60, q_gen_61, q_gen_62, q_gen_63, q_gen_64, q_gen_65, q_gen_66, q_gen_67, q_gen_68, q_gen_69, q_gen_7, q_gen_70, q_gen_71, q_gen_72, q_gen_73, q_gen_74, q_gen_75, q_gen_76, q_gen_77, q_gen_78, q_gen_79, q_gen_8, q_gen_80, q_gen_81, q_gen_82, q_gen_83, q_gen_84, q_gen_9},
Q_f={},
Delta=
{
<nil>() -> q_gen_14
<a>() -> q_gen_15
<b>() -> q_gen_20
<cons>(q_gen_20, q_gen_14) -> q_gen_28
<cons>(q_gen_15, q_gen_14) -> q_gen_58
<cons, cons>(q_gen_9, q_gen_8, q_gen_7, q_gen_2) -> q_gen_12
<cons, b>(q_gen_15, q_gen_14) -> q_gen_13
<b, cons>(q_gen_15, q_gen_14) -> q_gen_16
<cons, cons>(q_gen_5, q_gen_4, q_gen_3, q_gen_2) -> q_gen_18
<cons, b>(q_gen_20, q_gen_14) -> q_gen_19
<nil, nil>() -> q_gen_2
<b, cons>(q_gen_20, q_gen_14) -> q_gen_21
<cons, a>(q_gen_20, q_gen_14) -> q_gen_23
<a, cons>(q_gen_20, q_gen_14) -> q_gen_24
<cons, cons>(q_gen_5, q_gen_21, q_gen_19, q_gen_18) -> q_gen_26
<cons, b>(q_gen_20, q_gen_28) -> q_gen_27
<b, cons>(q_gen_20, q_gen_28) -> q_gen_29
<nil, b>() -> q_gen_3
<b, nil>() -> q_gen_4
<nil, cons>(q_gen_15, q_gen_14) -> q_gen_42
<b, b>() -> q_gen_5
<cons, a>(q_gen_15, q_gen_14) -> q_gen_53
<a, cons>(q_gen_15, q_gen_14) -> q_gen_54
<cons, cons>(q_gen_5, q_gen_16, q_gen_3, q_gen_42) -> q_gen_56
<b, cons>(q_gen_20, q_gen_58) -> q_gen_57
<nil, a>() -> q_gen_7
<nil, cons>(q_gen_20, q_gen_14) -> q_gen_79
<a, nil>() -> q_gen_8
<a, a>() -> q_gen_9
<nil, nil, nil>() -> q_gen_0
<cons, nil, cons>(q_gen_5, q_gen_4, q_gen_3, q_gen_2) -> q_gen_1
<cons, nil, cons>(q_gen_9, q_gen_8, q_gen_7, q_gen_2) -> q_gen_10
<cons, nil, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_11
<nil, cons, cons>(q_gen_5, q_gen_21, q_gen_19, q_gen_18) -> q_gen_17
<cons, nil, cons>(q_gen_9, q_gen_24, q_gen_23, q_gen_18) -> q_gen_22
<nil, cons, cons>(q_gen_5, q_gen_29, q_gen_27, q_gen_26) -> q_gen_25
<nil, cons, cons>(q_gen_5, q_gen_4, q_gen_3, q_gen_2) -> q_gen_30
<cons, cons, cons>(q_gen_39, q_gen_38, q_gen_37, q_gen_36, q_gen_35, q_gen_34, q_gen_33, q_gen_32) -> q_gen_31
<nil, nil, cons>(q_gen_20, q_gen_14) -> q_gen_32
<nil, nil, b>() -> q_gen_33
<nil, b, cons>(q_gen_20, q_gen_14) -> q_gen_34
<nil, b, b>() -> q_gen_35
<b, nil, cons>(q_gen_20, q_gen_14) -> q_gen_36
<b, nil, b>() -> q_gen_37
<b, b, cons>(q_gen_20, q_gen_14) -> q_gen_38
<b, b, b>() -> q_gen_39
<nil, nil, cons>(q_gen_15, q_gen_14) -> q_gen_40
<cons, nil, cons>(q_gen_5, q_gen_16, q_gen_3, q_gen_42) -> q_gen_41
<cons, cons, cons>(q_gen_48, q_gen_47, q_gen_37, q_gen_46, q_gen_45, q_gen_44, q_gen_33, q_gen_40) -> q_gen_43
<nil, a, cons>(q_gen_15, q_gen_14) -> q_gen_44
<nil, a, b>() -> q_gen_45
<b, nil, cons>(q_gen_15, q_gen_14) -> q_gen_46
<b, a, cons>(q_gen_15, q_gen_14) -> q_gen_47
<b, a, b>() -> q_gen_48
<cons, cons, cons>(q_gen_48, q_gen_51, q_gen_37, q_gen_36, q_gen_45, q_gen_50, q_gen_33, q_gen_32) -> q_gen_49
<nil, a, cons>(q_gen_20, q_gen_14) -> q_gen_50
<b, a, cons>(q_gen_20, q_gen_14) -> q_gen_51
<nil, cons, cons>(q_gen_9, q_gen_54, q_gen_53, q_gen_12) -> q_gen_52
<cons, nil, cons>(q_gen_5, q_gen_57, q_gen_19, q_gen_56) -> q_gen_55
<cons, cons, cons>(q_gen_65, q_gen_64, q_gen_63, q_gen_62, q_gen_61, q_gen_34, q_gen_60, q_gen_32) -> q_gen_59
<nil, cons, cons>(q_gen_9, q_gen_8, q_gen_7, q_gen_2) -> q_gen_6
<nil, nil, a>() -> q_gen_60
<nil, b, a>() -> q_gen_61
<a, nil, cons>(q_gen_20, q_gen_14) -> q_gen_62
<a, nil, a>() -> q_gen_63
<a, b, cons>(q_gen_20, q_gen_14) -> q_gen_64
<a, b, a>() -> q_gen_65
<cons, cons, cons>(q_gen_70, q_gen_69, q_gen_63, q_gen_68, q_gen_67, q_gen_44, q_gen_60, q_gen_40) -> q_gen_66
<nil, a, a>() -> q_gen_67
<a, nil, cons>(q_gen_15, q_gen_14) -> q_gen_68
<a, a, cons>(q_gen_15, q_gen_14) -> q_gen_69
<a, a, a>() -> q_gen_70
<cons, cons, cons>(q_gen_48, q_gen_76, q_gen_37, q_gen_75, q_gen_74, q_gen_73, q_gen_72, q_gen_41) -> q_gen_71
<cons, nil, b>(q_gen_20, q_gen_14) -> q_gen_72
<cons, a, cons>(q_gen_5, q_gen_16, q_gen_3, q_gen_42) -> q_gen_73
<cons, a, b>(q_gen_20, q_gen_14) -> q_gen_74
<b, nil, cons>(q_gen_20, q_gen_58) -> q_gen_75
<b, a, cons>(q_gen_20, q_gen_58) -> q_gen_76
<cons, cons, cons>(q_gen_39, q_gen_84, q_gen_83, q_gen_82, q_gen_35, q_gen_81, q_gen_80, q_gen_78) -> q_gen_77
<nil, cons, cons>(q_gen_5, q_gen_21, q_gen_3, q_gen_79) -> q_gen_78
<nil, cons, b>(q_gen_20, q_gen_14) -> q_gen_80
<nil, b, cons>(q_gen_20, q_gen_28) -> q_gen_81
<b, cons, cons>(q_gen_5, q_gen_21, q_gen_3, q_gen_79) -> q_gen_82
<b, cons, b>(q_gen_20, q_gen_14) -> q_gen_83
<b, b, cons>(q_gen_20, q_gen_28) -> q_gen_84
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.007275 s (model generation: 0.004553,  model checking: 0.002722):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  (append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 1  ;  (append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 1
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 1, which took 0.006004 s (model generation: 0.005329,  model checking: 0.000675):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  (append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 1  ;  (append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 4
}
Sat witness: Yes: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 2, which took 0.013832 s (model generation: 0.008314,  model checking: 0.005518):

Model:
|_
{
append -> 
{{{
Q={q_gen_0, q_gen_2, q_gen_3, q_gen_4, q_gen_5},
Q_f={q_gen_0},
Delta=
{
<nil, nil>() -> q_gen_2
<nil, b>() -> q_gen_3
<b, nil>() -> q_gen_4
<b, b>() -> q_gen_5
<cons, nil, cons>(q_gen_5, q_gen_4, q_gen_3, q_gen_2) -> q_gen_0
<nil, nil, nil>() -> q_gen_0
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  (append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 2  ;  (append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 4
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(a, nil)
})

-------------------------------------------
Step 3, which took 0.017311 s (model generation: 0.008981,  model checking: 0.008330):

Model:
|_
{
append -> 
{{{
Q={q_gen_0, q_gen_2, q_gen_3, q_gen_4, q_gen_5},
Q_f={q_gen_0},
Delta=
{
<nil, nil>() -> q_gen_2
<nil, a>() -> q_gen_3
<nil, b>() -> q_gen_3
<a, nil>() -> q_gen_4
<b, nil>() -> q_gen_4
<a, a>() -> q_gen_5
<b, b>() -> q_gen_5
<cons, nil, cons>(q_gen_5, q_gen_4, q_gen_3, q_gen_2) -> q_gen_0
<nil, cons, cons>(q_gen_5, q_gen_4, q_gen_3, q_gen_2) -> q_gen_0
<nil, nil, nil>() -> q_gen_0
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  (append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 3  ;  (append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 7
}
Sat witness: Yes: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 4, which took 0.028693 s (model generation: 0.010121,  model checking: 0.018572):

Model:
|_
{
append -> 
{{{
Q={q_gen_0, q_gen_12, q_gen_13, q_gen_14, q_gen_15, q_gen_16, q_gen_5},
Q_f={q_gen_0},
Delta=
{
<nil>() -> q_gen_14
<a>() -> q_gen_15
<cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_12
<nil, nil>() -> q_gen_12
<cons, b>(q_gen_15, q_gen_14) -> q_gen_13
<nil, a>() -> q_gen_13
<nil, b>() -> q_gen_13
<a, nil>() -> q_gen_16
<b, cons>(q_gen_15, q_gen_14) -> q_gen_16
<b, nil>() -> q_gen_16
<a, a>() -> q_gen_5
<b, b>() -> q_gen_5
<cons, nil, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, nil, nil>() -> q_gen_0
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  (append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 4  ;  (append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 7
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 5, which took 0.008877 s (model generation: 0.004519,  model checking: 0.004358):

Model:
|_
{
append -> 
{{{
Q={q_gen_0, q_gen_12, q_gen_13, q_gen_14, q_gen_15, q_gen_16, q_gen_5},
Q_f={q_gen_0},
Delta=
{
<nil>() -> q_gen_14
<a>() -> q_gen_15
<b>() -> q_gen_15
<cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_12
<nil, nil>() -> q_gen_12
<cons, b>(q_gen_15, q_gen_14) -> q_gen_13
<nil, a>() -> q_gen_13
<nil, b>() -> q_gen_13
<a, nil>() -> q_gen_16
<b, cons>(q_gen_15, q_gen_14) -> q_gen_16
<b, nil>() -> q_gen_16
<a, a>() -> q_gen_5
<b, b>() -> q_gen_5
<cons, nil, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, nil, nil>() -> q_gen_0
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  (append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 5  ;  (append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 10
}
Sat witness: Yes: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(b, nil)  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 6, which took 0.011646 s (model generation: 0.004876,  model checking: 0.006770):

Model:
|_
{
append -> 
{{{
Q={q_gen_0, q_gen_12, q_gen_13, q_gen_14, q_gen_15, q_gen_16, q_gen_5},
Q_f={q_gen_0},
Delta=
{
<nil>() -> q_gen_14
<a>() -> q_gen_15
<b>() -> q_gen_15
<cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_12
<nil, nil>() -> q_gen_12
<cons, a>(q_gen_15, q_gen_14) -> q_gen_13
<cons, b>(q_gen_15, q_gen_14) -> q_gen_13
<nil, a>() -> q_gen_13
<nil, b>() -> q_gen_13
<a, cons>(q_gen_15, q_gen_14) -> q_gen_16
<a, nil>() -> q_gen_16
<b, cons>(q_gen_15, q_gen_14) -> q_gen_16
<b, nil>() -> q_gen_16
<a, a>() -> q_gen_5
<b, b>() -> q_gen_5
<cons, nil, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, nil, nil>() -> q_gen_0
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  (append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 6  ;  (append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 10
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 7, which took 0.009095 s (model generation: 0.005513,  model checking: 0.003582):

Model:
|_
{
append -> 
{{{
Q={q_gen_0, q_gen_12, q_gen_13, q_gen_14, q_gen_15, q_gen_16, q_gen_5},
Q_f={q_gen_0},
Delta=
{
<cons>(q_gen_15, q_gen_14) -> q_gen_14
<nil>() -> q_gen_14
<a>() -> q_gen_15
<b>() -> q_gen_15
<cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_12
<nil, nil>() -> q_gen_12
<cons, a>(q_gen_15, q_gen_14) -> q_gen_13
<cons, b>(q_gen_15, q_gen_14) -> q_gen_13
<nil, a>() -> q_gen_13
<nil, b>() -> q_gen_13
<a, cons>(q_gen_15, q_gen_14) -> q_gen_16
<a, nil>() -> q_gen_16
<b, cons>(q_gen_15, q_gen_14) -> q_gen_16
<b, nil>() -> q_gen_16
<a, a>() -> q_gen_5
<b, b>() -> q_gen_5
<cons, nil, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, nil, nil>() -> q_gen_0
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  (append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 7  ;  (append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 13
}
Sat witness: Yes: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 8, which took 0.034428 s (model generation: 0.006388,  model checking: 0.028040):

Model:
|_
{
append -> 
{{{
Q={q_gen_0, q_gen_12, q_gen_13, q_gen_14, q_gen_15, q_gen_16, q_gen_33, q_gen_34, q_gen_35, q_gen_36, q_gen_37, q_gen_38, q_gen_39, q_gen_5},
Q_f={q_gen_0},
Delta=
{
<cons>(q_gen_15, q_gen_14) -> q_gen_14
<nil>() -> q_gen_14
<a>() -> q_gen_15
<b>() -> q_gen_15
<cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_12
<nil, nil>() -> q_gen_12
<cons, a>(q_gen_15, q_gen_14) -> q_gen_13
<cons, b>(q_gen_15, q_gen_14) -> q_gen_13
<nil, a>() -> q_gen_13
<nil, b>() -> q_gen_13
<a, cons>(q_gen_15, q_gen_14) -> q_gen_16
<a, nil>() -> q_gen_16
<b, cons>(q_gen_15, q_gen_14) -> q_gen_16
<b, nil>() -> q_gen_16
<a, a>() -> q_gen_5
<b, b>() -> q_gen_5
<cons, cons, cons>(q_gen_39, q_gen_38, q_gen_37, q_gen_36, q_gen_35, q_gen_34, q_gen_33, q_gen_0) -> q_gen_0
<cons, nil, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, nil, cons>(q_gen_15, q_gen_14) -> q_gen_0
<nil, nil, nil>() -> q_gen_0
<nil, nil, b>() -> q_gen_33
<nil, b, cons>(q_gen_15, q_gen_14) -> q_gen_34
<nil, b, b>() -> q_gen_35
<b, nil, cons>(q_gen_15, q_gen_14) -> q_gen_36
<b, nil, b>() -> q_gen_37
<b, b, cons>(q_gen_15, q_gen_14) -> q_gen_38
<b, b, b>() -> q_gen_39
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13  ;  (append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 8  ;  (append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 16
}
Sat witness: Yes: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 9, which took 0.071083 s (model generation: 0.007489,  model checking: 0.063594):

Model:
|_
{
append -> 
{{{
Q={q_gen_0, q_gen_12, q_gen_13, q_gen_14, q_gen_15, q_gen_16, q_gen_33, q_gen_34, q_gen_35, q_gen_36, q_gen_37, q_gen_38, q_gen_39, q_gen_5},
Q_f={q_gen_0},
Delta=
{
<cons>(q_gen_15, q_gen_14) -> q_gen_14
<nil>() -> q_gen_14
<a>() -> q_gen_15
<b>() -> q_gen_15
<cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_12
<nil, cons>(q_gen_15, q_gen_14) -> q_gen_12
<nil, nil>() -> q_gen_12
<cons, a>(q_gen_15, q_gen_14) -> q_gen_13
<cons, b>(q_gen_15, q_gen_14) -> q_gen_13
<nil, a>() -> q_gen_13
<nil, b>() -> q_gen_13
<a, cons>(q_gen_15, q_gen_14) -> q_gen_16
<a, nil>() -> q_gen_16
<b, cons>(q_gen_15, q_gen_14) -> q_gen_16
<b, nil>() -> q_gen_16
<a, a>() -> q_gen_5
<b, b>() -> q_gen_5
<cons, cons, cons>(q_gen_39, q_gen_38, q_gen_37, q_gen_36, q_gen_35, q_gen_34, q_gen_33, q_gen_0) -> q_gen_0
<cons, nil, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, nil, cons>(q_gen_15, q_gen_14) -> q_gen_0
<nil, nil, nil>() -> q_gen_0
<nil, nil, b>() -> q_gen_33
<nil, b, cons>(q_gen_15, q_gen_14) -> q_gen_34
<nil, b, b>() -> q_gen_35
<b, nil, cons>(q_gen_15, q_gen_14) -> q_gen_36
<b, nil, b>() -> q_gen_37
<b, b, cons>(q_gen_15, q_gen_14) -> q_gen_38
<b, b, b>() -> q_gen_39
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14  ;  (append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 9  ;  (append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 19
}
Sat witness: Yes: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 10, which took 0.008598 s (model generation: 0.008451,  model checking: 0.000147):

Model:
|_
{
append -> 
{{{
Q={q_gen_0, q_gen_12, q_gen_13, q_gen_14, q_gen_15, q_gen_16, q_gen_33, q_gen_34, q_gen_35, q_gen_36, q_gen_37, q_gen_38, q_gen_39, q_gen_5},
Q_f={q_gen_0},
Delta=
{
<cons>(q_gen_15, q_gen_14) -> q_gen_14
<nil>() -> q_gen_14
<a>() -> q_gen_15
<b>() -> q_gen_15
<cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_12
<nil, cons>(q_gen_15, q_gen_14) -> q_gen_12
<nil, nil>() -> q_gen_12
<cons, a>(q_gen_15, q_gen_14) -> q_gen_13
<cons, b>(q_gen_15, q_gen_14) -> q_gen_13
<nil, a>() -> q_gen_13
<nil, b>() -> q_gen_13
<a, cons>(q_gen_15, q_gen_14) -> q_gen_16
<a, nil>() -> q_gen_16
<b, cons>(q_gen_15, q_gen_14) -> q_gen_16
<b, nil>() -> q_gen_16
<a, a>() -> q_gen_5
<b, b>() -> q_gen_5
<cons, cons, cons>(q_gen_39, q_gen_38, q_gen_37, q_gen_36, q_gen_35, q_gen_34, q_gen_33, q_gen_0) -> q_gen_0
<cons, nil, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, nil, cons>(q_gen_15, q_gen_14) -> q_gen_0
<nil, nil, nil>() -> q_gen_0
<nil, nil, b>() -> q_gen_33
<nil, a, cons>(q_gen_15, q_gen_14) -> q_gen_34
<nil, b, cons>(q_gen_15, q_gen_14) -> q_gen_34
<nil, a, b>() -> q_gen_35
<nil, b, b>() -> q_gen_35
<b, nil, cons>(q_gen_15, q_gen_14) -> q_gen_36
<b, nil, b>() -> q_gen_37
<b, a, cons>(q_gen_15, q_gen_14) -> q_gen_38
<b, b, cons>(q_gen_15, q_gen_14) -> q_gen_38
<b, a, b>() -> q_gen_39
<b, b, b>() -> q_gen_39
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14  ;  (append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 12  ;  (append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 19
}
Sat witness: Yes: ((append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]), {
_oca -> cons(b, cons(b, nil))  ;  i -> b  ;  j -> a  ;  l1 -> cons(b, nil)
})

-------------------------------------------
Step 11, which took 0.014697 s (model generation: 0.009741,  model checking: 0.004956):

Model:
|_
{
append -> 
{{{
Q={q_gen_0, q_gen_12, q_gen_13, q_gen_14, q_gen_15, q_gen_16, q_gen_30, q_gen_33, q_gen_34, q_gen_35, q_gen_36, q_gen_37, q_gen_38, q_gen_39, q_gen_4, q_gen_45, q_gen_5},
Q_f={q_gen_0},
Delta=
{
<cons>(q_gen_15, q_gen_14) -> q_gen_14
<nil>() -> q_gen_14
<a>() -> q_gen_15
<b>() -> q_gen_15
<cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_12
<cons, cons>(q_gen_5, q_gen_4, q_gen_13, q_gen_12) -> q_gen_12
<nil, cons>(q_gen_15, q_gen_14) -> q_gen_12
<nil, nil>() -> q_gen_12
<cons, a>(q_gen_15, q_gen_14) -> q_gen_13
<cons, b>(q_gen_15, q_gen_14) -> q_gen_13
<nil, a>() -> q_gen_13
<nil, b>() -> q_gen_13
<a, cons>(q_gen_15, q_gen_14) -> q_gen_16
<a, nil>() -> q_gen_16
<b, cons>(q_gen_15, q_gen_14) -> q_gen_16
<b, nil>() -> q_gen_4
<a, a>() -> q_gen_5
<b, b>() -> q_gen_5
<cons, cons, cons>(q_gen_39, q_gen_38, q_gen_37, q_gen_36, q_gen_45, q_gen_34, q_gen_33, q_gen_30) -> q_gen_0
<cons, nil, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<cons, nil, cons>(q_gen_5, q_gen_4, q_gen_13, q_gen_12) -> q_gen_0
<nil, cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, nil, nil>() -> q_gen_0
<cons, cons, cons>(q_gen_39, q_gen_38, q_gen_37, q_gen_36, q_gen_35, q_gen_34, q_gen_33, q_gen_30) -> q_gen_30
<nil, cons, cons>(q_gen_5, q_gen_4, q_gen_13, q_gen_12) -> q_gen_30
<nil, nil, cons>(q_gen_15, q_gen_14) -> q_gen_30
<nil, nil, b>() -> q_gen_33
<nil, a, cons>(q_gen_15, q_gen_14) -> q_gen_34
<nil, b, cons>(q_gen_15, q_gen_14) -> q_gen_34
<nil, b, b>() -> q_gen_35
<b, nil, cons>(q_gen_15, q_gen_14) -> q_gen_36
<b, nil, b>() -> q_gen_37
<b, a, cons>(q_gen_15, q_gen_14) -> q_gen_38
<b, b, cons>(q_gen_15, q_gen_14) -> q_gen_38
<b, a, b>() -> q_gen_39
<b, b, b>() -> q_gen_39
<nil, a, b>() -> q_gen_45
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 17  ;  (append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 13  ;  (append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 19
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, nil)
})

-------------------------------------------
Step 12, which took 0.022100 s (model generation: 0.008725,  model checking: 0.013375):

Model:
|_
{
append -> 
{{{
Q={q_gen_0, q_gen_12, q_gen_13, q_gen_14, q_gen_15, q_gen_16, q_gen_20, q_gen_32, q_gen_33, q_gen_34, q_gen_35, q_gen_36, q_gen_37, q_gen_38, q_gen_39, q_gen_45, q_gen_5},
Q_f={q_gen_0},
Delta=
{
<cons>(q_gen_20, q_gen_14) -> q_gen_14
<nil>() -> q_gen_14
<a>() -> q_gen_15
<b>() -> q_gen_20
<cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_12
<nil, cons>(q_gen_15, q_gen_14) -> q_gen_12
<nil, nil>() -> q_gen_12
<cons, a>(q_gen_20, q_gen_14) -> q_gen_13
<cons, b>(q_gen_15, q_gen_14) -> q_gen_13
<cons, b>(q_gen_20, q_gen_14) -> q_gen_13
<nil, a>() -> q_gen_13
<nil, b>() -> q_gen_13
<a, cons>(q_gen_20, q_gen_14) -> q_gen_16
<a, nil>() -> q_gen_16
<b, cons>(q_gen_15, q_gen_14) -> q_gen_16
<b, cons>(q_gen_20, q_gen_14) -> q_gen_16
<b, nil>() -> q_gen_16
<a, a>() -> q_gen_5
<b, b>() -> q_gen_5
<cons, cons, cons>(q_gen_39, q_gen_38, q_gen_37, q_gen_36, q_gen_35, q_gen_34, q_gen_33, q_gen_32) -> q_gen_0
<cons, cons, cons>(q_gen_39, q_gen_38, q_gen_37, q_gen_36, q_gen_45, q_gen_34, q_gen_33, q_gen_0) -> q_gen_0
<cons, nil, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, nil, cons>(q_gen_15, q_gen_14) -> q_gen_0
<nil, nil, nil>() -> q_gen_0
<cons, cons, cons>(q_gen_39, q_gen_38, q_gen_37, q_gen_36, q_gen_45, q_gen_34, q_gen_33, q_gen_32) -> q_gen_32
<nil, nil, cons>(q_gen_20, q_gen_14) -> q_gen_32
<nil, nil, b>() -> q_gen_33
<nil, a, cons>(q_gen_15, q_gen_14) -> q_gen_34
<nil, a, cons>(q_gen_20, q_gen_14) -> q_gen_34
<nil, b, cons>(q_gen_20, q_gen_14) -> q_gen_34
<nil, b, b>() -> q_gen_35
<b, nil, cons>(q_gen_15, q_gen_14) -> q_gen_36
<b, nil, cons>(q_gen_20, q_gen_14) -> q_gen_36
<b, nil, b>() -> q_gen_37
<b, a, cons>(q_gen_15, q_gen_14) -> q_gen_38
<b, a, cons>(q_gen_20, q_gen_14) -> q_gen_38
<b, b, cons>(q_gen_20, q_gen_14) -> q_gen_38
<b, a, b>() -> q_gen_39
<b, b, b>() -> q_gen_39
<nil, a, b>() -> q_gen_45
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 20  ;  (append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 14  ;  (append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 19
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 13, which took 0.229301 s (model generation: 0.009345,  model checking: 0.219956):

Model:
|_
{
append -> 
{{{
Q={q_gen_0, q_gen_12, q_gen_13, q_gen_14, q_gen_15, q_gen_16, q_gen_20, q_gen_32, q_gen_33, q_gen_34, q_gen_35, q_gen_36, q_gen_37, q_gen_38, q_gen_39, q_gen_5, q_gen_51},
Q_f={q_gen_0},
Delta=
{
<cons>(q_gen_20, q_gen_14) -> q_gen_14
<nil>() -> q_gen_14
<a>() -> q_gen_15
<b>() -> q_gen_20
<cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_12
<nil, cons>(q_gen_15, q_gen_14) -> q_gen_12
<nil, nil>() -> q_gen_12
<cons, a>(q_gen_15, q_gen_14) -> q_gen_13
<cons, a>(q_gen_20, q_gen_14) -> q_gen_13
<cons, b>(q_gen_15, q_gen_14) -> q_gen_13
<cons, b>(q_gen_20, q_gen_14) -> q_gen_13
<nil, a>() -> q_gen_13
<nil, b>() -> q_gen_13
<a, cons>(q_gen_15, q_gen_14) -> q_gen_16
<a, cons>(q_gen_20, q_gen_14) -> q_gen_16
<a, nil>() -> q_gen_16
<b, cons>(q_gen_15, q_gen_14) -> q_gen_16
<b, cons>(q_gen_20, q_gen_14) -> q_gen_16
<b, nil>() -> q_gen_16
<a, a>() -> q_gen_5
<b, b>() -> q_gen_5
<cons, cons, cons>(q_gen_39, q_gen_38, q_gen_37, q_gen_36, q_gen_35, q_gen_34, q_gen_33, q_gen_32) -> q_gen_0
<cons, nil, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, nil, nil>() -> q_gen_0
<cons, cons, cons>(q_gen_39, q_gen_51, q_gen_37, q_gen_36, q_gen_35, q_gen_34, q_gen_33, q_gen_32) -> q_gen_32
<nil, nil, cons>(q_gen_15, q_gen_14) -> q_gen_32
<nil, nil, cons>(q_gen_20, q_gen_14) -> q_gen_32
<nil, nil, b>() -> q_gen_33
<nil, a, cons>(q_gen_15, q_gen_14) -> q_gen_34
<nil, a, cons>(q_gen_20, q_gen_14) -> q_gen_34
<nil, b, cons>(q_gen_20, q_gen_14) -> q_gen_34
<nil, a, b>() -> q_gen_35
<nil, b, b>() -> q_gen_35
<b, nil, cons>(q_gen_15, q_gen_14) -> q_gen_36
<b, nil, cons>(q_gen_20, q_gen_14) -> q_gen_36
<b, nil, b>() -> q_gen_37
<b, a, cons>(q_gen_15, q_gen_14) -> q_gen_38
<b, b, cons>(q_gen_20, q_gen_14) -> q_gen_38
<b, a, b>() -> q_gen_39
<b, b, b>() -> q_gen_39
<b, a, cons>(q_gen_20, q_gen_14) -> q_gen_51
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 20  ;  (append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 15  ;  (append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 22
}
Sat witness: Yes: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(b, cons(a, nil))  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 14, which took 0.901200 s (model generation: 0.011451,  model checking: 0.889749):

Model:
|_
{
append -> 
{{{
Q={q_gen_0, q_gen_12, q_gen_13, q_gen_14, q_gen_15, q_gen_16, q_gen_20, q_gen_32, q_gen_33, q_gen_34, q_gen_35, q_gen_36, q_gen_37, q_gen_38, q_gen_39, q_gen_5, q_gen_51},
Q_f={q_gen_0},
Delta=
{
<cons>(q_gen_15, q_gen_14) -> q_gen_14
<cons>(q_gen_20, q_gen_14) -> q_gen_14
<nil>() -> q_gen_14
<a>() -> q_gen_15
<b>() -> q_gen_20
<cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_12
<nil, cons>(q_gen_15, q_gen_14) -> q_gen_12
<nil, nil>() -> q_gen_12
<cons, a>(q_gen_15, q_gen_14) -> q_gen_13
<cons, a>(q_gen_20, q_gen_14) -> q_gen_13
<cons, b>(q_gen_15, q_gen_14) -> q_gen_13
<cons, b>(q_gen_20, q_gen_14) -> q_gen_13
<nil, a>() -> q_gen_13
<nil, b>() -> q_gen_13
<a, cons>(q_gen_15, q_gen_14) -> q_gen_16
<a, cons>(q_gen_20, q_gen_14) -> q_gen_16
<a, nil>() -> q_gen_16
<b, cons>(q_gen_15, q_gen_14) -> q_gen_16
<b, cons>(q_gen_20, q_gen_14) -> q_gen_16
<b, nil>() -> q_gen_16
<a, a>() -> q_gen_5
<b, b>() -> q_gen_5
<cons, cons, cons>(q_gen_39, q_gen_38, q_gen_37, q_gen_36, q_gen_35, q_gen_34, q_gen_33, q_gen_32) -> q_gen_0
<cons, nil, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, nil, nil>() -> q_gen_0
<cons, cons, cons>(q_gen_39, q_gen_51, q_gen_37, q_gen_36, q_gen_35, q_gen_34, q_gen_33, q_gen_32) -> q_gen_32
<nil, nil, cons>(q_gen_15, q_gen_14) -> q_gen_32
<nil, nil, cons>(q_gen_20, q_gen_14) -> q_gen_32
<nil, nil, b>() -> q_gen_33
<nil, a, cons>(q_gen_15, q_gen_14) -> q_gen_34
<nil, a, cons>(q_gen_20, q_gen_14) -> q_gen_34
<nil, b, cons>(q_gen_20, q_gen_14) -> q_gen_34
<nil, a, b>() -> q_gen_35
<nil, b, b>() -> q_gen_35
<b, nil, cons>(q_gen_15, q_gen_14) -> q_gen_36
<b, nil, cons>(q_gen_20, q_gen_14) -> q_gen_36
<b, nil, b>() -> q_gen_37
<b, a, cons>(q_gen_15, q_gen_14) -> q_gen_38
<b, b, cons>(q_gen_20, q_gen_14) -> q_gen_38
<b, a, b>() -> q_gen_39
<b, b, b>() -> q_gen_39
<b, a, cons>(q_gen_20, q_gen_14) -> q_gen_51
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 21  ;  (append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 16  ;  (append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 25
}
Sat witness: Yes: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 15, which took 0.447541 s (model generation: 0.012749,  model checking: 0.434792):

Model:
|_
{
append -> 
{{{
Q={q_gen_0, q_gen_12, q_gen_13, q_gen_14, q_gen_15, q_gen_16, q_gen_20, q_gen_32, q_gen_33, q_gen_34, q_gen_35, q_gen_36, q_gen_37, q_gen_38, q_gen_39, q_gen_5, q_gen_50},
Q_f={q_gen_0},
Delta=
{
<cons>(q_gen_15, q_gen_14) -> q_gen_14
<cons>(q_gen_20, q_gen_14) -> q_gen_14
<nil>() -> q_gen_14
<a>() -> q_gen_15
<b>() -> q_gen_20
<cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_12
<nil, cons>(q_gen_15, q_gen_14) -> q_gen_12
<nil, nil>() -> q_gen_12
<cons, a>(q_gen_15, q_gen_14) -> q_gen_13
<cons, a>(q_gen_20, q_gen_14) -> q_gen_13
<cons, b>(q_gen_15, q_gen_14) -> q_gen_13
<cons, b>(q_gen_20, q_gen_14) -> q_gen_13
<nil, a>() -> q_gen_13
<nil, b>() -> q_gen_13
<a, cons>(q_gen_15, q_gen_14) -> q_gen_16
<a, cons>(q_gen_20, q_gen_14) -> q_gen_16
<a, nil>() -> q_gen_16
<b, cons>(q_gen_15, q_gen_14) -> q_gen_16
<b, cons>(q_gen_20, q_gen_14) -> q_gen_16
<b, nil>() -> q_gen_16
<a, a>() -> q_gen_5
<b, b>() -> q_gen_5
<cons, cons, cons>(q_gen_39, q_gen_38, q_gen_37, q_gen_36, q_gen_35, q_gen_34, q_gen_33, q_gen_32) -> q_gen_0
<cons, nil, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, nil, nil>() -> q_gen_0
<cons, cons, cons>(q_gen_39, q_gen_38, q_gen_37, q_gen_36, q_gen_35, q_gen_50, q_gen_33, q_gen_32) -> q_gen_32
<nil, nil, cons>(q_gen_15, q_gen_14) -> q_gen_32
<nil, nil, cons>(q_gen_20, q_gen_14) -> q_gen_32
<nil, nil, a>() -> q_gen_33
<nil, nil, b>() -> q_gen_33
<nil, a, cons>(q_gen_15, q_gen_14) -> q_gen_34
<nil, b, cons>(q_gen_20, q_gen_14) -> q_gen_34
<nil, a, b>() -> q_gen_35
<nil, b, a>() -> q_gen_35
<nil, b, b>() -> q_gen_35
<a, nil, cons>(q_gen_20, q_gen_14) -> q_gen_36
<b, nil, cons>(q_gen_15, q_gen_14) -> q_gen_36
<b, nil, cons>(q_gen_20, q_gen_14) -> q_gen_36
<a, nil, a>() -> q_gen_37
<b, nil, b>() -> q_gen_37
<a, b, cons>(q_gen_20, q_gen_14) -> q_gen_38
<b, a, cons>(q_gen_15, q_gen_14) -> q_gen_38
<b, a, cons>(q_gen_20, q_gen_14) -> q_gen_38
<b, b, cons>(q_gen_20, q_gen_14) -> q_gen_38
<a, b, a>() -> q_gen_39
<b, a, b>() -> q_gen_39
<b, b, b>() -> q_gen_39
<nil, a, cons>(q_gen_20, q_gen_14) -> q_gen_50
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22  ;  (append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 17  ;  (append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 28
}
Sat witness: Yes: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 16, which took 3.774502 s (model generation: 0.013788,  model checking: 3.760714):

Model:
|_
{
append -> 
{{{
Q={q_gen_0, q_gen_12, q_gen_13, q_gen_14, q_gen_15, q_gen_16, q_gen_20, q_gen_32, q_gen_33, q_gen_34, q_gen_35, q_gen_36, q_gen_37, q_gen_38, q_gen_39, q_gen_44, q_gen_5},
Q_f={q_gen_0},
Delta=
{
<cons>(q_gen_15, q_gen_14) -> q_gen_14
<cons>(q_gen_20, q_gen_14) -> q_gen_14
<nil>() -> q_gen_14
<a>() -> q_gen_15
<b>() -> q_gen_20
<cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_12
<nil, cons>(q_gen_15, q_gen_14) -> q_gen_12
<nil, nil>() -> q_gen_12
<cons, a>(q_gen_15, q_gen_14) -> q_gen_13
<cons, a>(q_gen_20, q_gen_14) -> q_gen_13
<cons, b>(q_gen_15, q_gen_14) -> q_gen_13
<cons, b>(q_gen_20, q_gen_14) -> q_gen_13
<nil, a>() -> q_gen_13
<nil, b>() -> q_gen_13
<a, cons>(q_gen_15, q_gen_14) -> q_gen_16
<a, cons>(q_gen_20, q_gen_14) -> q_gen_16
<a, nil>() -> q_gen_16
<b, cons>(q_gen_15, q_gen_14) -> q_gen_16
<b, cons>(q_gen_20, q_gen_14) -> q_gen_16
<b, nil>() -> q_gen_16
<a, a>() -> q_gen_5
<b, b>() -> q_gen_5
<cons, cons, cons>(q_gen_39, q_gen_38, q_gen_37, q_gen_36, q_gen_35, q_gen_34, q_gen_33, q_gen_32) -> q_gen_0
<cons, cons, cons>(q_gen_39, q_gen_38, q_gen_37, q_gen_36, q_gen_35, q_gen_44, q_gen_33, q_gen_0) -> q_gen_0
<cons, nil, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, nil, cons>(q_gen_15, q_gen_14) -> q_gen_0
<nil, nil, nil>() -> q_gen_0
<cons, cons, cons>(q_gen_39, q_gen_38, q_gen_37, q_gen_36, q_gen_35, q_gen_44, q_gen_33, q_gen_32) -> q_gen_32
<nil, nil, cons>(q_gen_20, q_gen_14) -> q_gen_32
<nil, nil, a>() -> q_gen_33
<nil, nil, b>() -> q_gen_33
<nil, b, cons>(q_gen_20, q_gen_14) -> q_gen_34
<nil, a, a>() -> q_gen_35
<nil, a, b>() -> q_gen_35
<nil, b, a>() -> q_gen_35
<nil, b, b>() -> q_gen_35
<a, nil, cons>(q_gen_15, q_gen_14) -> q_gen_36
<a, nil, cons>(q_gen_20, q_gen_14) -> q_gen_36
<b, nil, cons>(q_gen_15, q_gen_14) -> q_gen_36
<b, nil, cons>(q_gen_20, q_gen_14) -> q_gen_36
<a, nil, a>() -> q_gen_37
<b, nil, b>() -> q_gen_37
<a, a, cons>(q_gen_15, q_gen_14) -> q_gen_38
<a, b, cons>(q_gen_20, q_gen_14) -> q_gen_38
<b, a, cons>(q_gen_15, q_gen_14) -> q_gen_38
<b, a, cons>(q_gen_20, q_gen_14) -> q_gen_38
<b, b, cons>(q_gen_20, q_gen_14) -> q_gen_38
<a, a, a>() -> q_gen_39
<a, b, a>() -> q_gen_39
<b, a, b>() -> q_gen_39
<b, b, b>() -> q_gen_39
<nil, a, cons>(q_gen_15, q_gen_14) -> q_gen_44
<nil, a, cons>(q_gen_20, q_gen_14) -> q_gen_44
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 23  ;  (append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 18  ;  (append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 31
}
Sat witness: Yes: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(b, cons(a, nil))  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 17, which took 3.318502 s (model generation: 0.017755,  model checking: 3.300747):

Model:
|_
{
append -> 
{{{
Q={q_gen_0, q_gen_12, q_gen_13, q_gen_14, q_gen_15, q_gen_16, q_gen_20, q_gen_32, q_gen_33, q_gen_34, q_gen_35, q_gen_36, q_gen_37, q_gen_38, q_gen_39, q_gen_47, q_gen_5},
Q_f={q_gen_0},
Delta=
{
<cons>(q_gen_15, q_gen_14) -> q_gen_14
<cons>(q_gen_20, q_gen_14) -> q_gen_14
<nil>() -> q_gen_14
<a>() -> q_gen_15
<b>() -> q_gen_20
<cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_12
<nil, cons>(q_gen_15, q_gen_14) -> q_gen_12
<nil, nil>() -> q_gen_12
<cons, a>(q_gen_15, q_gen_14) -> q_gen_13
<cons, a>(q_gen_20, q_gen_14) -> q_gen_13
<cons, b>(q_gen_15, q_gen_14) -> q_gen_13
<cons, b>(q_gen_20, q_gen_14) -> q_gen_13
<nil, a>() -> q_gen_13
<nil, b>() -> q_gen_13
<a, cons>(q_gen_15, q_gen_14) -> q_gen_16
<a, cons>(q_gen_20, q_gen_14) -> q_gen_16
<a, nil>() -> q_gen_16
<b, cons>(q_gen_15, q_gen_14) -> q_gen_16
<b, cons>(q_gen_20, q_gen_14) -> q_gen_16
<b, nil>() -> q_gen_16
<a, a>() -> q_gen_5
<b, b>() -> q_gen_5
<cons, cons, cons>(q_gen_39, q_gen_38, q_gen_37, q_gen_36, q_gen_35, q_gen_34, q_gen_33, q_gen_32) -> q_gen_0
<cons, cons, cons>(q_gen_39, q_gen_47, q_gen_37, q_gen_36, q_gen_35, q_gen_34, q_gen_33, q_gen_0) -> q_gen_0
<cons, nil, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, cons, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_0
<nil, nil, cons>(q_gen_15, q_gen_14) -> q_gen_0
<nil, nil, nil>() -> q_gen_0
<cons, cons, cons>(q_gen_39, q_gen_47, q_gen_37, q_gen_36, q_gen_35, q_gen_34, q_gen_33, q_gen_32) -> q_gen_32
<nil, nil, cons>(q_gen_20, q_gen_14) -> q_gen_32
<cons, nil, b>(q_gen_20, q_gen_14) -> q_gen_33
<nil, nil, a>() -> q_gen_33
<nil, nil, b>() -> q_gen_33
<cons, a, cons>(q_gen_5, q_gen_16, q_gen_13, q_gen_12) -> q_gen_34
<nil, a, cons>(q_gen_15, q_gen_14) -> q_gen_34
<nil, a, cons>(q_gen_20, q_gen_14) -> q_gen_34
<nil, b, cons>(q_gen_20, q_gen_14) -> q_gen_34
<cons, a, b>(q_gen_20, q_gen_14) -> q_gen_35
<nil, a, a>() -> q_gen_35
<nil, a, b>() -> q_gen_35
<nil, b, a>() -> q_gen_35
<nil, b, b>() -> q_gen_35
<a, nil, cons>(q_gen_15, q_gen_14) -> q_gen_36
<a, nil, cons>(q_gen_20, q_gen_14) -> q_gen_36
<b, nil, cons>(q_gen_15, q_gen_14) -> q_gen_36
<b, nil, cons>(q_gen_20, q_gen_14) -> q_gen_36
<a, nil, a>() -> q_gen_37
<b, nil, b>() -> q_gen_37
<a, b, cons>(q_gen_20, q_gen_14) -> q_gen_38
<b, b, cons>(q_gen_20, q_gen_14) -> q_gen_38
<a, a, a>() -> q_gen_39
<a, b, a>() -> q_gen_39
<b, a, b>() -> q_gen_39
<b, b, b>() -> q_gen_39
<a, a, cons>(q_gen_15, q_gen_14) -> q_gen_47
<b, a, cons>(q_gen_15, q_gen_14) -> q_gen_47
<b, a, cons>(q_gen_20, q_gen_14) -> q_gen_47
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}

}
--
Equality automata are defined for: {eq_elt, eq_eltlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 24  ;  (append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 19  ;  (append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 34
}
Sat witness: Yes: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> nil
})

Total time: 30.000035
Reason for stopping: DontKnow. Stopped because: timeout