Solving ../../benchmarks/true/append_equal_natlist.smt2...

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


Learning problem is:

env: {
nat -> {s, z}  ;  natlist -> {cons, nil}
}
definition:
{
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)])}
(append([_hw, _iw, _jw]) /\ append([_hw, _iw, _kw])) -> eq_natlist([_jw, _kw])
)
}

properties:
{(append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j])}


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0  ;  (append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]) -> 0  ;  (append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]) -> 0
}


Solving took 32.113300 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_100, q_gen_101, q_gen_102, q_gen_103, q_gen_104, q_gen_105, q_gen_106, q_gen_107, q_gen_108, q_gen_109, q_gen_110, q_gen_111, q_gen_112, q_gen_113, q_gen_114, q_gen_115, q_gen_116, q_gen_117, q_gen_118, q_gen_119, q_gen_120, q_gen_121, q_gen_122, q_gen_123, q_gen_124, q_gen_125, q_gen_126, q_gen_127, q_gen_128, q_gen_129, q_gen_130, q_gen_131, q_gen_132, q_gen_133, q_gen_134, q_gen_135, q_gen_136, q_gen_137, q_gen_138, q_gen_139, q_gen_85, q_gen_86, q_gen_87, q_gen_88, q_gen_89, q_gen_90, q_gen_91, q_gen_92, q_gen_93, q_gen_94, q_gen_95, q_gen_96, q_gen_97, q_gen_98, q_gen_99},
Q_f={},
Delta=
{
<nil>() -> q_gen_104
<cons>(q_gen_93, q_gen_104) -> q_gen_112
<z>() -> q_gen_93
<s>(q_gen_93) -> q_gen_98
<s, s>(q_gen_95) -> q_gen_100
<cons, cons>(q_gen_90, q_gen_89, q_gen_88, q_gen_87) -> q_gen_102
<cons, z>(q_gen_93, q_gen_104) -> q_gen_103
<z, cons>(q_gen_93, q_gen_104) -> q_gen_105
<cons, s>(q_gen_90, q_gen_88) -> q_gen_107
<s, cons>(q_gen_90, q_gen_89) -> q_gen_108
<cons, cons>(q_gen_90, q_gen_105, q_gen_103, q_gen_102) -> q_gen_110
<cons, z>(q_gen_93, q_gen_112) -> q_gen_111
<z, cons>(q_gen_93, q_gen_112) -> q_gen_113
<cons, s>(q_gen_116, q_gen_92) -> q_gen_115
<z, s>(q_gen_93) -> q_gen_116
<s, cons>(q_gen_118, q_gen_94) -> q_gen_117
<s, z>(q_gen_93) -> q_gen_118
<cons, cons>(q_gen_100, q_gen_99, q_gen_97, q_gen_87) -> q_gen_133
<cons, s>(q_gen_135, q_gen_92) -> q_gen_134
<s, s>(q_gen_118) -> q_gen_135
<s, cons>(q_gen_137, q_gen_94) -> q_gen_136
<s, s>(q_gen_116) -> q_gen_137
<nil, nil>() -> q_gen_87
<nil, z>() -> q_gen_88
<z, nil>() -> q_gen_89
<z, z>() -> q_gen_90
<nil, s>(q_gen_93) -> q_gen_92
<s, nil>(q_gen_93) -> q_gen_94
<s, s>(q_gen_90) -> q_gen_95
<nil, s>(q_gen_98) -> q_gen_97
<s, nil>(q_gen_98) -> q_gen_99
<nil, cons, cons>(q_gen_90, q_gen_105, q_gen_103, q_gen_102) -> q_gen_101
<cons, nil, cons>(q_gen_95, q_gen_108, q_gen_107, q_gen_102) -> q_gen_106
<nil, cons, cons>(q_gen_90, q_gen_113, q_gen_111, q_gen_110) -> q_gen_109
<cons, nil, cons>(q_gen_100, q_gen_117, q_gen_115, q_gen_102) -> q_gen_114
<cons, nil, cons>(q_gen_118, q_gen_94, q_gen_88, q_gen_87) -> q_gen_119
<nil, cons, cons>(q_gen_90, q_gen_89, q_gen_88, q_gen_87) -> q_gen_120
<cons, nil, cons>(q_gen_95, q_gen_94, q_gen_92, q_gen_87) -> q_gen_121
<nil, cons, cons>(q_gen_116, q_gen_89, q_gen_92, q_gen_87) -> q_gen_122
<cons, cons, cons>(q_gen_131, q_gen_130, q_gen_129, q_gen_128, q_gen_127, q_gen_126, q_gen_125, q_gen_124) -> q_gen_123
<nil, nil, cons>(q_gen_93, q_gen_104) -> q_gen_124
<nil, nil, z>() -> q_gen_125
<nil, z, cons>(q_gen_93, q_gen_104) -> q_gen_126
<nil, z, z>() -> q_gen_127
<z, nil, cons>(q_gen_93, q_gen_104) -> q_gen_128
<z, nil, z>() -> q_gen_129
<z, z, cons>(q_gen_93, q_gen_104) -> q_gen_130
<z, z, z>() -> q_gen_131
<nil, cons, cons>(q_gen_100, q_gen_136, q_gen_134, q_gen_133) -> q_gen_132
<cons, nil, cons>(q_gen_135, q_gen_99, q_gen_92, q_gen_87) -> q_gen_138
<nil, cons, cons>(q_gen_137, q_gen_94, q_gen_97, q_gen_87) -> q_gen_139
<nil, nil, nil>() -> q_gen_85
<cons, nil, cons>(q_gen_90, q_gen_89, q_gen_88, q_gen_87) -> q_gen_86
<nil, cons, cons>(q_gen_95, q_gen_94, q_gen_92, q_gen_87) -> q_gen_91
<cons, nil, cons>(q_gen_100, q_gen_99, q_gen_97, q_gen_87) -> q_gen_96
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004577 s (model generation: 0.003964,  model checking: 0.000613):

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

}

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

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

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

-------------------------------------------
Step 1, which took 0.003893 s (model generation: 0.003510,  model checking: 0.000383):

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  (append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]) -> 1  ;  (append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]) -> 4
}
Sat witness: Yes: ((append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]), {
_gw -> nil  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 2, which took 0.021216 s (model generation: 0.003529,  model checking: 0.017687):

Model:
|_
{
append -> 
{{{
Q={q_gen_85, q_gen_87, q_gen_88, q_gen_89, q_gen_90},
Q_f={q_gen_85},
Delta=
{
<nil, nil>() -> q_gen_87
<nil, z>() -> q_gen_88
<z, nil>() -> q_gen_89
<z, z>() -> q_gen_90
<cons, nil, cons>(q_gen_90, q_gen_89, q_gen_88, q_gen_87) -> q_gen_85
<nil, nil, nil>() -> q_gen_85
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  (append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]) -> 2  ;  (append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]) -> 4
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(s(z), nil)
})

-------------------------------------------
Step 3, which took 0.006609 s (model generation: 0.004596,  model checking: 0.002013):

Model:
|_
{
append -> 
{{{
Q={q_gen_85, q_gen_87, q_gen_88, q_gen_89, q_gen_90, q_gen_93},
Q_f={q_gen_85},
Delta=
{
<z>() -> q_gen_93
<nil, nil>() -> q_gen_87
<nil, s>(q_gen_93) -> q_gen_88
<nil, z>() -> q_gen_88
<s, nil>(q_gen_93) -> q_gen_89
<z, nil>() -> q_gen_89
<s, s>(q_gen_90) -> q_gen_90
<z, z>() -> q_gen_90
<cons, nil, cons>(q_gen_90, q_gen_89, q_gen_88, q_gen_87) -> q_gen_85
<nil, cons, cons>(q_gen_90, q_gen_89, q_gen_88, q_gen_87) -> q_gen_85
<nil, nil, nil>() -> q_gen_85
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  (append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]) -> 3  ;  (append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]) -> 7
}
Sat witness: Yes: ((append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]), {
_gw -> nil  ;  h1 -> s(s(z))  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 4, which took 0.026020 s (model generation: 0.004314,  model checking: 0.021706):

Model:
|_
{
append -> 
{{{
Q={q_gen_100, q_gen_85, q_gen_87, q_gen_88, q_gen_89, q_gen_93},
Q_f={q_gen_85},
Delta=
{
<s>(q_gen_93) -> q_gen_93
<z>() -> q_gen_93
<s, s>(q_gen_100) -> q_gen_100
<z, z>() -> q_gen_100
<nil, nil>() -> q_gen_87
<nil, s>(q_gen_93) -> q_gen_88
<nil, z>() -> q_gen_88
<s, nil>(q_gen_93) -> q_gen_89
<z, nil>() -> q_gen_89
<cons, nil, cons>(q_gen_100, q_gen_89, q_gen_88, q_gen_87) -> q_gen_85
<nil, cons, cons>(q_gen_100, q_gen_89, q_gen_88, q_gen_87) -> q_gen_85
<nil, nil, nil>() -> q_gen_85
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  (append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]) -> 4  ;  (append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]) -> 7
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(z, cons(z, nil))
})

-------------------------------------------
Step 5, which took 0.008669 s (model generation: 0.004636,  model checking: 0.004033):

Model:
|_
{
append -> 
{{{
Q={q_gen_100, q_gen_101, q_gen_102, q_gen_103, q_gen_104, q_gen_105, q_gen_93},
Q_f={q_gen_101},
Delta=
{
<nil>() -> q_gen_104
<s>(q_gen_93) -> q_gen_93
<z>() -> q_gen_93
<s, s>(q_gen_100) -> q_gen_100
<z, z>() -> q_gen_100
<cons, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_102
<nil, nil>() -> q_gen_102
<cons, z>(q_gen_93, q_gen_104) -> q_gen_103
<nil, s>(q_gen_93) -> q_gen_103
<nil, z>() -> q_gen_103
<s, nil>(q_gen_93) -> q_gen_105
<z, cons>(q_gen_93, q_gen_104) -> q_gen_105
<z, nil>() -> q_gen_105
<cons, nil, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_101
<nil, cons, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_101
<nil, nil, nil>() -> q_gen_101
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  (append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]) -> 5  ;  (append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]) -> 10
}
Sat witness: Yes: ((append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]), {
_gw -> cons(z, nil)  ;  h1 -> s(z)  ;  l2 -> nil  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 6, which took 0.043191 s (model generation: 0.004811,  model checking: 0.038380):

Model:
|_
{
append -> 
{{{
Q={q_gen_100, q_gen_101, q_gen_102, q_gen_103, q_gen_104, q_gen_105, q_gen_93},
Q_f={q_gen_101},
Delta=
{
<nil>() -> q_gen_104
<s>(q_gen_93) -> q_gen_93
<z>() -> q_gen_93
<s, s>(q_gen_100) -> q_gen_100
<z, z>() -> q_gen_100
<cons, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_102
<nil, nil>() -> q_gen_102
<cons, s>(q_gen_100, q_gen_103) -> q_gen_103
<cons, z>(q_gen_93, q_gen_104) -> q_gen_103
<nil, s>(q_gen_93) -> q_gen_103
<nil, z>() -> q_gen_103
<s, cons>(q_gen_100, q_gen_105) -> q_gen_105
<s, nil>(q_gen_93) -> q_gen_105
<z, cons>(q_gen_93, q_gen_104) -> q_gen_105
<z, nil>() -> q_gen_105
<cons, nil, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_101
<nil, cons, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_101
<nil, nil, nil>() -> q_gen_101
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  (append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]) -> 6  ;  (append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]) -> 10
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(z, cons(z, cons(z, nil)))
})

-------------------------------------------
Step 7, which took 0.010379 s (model generation: 0.006368,  model checking: 0.004011):

Model:
|_
{
append -> 
{{{
Q={q_gen_100, q_gen_101, q_gen_102, q_gen_103, q_gen_104, q_gen_105, q_gen_93},
Q_f={q_gen_101},
Delta=
{
<cons>(q_gen_93, q_gen_104) -> q_gen_104
<nil>() -> q_gen_104
<s>(q_gen_93) -> q_gen_93
<z>() -> q_gen_93
<s, s>(q_gen_100) -> q_gen_100
<z, z>() -> q_gen_100
<cons, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_102
<nil, nil>() -> q_gen_102
<cons, s>(q_gen_100, q_gen_103) -> q_gen_103
<cons, z>(q_gen_93, q_gen_104) -> q_gen_103
<nil, s>(q_gen_93) -> q_gen_103
<nil, z>() -> q_gen_103
<s, cons>(q_gen_100, q_gen_105) -> q_gen_105
<s, nil>(q_gen_93) -> q_gen_105
<z, cons>(q_gen_93, q_gen_104) -> q_gen_105
<z, nil>() -> q_gen_105
<cons, nil, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_101
<nil, cons, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_101
<nil, nil, nil>() -> q_gen_101
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  (append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]) -> 7  ;  (append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]) -> 13
}
Sat witness: Yes: ((append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]), {
_gw -> cons(z, nil)  ;  h1 -> s(s(z))  ;  l2 -> nil  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 8, which took 0.006708 s (model generation: 0.006107,  model checking: 0.000601):

Model:
|_
{
append -> 
{{{
Q={q_gen_100, q_gen_101, q_gen_102, q_gen_103, q_gen_104, q_gen_105, q_gen_93},
Q_f={q_gen_101},
Delta=
{
<cons>(q_gen_93, q_gen_104) -> q_gen_104
<nil>() -> q_gen_104
<s>(q_gen_93) -> q_gen_93
<z>() -> q_gen_93
<s, s>(q_gen_100) -> q_gen_100
<s, z>(q_gen_93) -> q_gen_100
<z, s>(q_gen_93) -> q_gen_100
<z, z>() -> q_gen_100
<cons, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_102
<nil, nil>() -> q_gen_102
<cons, s>(q_gen_100, q_gen_103) -> q_gen_103
<cons, z>(q_gen_93, q_gen_104) -> q_gen_103
<nil, s>(q_gen_93) -> q_gen_103
<nil, z>() -> q_gen_103
<s, cons>(q_gen_100, q_gen_105) -> q_gen_105
<s, nil>(q_gen_93) -> q_gen_105
<z, cons>(q_gen_93, q_gen_104) -> q_gen_105
<z, nil>() -> q_gen_105
<cons, nil, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_101
<nil, cons, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_101
<nil, nil, nil>() -> q_gen_101
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  (append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]) -> 10  ;  (append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]) -> 13
}
Sat witness: Yes: ((append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]), {
_lw -> cons(z, nil)  ;  _nw -> cons(z, nil)  ;  _ow -> cons(z, nil)  ;  i -> z  ;  j -> s(z)  ;  l1 -> nil  ;  l2 -> nil
})

-------------------------------------------
Step 9, which took 0.007023 s (model generation: 0.006666,  model checking: 0.000357):

Model:
|_
{
append -> 
{{{
Q={q_gen_100, q_gen_101, q_gen_102, q_gen_103, q_gen_104, q_gen_105, q_gen_118, q_gen_119, q_gen_93},
Q_f={q_gen_101},
Delta=
{
<cons>(q_gen_93, q_gen_104) -> q_gen_104
<nil>() -> q_gen_104
<s>(q_gen_93) -> q_gen_93
<z>() -> q_gen_93
<s, s>(q_gen_100) -> q_gen_100
<z, s>(q_gen_93) -> q_gen_100
<z, z>() -> q_gen_100
<cons, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_102
<nil, nil>() -> q_gen_102
<cons, s>(q_gen_100, q_gen_103) -> q_gen_103
<cons, z>(q_gen_93, q_gen_104) -> q_gen_103
<nil, s>(q_gen_93) -> q_gen_103
<nil, z>() -> q_gen_103
<s, cons>(q_gen_100, q_gen_105) -> q_gen_105
<s, cons>(q_gen_118, q_gen_105) -> q_gen_105
<s, nil>(q_gen_93) -> q_gen_105
<z, cons>(q_gen_93, q_gen_104) -> q_gen_105
<z, nil>() -> q_gen_105
<s, z>(q_gen_93) -> q_gen_118
<cons, nil, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_101
<nil, cons, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_101
<nil, nil, nil>() -> q_gen_101
<cons, nil, cons>(q_gen_118, q_gen_105, q_gen_103, q_gen_102) -> q_gen_119
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  (append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]) -> 13  ;  (append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]) -> 13
}
Sat witness: Yes: ((append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]), {
_lw -> cons(z, nil)  ;  _nw -> cons(s(z), nil)  ;  _ow -> cons(s(z), nil)  ;  i -> z  ;  j -> s(z)  ;  l1 -> nil  ;  l2 -> nil
})

-------------------------------------------
Step 10, which took 0.012015 s (model generation: 0.010271,  model checking: 0.001744):

Model:
|_
{
append -> 
{{{
Q={q_gen_100, q_gen_101, q_gen_102, q_gen_103, q_gen_104, q_gen_105, q_gen_117, q_gen_120, q_gen_93},
Q_f={q_gen_101},
Delta=
{
<cons>(q_gen_93, q_gen_104) -> q_gen_104
<nil>() -> q_gen_104
<s>(q_gen_93) -> q_gen_93
<z>() -> q_gen_93
<s, s>(q_gen_100) -> q_gen_100
<s, z>(q_gen_93) -> q_gen_100
<z, s>(q_gen_93) -> q_gen_100
<z, z>() -> q_gen_100
<cons, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_102
<cons, cons>(q_gen_100, q_gen_117, q_gen_103, q_gen_102) -> q_gen_102
<nil, nil>() -> q_gen_102
<cons, s>(q_gen_100, q_gen_103) -> q_gen_103
<cons, z>(q_gen_93, q_gen_104) -> q_gen_103
<nil, s>(q_gen_93) -> q_gen_103
<nil, z>() -> q_gen_103
<s, cons>(q_gen_100, q_gen_117) -> q_gen_105
<s, nil>(q_gen_93) -> q_gen_105
<z, cons>(q_gen_93, q_gen_104) -> q_gen_105
<s, cons>(q_gen_100, q_gen_105) -> q_gen_117
<z, nil>() -> q_gen_117
<cons, nil, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_101
<cons, nil, cons>(q_gen_100, q_gen_117, q_gen_103, q_gen_102) -> q_gen_101
<nil, cons, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_101
<nil, nil, nil>() -> q_gen_101
<nil, cons, cons>(q_gen_100, q_gen_117, q_gen_103, q_gen_102) -> q_gen_120
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15  ;  (append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]) -> 13  ;  (append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]) -> 13
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(z, nil)
})

-------------------------------------------
Step 11, which took 17.309916 s (model generation: 0.016069,  model checking: 17.293847):

Model:
|_
{
append -> 
{{{
Q={q_gen_100, q_gen_101, q_gen_102, q_gen_103, q_gen_104, q_gen_105, q_gen_116, q_gen_119, q_gen_93},
Q_f={q_gen_101},
Delta=
{
<cons>(q_gen_93, q_gen_104) -> q_gen_104
<nil>() -> q_gen_104
<s>(q_gen_93) -> q_gen_93
<z>() -> q_gen_93
<s, s>(q_gen_100) -> q_gen_100
<z, z>() -> q_gen_100
<cons, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_102
<nil, nil>() -> q_gen_102
<cons, s>(q_gen_100, q_gen_103) -> q_gen_103
<cons, s>(q_gen_116, q_gen_103) -> q_gen_103
<cons, z>(q_gen_93, q_gen_104) -> q_gen_103
<nil, s>(q_gen_93) -> q_gen_103
<nil, z>() -> q_gen_103
<s, cons>(q_gen_100, q_gen_105) -> q_gen_105
<s, cons>(q_gen_116, q_gen_105) -> q_gen_105
<s, nil>(q_gen_93) -> q_gen_105
<z, cons>(q_gen_93, q_gen_104) -> q_gen_105
<z, nil>() -> q_gen_105
<s, z>(q_gen_93) -> q_gen_116
<z, s>(q_gen_93) -> q_gen_116
<cons, nil, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_101
<nil, cons, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_101
<nil, nil, nil>() -> q_gen_101
<cons, nil, cons>(q_gen_116, q_gen_105, q_gen_103, q_gen_102) -> q_gen_119
<nil, cons, cons>(q_gen_116, q_gen_105, q_gen_103, q_gen_102) -> q_gen_119
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15  ;  (append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]) -> 13  ;  (append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]) -> 16
}
Sat witness: Yes: ((append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]), {
_gw -> cons(z, nil)  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 12, which took 10.135157 s (model generation: 0.009415,  model checking: 10.125742):

Model:
|_
{
append -> 
{{{
Q={q_gen_100, q_gen_101, q_gen_102, q_gen_103, q_gen_104, q_gen_105, q_gen_116, q_gen_119, q_gen_125, q_gen_126, q_gen_127, q_gen_128, q_gen_129, q_gen_130, q_gen_131, q_gen_93},
Q_f={q_gen_101},
Delta=
{
<cons>(q_gen_93, q_gen_104) -> q_gen_104
<nil>() -> q_gen_104
<s>(q_gen_93) -> q_gen_93
<z>() -> q_gen_93
<s, s>(q_gen_100) -> q_gen_100
<z, z>() -> q_gen_100
<cons, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_102
<nil, nil>() -> q_gen_102
<cons, s>(q_gen_100, q_gen_103) -> q_gen_103
<cons, s>(q_gen_116, q_gen_103) -> q_gen_103
<cons, z>(q_gen_93, q_gen_104) -> q_gen_103
<nil, s>(q_gen_93) -> q_gen_103
<nil, z>() -> q_gen_103
<s, cons>(q_gen_100, q_gen_105) -> q_gen_105
<s, cons>(q_gen_116, q_gen_105) -> q_gen_105
<s, nil>(q_gen_93) -> q_gen_105
<z, cons>(q_gen_93, q_gen_104) -> q_gen_105
<z, nil>() -> q_gen_105
<s, z>(q_gen_93) -> q_gen_116
<z, s>(q_gen_93) -> q_gen_116
<cons, cons, cons>(q_gen_131, q_gen_130, q_gen_129, q_gen_128, q_gen_127, q_gen_126, q_gen_125, q_gen_119) -> q_gen_101
<cons, nil, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_101
<nil, cons, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_101
<nil, nil, nil>() -> q_gen_101
<cons, nil, cons>(q_gen_116, q_gen_105, q_gen_103, q_gen_102) -> q_gen_119
<nil, cons, cons>(q_gen_116, q_gen_105, q_gen_103, q_gen_102) -> q_gen_119
<nil, nil, cons>(q_gen_93, q_gen_104) -> q_gen_119
<nil, nil, z>() -> q_gen_125
<nil, z, cons>(q_gen_93, q_gen_104) -> q_gen_126
<nil, z, z>() -> q_gen_127
<z, nil, cons>(q_gen_93, q_gen_104) -> q_gen_128
<z, nil, z>() -> q_gen_129
<z, z, cons>(q_gen_93, q_gen_104) -> q_gen_130
<z, z, z>() -> q_gen_131
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18  ;  (append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]) -> 14  ;  (append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]) -> 16
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(s(s(z)), cons(s(s(z)), nil))
})

-------------------------------------------
Step 13, which took 0.014892 s (model generation: 0.011089,  model checking: 0.003803):

Model:
|_
{
append -> 
{{{
Q={q_gen_100, q_gen_101, q_gen_102, q_gen_103, q_gen_104, q_gen_105, q_gen_116, q_gen_119, q_gen_125, q_gen_126, q_gen_127, q_gen_128, q_gen_129, q_gen_130, q_gen_131, q_gen_93},
Q_f={q_gen_101},
Delta=
{
<cons>(q_gen_93, q_gen_104) -> q_gen_104
<nil>() -> q_gen_104
<s>(q_gen_93) -> q_gen_93
<z>() -> q_gen_93
<s, s>(q_gen_100) -> q_gen_100
<s, s>(q_gen_116) -> q_gen_100
<z, z>() -> q_gen_100
<cons, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_102
<nil, nil>() -> q_gen_102
<cons, s>(q_gen_100, q_gen_103) -> q_gen_103
<cons, s>(q_gen_116, q_gen_103) -> q_gen_103
<cons, z>(q_gen_93, q_gen_104) -> q_gen_103
<nil, s>(q_gen_93) -> q_gen_103
<nil, z>() -> q_gen_103
<s, cons>(q_gen_100, q_gen_105) -> q_gen_105
<s, cons>(q_gen_116, q_gen_105) -> q_gen_105
<s, nil>(q_gen_93) -> q_gen_105
<z, cons>(q_gen_93, q_gen_104) -> q_gen_105
<z, nil>() -> q_gen_105
<s, z>(q_gen_93) -> q_gen_116
<z, s>(q_gen_93) -> q_gen_116
<cons, cons, cons>(q_gen_131, q_gen_130, q_gen_129, q_gen_128, q_gen_127, q_gen_126, q_gen_125, q_gen_119) -> q_gen_101
<cons, nil, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_101
<nil, cons, cons>(q_gen_100, q_gen_105, q_gen_103, q_gen_102) -> q_gen_101
<nil, nil, nil>() -> q_gen_101
<cons, nil, cons>(q_gen_116, q_gen_105, q_gen_103, q_gen_102) -> q_gen_119
<nil, cons, cons>(q_gen_116, q_gen_105, q_gen_103, q_gen_102) -> q_gen_119
<nil, nil, cons>(q_gen_93, q_gen_104) -> q_gen_119
<nil, nil, z>() -> q_gen_125
<nil, z, cons>(q_gen_93, q_gen_104) -> q_gen_126
<nil, z, z>() -> q_gen_127
<z, nil, cons>(q_gen_93, q_gen_104) -> q_gen_128
<z, nil, z>() -> q_gen_129
<z, z, cons>(q_gen_93, q_gen_104) -> q_gen_130
<z, z, z>() -> q_gen_131
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18  ;  (append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]) -> 17  ;  (append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]) -> 16
}
Sat witness: Yes: ((append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]), {
_lw -> cons(s(z), nil)  ;  _nw -> cons(s(z), nil)  ;  _ow -> cons(s(s(z)), nil)  ;  i -> s(z)  ;  j -> s(s(z))  ;  l1 -> nil  ;  l2 -> nil
})

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