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, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)])}
(append([_mea, _nea, _oea]) /\ append([_mea, _nea, _pea])) -> eq_natlist([_oea, _pea])
)
(reverse, F:
{() -> reverse([nil, nil])
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea])}
(reverse([_sea, _tea]) /\ reverse([_sea, _uea])) -> eq_natlist([_tea, _uea])
)
(leq, P:
{() -> leq([z, s(nn2)])
() -> leq([z, z])
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)])
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2])
(leq([s(nn1), z])) -> BOT}
)
(length, F:
{() -> length([nil, z])
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)])}
(length([_wea, _xea]) /\ length([_wea, _yea])) -> eq_nat([_xea, _yea])
)
}

properties:
{(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa])}


over-approximation: {append, length, reverse}
under-approximation: {leq}

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 0
() -> leq([z, s(nn2)]) -> 0
() -> leq([z, z]) -> 0
() -> reverse([nil, nil]) -> 0
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 0
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 0
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 0
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 0
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 0
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 0
(leq([s(nn1), z])) -> BOT -> 0
}


Solving took 60.570649 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6017, q_gen_6018, q_gen_6019, q_gen_6022, q_gen_6023, q_gen_6024, q_gen_6025, q_gen_6030, q_gen_6031, q_gen_6032, q_gen_6033, q_gen_6034, q_gen_6035, q_gen_6038, q_gen_6039, q_gen_6040, q_gen_6045, q_gen_6046, q_gen_6047, q_gen_6048, q_gen_6049, q_gen_6053, q_gen_6054, q_gen_6055, q_gen_6061, q_gen_6062, q_gen_6065, q_gen_6066, q_gen_6067, q_gen_6068, q_gen_6069, q_gen_6070, q_gen_6075, q_gen_6076, q_gen_6080, q_gen_6081, q_gen_6082, q_gen_6083, q_gen_6084, q_gen_6085, q_gen_6090, q_gen_6091},
Q_f={},
Delta=
{
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<cons>(q_gen_6033, q_gen_6032) -> q_gen_6047
<nil, nil>() -> q_gen_6018
<z, z>() -> q_gen_6019
<cons, cons>(q_gen_6024, q_gen_6018) -> q_gen_6023
<s, s>(q_gen_6019) -> q_gen_6024
<nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6039
<nil, cons>(q_gen_6033, q_gen_6047) -> q_gen_6049
<cons, cons>(q_gen_6019, q_gen_6069) -> q_gen_6068
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6069
<cons, cons>(q_gen_6019, q_gen_6039) -> q_gen_6091
<nil, nil, nil>() -> q_gen_6013
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6017
<nil, cons, cons>(q_gen_6024, q_gen_6023) -> q_gen_6022
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6025
<cons, cons, cons>(q_gen_6034, q_gen_6031) -> q_gen_6030
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6031
<z, z, z>() -> q_gen_6034
<nil, cons, cons>(q_gen_6024, q_gen_6018) -> q_gen_6035
<cons, nil, cons>(q_gen_6019, q_gen_6039) -> q_gen_6038
<nil, cons, cons>(q_gen_6019, q_gen_6039) -> q_gen_6040
<cons, cons, cons>(q_gen_6034, q_gen_6046) -> q_gen_6045
<nil, nil, cons>(q_gen_6033, q_gen_6047) -> q_gen_6046
<nil, cons, cons>(q_gen_6019, q_gen_6049) -> q_gen_6048
<cons, cons, cons>(q_gen_6054, q_gen_6046) -> q_gen_6053
<s, z, s>(q_gen_6019) -> q_gen_6054
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6055
<cons, cons, cons>(q_gen_6034, q_gen_6038) -> q_gen_6061
<cons, cons, cons>(q_gen_6034, q_gen_6017) -> q_gen_6062
<cons, cons, cons>(q_gen_6034, q_gen_6040) -> q_gen_6065
<cons, cons, cons>(q_gen_6054, q_gen_6045) -> q_gen_6066
<nil, cons, cons>(q_gen_6019, q_gen_6068) -> q_gen_6067
<cons, cons, cons>(q_gen_6054, q_gen_6031) -> q_gen_6070
<nil, cons, cons>(q_gen_6019, q_gen_6069) -> q_gen_6075
<cons, cons, cons>(q_gen_6054, q_gen_6040) -> q_gen_6076
<cons, cons, cons>(q_gen_6034, q_gen_6081) -> q_gen_6080
<cons, nil, cons>(q_gen_6019, q_gen_6069) -> q_gen_6081
<cons, cons, cons>(q_gen_6034, q_gen_6083) -> q_gen_6082
<cons, nil, cons>(q_gen_6019, q_gen_6068) -> q_gen_6083
<cons, cons, cons>(q_gen_6034, q_gen_6085) -> q_gen_6084
<cons, nil, cons>(q_gen_6024, q_gen_6069) -> q_gen_6085
<cons, nil, cons>(q_gen_6019, q_gen_6091) -> q_gen_6090
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6015, q_gen_6016, q_gen_6028, q_gen_6029, q_gen_6059, q_gen_6077},
Q_f={},
Delta=
{
<z>() -> q_gen_6016
<s>(q_gen_6016) -> q_gen_6029
<nil, z>() -> q_gen_6012
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6015
<cons, s>(q_gen_6029, q_gen_6012) -> q_gen_6028
<cons, s>(q_gen_6016, q_gen_6015) -> q_gen_6059
<cons, s>(q_gen_6016, q_gen_6059) -> q_gen_6077
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6010, q_gen_6011, q_gen_6014, q_gen_6020, q_gen_6021, q_gen_6058, q_gen_6060, q_gen_6078},
Q_f={},
Delta=
{
<z>() -> q_gen_6011
<s>(q_gen_6011) -> q_gen_6021
<z, z>() -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6010
<s, s>(q_gen_6009) -> q_gen_6014
<z, s>(q_gen_6021) -> q_gen_6020
<s, z>(q_gen_6011) -> q_gen_6058
<s, s>(q_gen_6058) -> q_gen_6060
<s, s>(q_gen_6060) -> q_gen_6078
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6026, q_gen_6027, q_gen_6036, q_gen_6037, q_gen_6041, q_gen_6042, q_gen_6043, q_gen_6044, q_gen_6050, q_gen_6051, q_gen_6052, q_gen_6056, q_gen_6057, q_gen_6063, q_gen_6064, q_gen_6071, q_gen_6072, q_gen_6073, q_gen_6074, q_gen_6079, q_gen_6086, q_gen_6087, q_gen_6088, q_gen_6089},
Q_f={},
Delta=
{
<nil>() -> q_gen_6043
<z>() -> q_gen_6044
<cons>(q_gen_6044, q_gen_6043) -> q_gen_6052
<nil, nil>() -> q_gen_6008
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6026
<z, z>() -> q_gen_6027
<cons, cons>(q_gen_6037, q_gen_6008) -> q_gen_6036
<s, s>(q_gen_6027) -> q_gen_6037
<cons, cons>(q_gen_6027, q_gen_6042) -> q_gen_6041
<nil, cons>(q_gen_6044, q_gen_6043) -> q_gen_6042
<cons, cons>(q_gen_6027, q_gen_6051) -> q_gen_6050
<nil, cons>(q_gen_6044, q_gen_6052) -> q_gen_6051
<cons, cons>(q_gen_6027, q_gen_6057) -> q_gen_6056
<cons, nil>(q_gen_6044, q_gen_6043) -> q_gen_6057
<cons, cons>(q_gen_6027, q_gen_6026) -> q_gen_6063
<cons, cons>(q_gen_6027, q_gen_6056) -> q_gen_6064
<cons, cons>(q_gen_6074, q_gen_6072) -> q_gen_6071
<cons, cons>(q_gen_6073, q_gen_6008) -> q_gen_6072
<s, z>(q_gen_6044) -> q_gen_6073
<z, s>(q_gen_6044) -> q_gen_6074
<cons, cons>(q_gen_6027, q_gen_6041) -> q_gen_6079
<cons, cons>(q_gen_6073, q_gen_6087) -> q_gen_6086
<cons, cons>(q_gen_6074, q_gen_6026) -> q_gen_6087
<cons, cons>(q_gen_6027, q_gen_6089) -> q_gen_6088
<cons, cons>(q_gen_6037, q_gen_6056) -> q_gen_6089
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.008020 s (model generation: 0.007584,  model checking: 0.000436):

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

}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={},
Q_f={},
Delta=
{

}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 0
() -> leq([z, s(nn2)]) -> 0
() -> leq([z, z]) -> 0
() -> reverse([nil, nil]) -> 3
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 1
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 1
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 1
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Found: (() -> reverse([nil, nil]), {

})

-------------------------------------------
Step 1, which took 0.010573 s (model generation: 0.010434,  model checking: 0.000139):

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

}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008},
Q_f={q_gen_6008},
Delta=
{
<nil, nil>() -> q_gen_6008
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 0
() -> leq([z, s(nn2)]) -> 0
() -> leq([z, z]) -> 3
() -> reverse([nil, nil]) -> 3
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 1
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 1
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 1
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Found: (() -> leq([z, z]), {

})

-------------------------------------------
Step 2, which took 0.011249 s (model generation: 0.011107,  model checking: 0.000142):

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

}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009},
Q_f={q_gen_6009},
Delta=
{
<z, z>() -> q_gen_6009
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008},
Q_f={q_gen_6008},
Delta=
{
<nil, nil>() -> q_gen_6008
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 0
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
() -> reverse([nil, nil]) -> 3
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 1
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 1
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 1
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Found: (() -> leq([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 3, which took 0.010968 s (model generation: 0.010871,  model checking: 0.000097):

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

}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011},
Q_f={q_gen_6009},
Delta=
{
<z>() -> q_gen_6011
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008},
Q_f={q_gen_6008},
Delta=
{
<nil, nil>() -> q_gen_6008
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
() -> reverse([nil, nil]) -> 3
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 1
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 1
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 1
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Found: (() -> length([nil, z]), {

})

-------------------------------------------
Step 4, which took 0.011195 s (model generation: 0.010864,  model checking: 0.000331):

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

}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012},
Q_f={q_gen_6012},
Delta=
{
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011},
Q_f={q_gen_6009},
Delta=
{
<z>() -> q_gen_6011
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008},
Q_f={q_gen_6008},
Delta=
{
<nil, nil>() -> q_gen_6008
}

Datatype: <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
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
() -> reverse([nil, nil]) -> 3
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 1
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 1
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 1
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 5, which took 0.011596 s (model generation: 0.011348,  model checking: 0.000248):

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

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012},
Q_f={q_gen_6012},
Delta=
{
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011},
Q_f={q_gen_6009},
Delta=
{
<z>() -> q_gen_6011
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008},
Q_f={q_gen_6008},
Delta=
{
<nil, nil>() -> q_gen_6008
}

Datatype: <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
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
() -> reverse([nil, nil]) -> 3
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 1
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 1
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 1
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2
(leq([s(nn1), z])) -> BOT -> 2
}
Sat witness: Found: ((leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 6, which took 0.011182 s (model generation: 0.010976,  model checking: 0.000206):

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

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012},
Q_f={q_gen_6012},
Delta=
{
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011},
Q_f={q_gen_6009},
Delta=
{
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008},
Q_f={q_gen_6008},
Delta=
{
<nil, nil>() -> q_gen_6008
}

Datatype: <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
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
() -> reverse([nil, nil]) -> 3
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 1
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 1
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 1
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2
(leq([s(nn1), z])) -> BOT -> 2
}
Sat witness: Found: ((length([ll, _vea])) -> length([cons(x, ll), s(_vea)]), {
_vea -> z  ;  ll -> nil  ;  x -> z
})

-------------------------------------------
Step 7, which took 0.012782 s (model generation: 0.012198,  model checking: 0.000584):

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

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011},
Q_f={q_gen_6009},
Delta=
{
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008},
Q_f={q_gen_6008},
Delta=
{
<nil, nil>() -> q_gen_6008
}

Datatype: <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
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
() -> reverse([nil, nil]) -> 3
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 1
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 4
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 2
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2
(leq([s(nn1), z])) -> BOT -> 2
}
Sat witness: Found: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), {
_lea -> nil  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 8, which took 0.014083 s (model generation: 0.012811,  model checking: 0.001272):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019},
Q_f={q_gen_6013},
Delta=
{
<nil, nil>() -> q_gen_6018
<z, z>() -> q_gen_6019
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011},
Q_f={q_gen_6009},
Delta=
{
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008},
Q_f={q_gen_6008},
Delta=
{
<nil, nil>() -> q_gen_6008
}

Datatype: <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
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 4
() -> reverse([nil, nil]) -> 4
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 2
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 4
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 3
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 3
(leq([s(nn1), z])) -> BOT -> 3
}
Sat witness: Found: (() -> leq([z, s(nn2)]), {
nn2 -> s(z)
})

-------------------------------------------
Step 9, which took 0.015210 s (model generation: 0.013858,  model checking: 0.001352):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019},
Q_f={q_gen_6013},
Delta=
{
<nil, nil>() -> q_gen_6018
<z, z>() -> q_gen_6019
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008},
Q_f={q_gen_6008},
Delta=
{
<nil, nil>() -> q_gen_6008
}

Datatype: <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
() -> length([nil, z]) -> 4
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 4
() -> reverse([nil, nil]) -> 4
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 3
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 4
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 4
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4
(leq([s(nn1), z])) -> BOT -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(s(z), cons(s(z), nil))
})

-------------------------------------------
Step 10, which took 0.014205 s (model generation: 0.013888,  model checking: 0.000317):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019},
Q_f={q_gen_6013},
Delta=
{
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008},
Q_f={q_gen_6008},
Delta=
{
<nil, nil>() -> q_gen_6008
}

Datatype: <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
() -> length([nil, z]) -> 4
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 4
() -> reverse([nil, nil]) -> 4
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 6
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 4
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 4
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4
(leq([s(nn1), z])) -> BOT -> 4
}
Sat witness: Found: ((append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]), {
_qea -> nil  ;  _rea -> cons(z, nil)  ;  h1 -> z  ;  t1 -> nil
})

-------------------------------------------
Step 11, which took 0.010192 s (model generation: 0.009711,  model checking: 0.000481):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019},
Q_f={q_gen_6013},
Delta=
{
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027},
Q_f={q_gen_6008},
Delta=
{
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<z, z>() -> q_gen_6027
}

Datatype: <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
() -> length([nil, z]) -> 4
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 4
() -> reverse([nil, nil]) -> 4
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 6
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 4
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 4
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5
(leq([s(nn1), z])) -> BOT -> 5
}
Sat witness: Found: ((length([ll, _vea])) -> length([cons(x, ll), s(_vea)]), {
_vea -> z  ;  ll -> nil  ;  x -> s(z)
})

-------------------------------------------
Step 12, which took 0.006426 s (model generation: 0.005213,  model checking: 0.001213):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019},
Q_f={q_gen_6013},
Delta=
{
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027},
Q_f={q_gen_6008},
Delta=
{
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<z, z>() -> q_gen_6027
}

Datatype: <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
() -> length([nil, z]) -> 4
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 4
() -> reverse([nil, nil]) -> 4
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 6
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 7
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 5
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5
(leq([s(nn1), z])) -> BOT -> 5
}
Sat witness: Found: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), {
_lea -> cons(z, nil)  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 13, which took 0.006249 s (model generation: 0.005580,  model checking: 0.000669):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019, q_gen_6032, q_gen_6033, q_gen_6034},
Q_f={q_gen_6013},
Delta=
{
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6013
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
<z, z, z>() -> q_gen_6034
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027},
Q_f={q_gen_6008},
Delta=
{
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<z, z>() -> q_gen_6027
}

Datatype: <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
() -> length([nil, z]) -> 5
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 5
() -> reverse([nil, nil]) -> 5
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 9
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 7
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 6
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 6
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 6
(leq([s(nn1), z])) -> BOT -> 6
}
Sat witness: Found: ((append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]), {
_qea -> nil  ;  _rea -> cons(s(z), nil)  ;  h1 -> s(z)  ;  t1 -> nil
})

-------------------------------------------
Step 14, which took 0.011522 s (model generation: 0.008633,  model checking: 0.002889):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019, q_gen_6032, q_gen_6033, q_gen_6034},
Q_f={q_gen_6013},
Delta=
{
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6013
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
<z, z, z>() -> q_gen_6034
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027},
Q_f={q_gen_6008},
Delta=
{
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<s, s>(q_gen_6027) -> q_gen_6027
<z, z>() -> q_gen_6027
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> length([nil, z]) -> 6
() -> leq([z, s(nn2)]) -> 7
() -> leq([z, z]) -> 6
() -> reverse([nil, nil]) -> 6
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 9
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 10
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 7
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 8
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 7
(leq([s(nn1), z])) -> BOT -> 7
}
Sat witness: Found: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), {
_lea -> cons(z, nil)  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 15, which took 0.019186 s (model generation: 0.016908,  model checking: 0.002278):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019, q_gen_6032, q_gen_6033, q_gen_6034},
Q_f={q_gen_6013},
Delta=
{
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6018
<nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6013
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
<z, z, z>() -> q_gen_6034
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027},
Q_f={q_gen_6008},
Delta=
{
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<s, s>(q_gen_6027) -> q_gen_6027
<z, z>() -> q_gen_6027
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 8
() -> length([nil, z]) -> 7
() -> leq([z, s(nn2)]) -> 8
() -> leq([z, z]) -> 7
() -> reverse([nil, nil]) -> 7
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 12
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 10
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 8
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 9
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 8
(leq([s(nn1), z])) -> BOT -> 8
}
Sat witness: Found: ((append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]), {
_qea -> nil  ;  _rea -> cons(z, cons(z, nil))  ;  h1 -> z  ;  t1 -> nil
})

-------------------------------------------
Step 16, which took 0.022962 s (model generation: 0.018821,  model checking: 0.004141):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019, q_gen_6032, q_gen_6033, q_gen_6034},
Q_f={q_gen_6013},
Delta=
{
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6018
<nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6013
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
<z, z, z>() -> q_gen_6034
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027, q_gen_6043, q_gen_6044},
Q_f={q_gen_6008},
Delta=
{
<nil>() -> q_gen_6043
<z>() -> q_gen_6044
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<nil, cons>(q_gen_6044, q_gen_6043) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<s, s>(q_gen_6027) -> q_gen_6027
<z, z>() -> q_gen_6027
}

Datatype: <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
() -> length([nil, z]) -> 8
() -> leq([z, s(nn2)]) -> 9
() -> leq([z, z]) -> 8
() -> reverse([nil, nil]) -> 8
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 12
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 13
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 9
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 10
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 9
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 9
(leq([s(nn1), z])) -> BOT -> 9
}
Sat witness: Found: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), {
_lea -> cons(z, cons(z, nil))  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 17, which took 0.021802 s (model generation: 0.019156,  model checking: 0.002646):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019, q_gen_6032, q_gen_6033, q_gen_6034},
Q_f={q_gen_6013},
Delta=
{
<cons>(q_gen_6033, q_gen_6032) -> q_gen_6032
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6018
<nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6013
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
<z, z, z>() -> q_gen_6034
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027, q_gen_6043, q_gen_6044},
Q_f={q_gen_6008},
Delta=
{
<nil>() -> q_gen_6043
<z>() -> q_gen_6044
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<nil, cons>(q_gen_6044, q_gen_6043) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<s, s>(q_gen_6027) -> q_gen_6027
<z, z>() -> q_gen_6027
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> length([nil, z]) -> 9
() -> leq([z, s(nn2)]) -> 10
() -> leq([z, z]) -> 9
() -> reverse([nil, nil]) -> 9
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 15
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 13
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 10
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 11
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10
(leq([s(nn1), z])) -> BOT -> 10
}
Sat witness: Found: ((append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]), {
_qea -> nil  ;  _rea -> cons(z, cons(z, cons(z, nil)))  ;  h1 -> z  ;  t1 -> nil
})

-------------------------------------------
Step 18, which took 0.027922 s (model generation: 0.021838,  model checking: 0.006084):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019, q_gen_6032, q_gen_6033, q_gen_6034},
Q_f={q_gen_6013},
Delta=
{
<cons>(q_gen_6033, q_gen_6032) -> q_gen_6032
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6018
<nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6013
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
<z, z, z>() -> q_gen_6034
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027, q_gen_6043, q_gen_6044},
Q_f={q_gen_6008},
Delta=
{
<cons>(q_gen_6044, q_gen_6043) -> q_gen_6043
<nil>() -> q_gen_6043
<z>() -> q_gen_6044
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<nil, cons>(q_gen_6044, q_gen_6043) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<s, s>(q_gen_6027) -> q_gen_6027
<z, z>() -> q_gen_6027
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 11
() -> length([nil, z]) -> 10
() -> leq([z, s(nn2)]) -> 11
() -> leq([z, z]) -> 10
() -> reverse([nil, nil]) -> 10
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 15
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 16
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 11
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 12
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11
(leq([s(nn1), z])) -> BOT -> 11
}
Sat witness: Found: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), {
_lea -> cons(z, cons(z, nil))  ;  h1 -> s(z)  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 19, which took 0.029082 s (model generation: 0.024755,  model checking: 0.004327):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019, q_gen_6032, q_gen_6033, q_gen_6034},
Q_f={q_gen_6013},
Delta=
{
<cons>(q_gen_6033, q_gen_6032) -> q_gen_6032
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6018
<nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6013
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
<s, z, s>(q_gen_6019) -> q_gen_6034
<z, z, z>() -> q_gen_6034
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027, q_gen_6043, q_gen_6044},
Q_f={q_gen_6008},
Delta=
{
<cons>(q_gen_6044, q_gen_6043) -> q_gen_6043
<nil>() -> q_gen_6043
<z>() -> q_gen_6044
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<nil, cons>(q_gen_6044, q_gen_6043) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<s, s>(q_gen_6027) -> q_gen_6027
<z, z>() -> q_gen_6027
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12
() -> length([nil, z]) -> 11
() -> leq([z, s(nn2)]) -> 12
() -> leq([z, z]) -> 11
() -> reverse([nil, nil]) -> 11
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 18
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 16
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 12
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 13
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 12
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 12
(leq([s(nn1), z])) -> BOT -> 12
}
Sat witness: Found: ((append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]), {
_qea -> cons(z, nil)  ;  _rea -> cons(z, nil)  ;  h1 -> z  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 20, which took 0.029734 s (model generation: 0.028739,  model checking: 0.000995):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019, q_gen_6032, q_gen_6033, q_gen_6034},
Q_f={q_gen_6013},
Delta=
{
<cons>(q_gen_6033, q_gen_6032) -> q_gen_6032
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6018
<nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6013
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
<s, z, s>(q_gen_6019) -> q_gen_6034
<z, z, z>() -> q_gen_6034
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027, q_gen_6043, q_gen_6044},
Q_f={q_gen_6008},
Delta=
{
<cons>(q_gen_6044, q_gen_6043) -> q_gen_6043
<nil>() -> q_gen_6043
<z>() -> q_gen_6044
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<cons, nil>(q_gen_6044, q_gen_6043) -> q_gen_6008
<nil, cons>(q_gen_6044, q_gen_6043) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<s, s>(q_gen_6027) -> q_gen_6027
<z, z>() -> q_gen_6027
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12
() -> length([nil, z]) -> 12
() -> leq([z, s(nn2)]) -> 12
() -> leq([z, z]) -> 12
() -> reverse([nil, nil]) -> 12
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 18
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 16
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 15
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 13
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 13
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 13
(leq([s(nn1), z])) -> BOT -> 13
}
Sat witness: Found: ((length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]), {
_afa -> nil  ;  _bfa -> z  ;  _zea -> s(z)  ;  l1 -> cons(z, nil)
})

-------------------------------------------
Step 21, which took 0.021085 s (model generation: 0.019847,  model checking: 0.001238):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019, q_gen_6032, q_gen_6033, q_gen_6034},
Q_f={q_gen_6013},
Delta=
{
<cons>(q_gen_6033, q_gen_6032) -> q_gen_6032
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6018
<nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6013
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
<s, z, s>(q_gen_6019) -> q_gen_6034
<z, z, z>() -> q_gen_6034
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<s, z>(q_gen_6011) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027, q_gen_6043, q_gen_6044},
Q_f={q_gen_6008},
Delta=
{
<cons>(q_gen_6044, q_gen_6043) -> q_gen_6043
<nil>() -> q_gen_6043
<z>() -> q_gen_6044
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<cons, nil>(q_gen_6044, q_gen_6043) -> q_gen_6008
<nil, cons>(q_gen_6044, q_gen_6043) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<s, s>(q_gen_6027) -> q_gen_6027
<z, z>() -> q_gen_6027
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13
() -> length([nil, z]) -> 13
() -> leq([z, s(nn2)]) -> 13
() -> leq([z, z]) -> 13
() -> reverse([nil, nil]) -> 13
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 18
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 16
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 15
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 13
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 13
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 13
(leq([s(nn1), z])) -> BOT -> 16
}
Sat witness: Found: ((leq([s(nn1), z])) -> BOT, {
nn1 -> z
})

-------------------------------------------
Step 22, which took 0.013075 s (model generation: 0.011944,  model checking: 0.001131):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019, q_gen_6032, q_gen_6033, q_gen_6034},
Q_f={q_gen_6013},
Delta=
{
<cons>(q_gen_6033, q_gen_6032) -> q_gen_6032
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6018
<nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6013
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
<s, z, s>(q_gen_6019) -> q_gen_6034
<z, z, z>() -> q_gen_6034
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011, q_gen_6058},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
<s, z>(q_gen_6011) -> q_gen_6058
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027, q_gen_6042, q_gen_6043, q_gen_6044},
Q_f={q_gen_6008},
Delta=
{
<cons>(q_gen_6044, q_gen_6043) -> q_gen_6043
<nil>() -> q_gen_6043
<z>() -> q_gen_6044
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<cons, cons>(q_gen_6027, q_gen_6042) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<s, s>(q_gen_6027) -> q_gen_6027
<z, z>() -> q_gen_6027
<cons, nil>(q_gen_6044, q_gen_6043) -> q_gen_6042
<nil, cons>(q_gen_6044, q_gen_6043) -> q_gen_6042
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14
() -> length([nil, z]) -> 14
() -> leq([z, s(nn2)]) -> 14
() -> leq([z, z]) -> 14
() -> reverse([nil, nil]) -> 14
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 18
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 16
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 18
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 14
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 14
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14
(leq([s(nn1), z])) -> BOT -> 16
}
Sat witness: Found: ((length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]), {
_afa -> cons(z, nil)  ;  _bfa -> s(z)  ;  _zea -> s(s(z))  ;  l1 -> cons(z, cons(z, nil))
})

-------------------------------------------
Step 23, which took 0.012370 s (model generation: 0.012101,  model checking: 0.000269):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019, q_gen_6032, q_gen_6033, q_gen_6034},
Q_f={q_gen_6013},
Delta=
{
<cons>(q_gen_6033, q_gen_6032) -> q_gen_6032
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6018
<nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6013
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
<s, z, s>(q_gen_6019) -> q_gen_6034
<z, z, z>() -> q_gen_6034
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011, q_gen_6058},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<s, s>(q_gen_6058) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
<s, z>(q_gen_6011) -> q_gen_6058
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027, q_gen_6042, q_gen_6043, q_gen_6044},
Q_f={q_gen_6008},
Delta=
{
<cons>(q_gen_6044, q_gen_6043) -> q_gen_6043
<nil>() -> q_gen_6043
<z>() -> q_gen_6044
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<cons, cons>(q_gen_6027, q_gen_6042) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<s, s>(q_gen_6027) -> q_gen_6027
<z, z>() -> q_gen_6027
<cons, nil>(q_gen_6044, q_gen_6043) -> q_gen_6042
<nil, cons>(q_gen_6044, q_gen_6043) -> q_gen_6042
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14
() -> length([nil, z]) -> 14
() -> leq([z, s(nn2)]) -> 14
() -> leq([z, z]) -> 14
() -> reverse([nil, nil]) -> 14
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 18
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 16
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 18
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 14
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 14
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 17
(leq([s(nn1), z])) -> BOT -> 16
}
Sat witness: Found: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(z)  ;  nn2 -> z
})

-------------------------------------------
Step 24, which took 0.030364 s (model generation: 0.026982,  model checking: 0.003382):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019, q_gen_6031, q_gen_6032, q_gen_6033, q_gen_6034},
Q_f={q_gen_6013},
Delta=
{
<cons>(q_gen_6033, q_gen_6032) -> q_gen_6032
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6018
<nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<cons, cons, cons>(q_gen_6034, q_gen_6031) -> q_gen_6013
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6031
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6031
<s, z, s>(q_gen_6019) -> q_gen_6034
<z, z, z>() -> q_gen_6034
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011, q_gen_6058},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
<s, s>(q_gen_6058) -> q_gen_6058
<s, z>(q_gen_6011) -> q_gen_6058
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027, q_gen_6043, q_gen_6044, q_gen_6056},
Q_f={q_gen_6008},
Delta=
{
<cons>(q_gen_6044, q_gen_6043) -> q_gen_6043
<nil>() -> q_gen_6043
<z>() -> q_gen_6044
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<nil, cons>(q_gen_6044, q_gen_6043) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<s, s>(q_gen_6027) -> q_gen_6027
<z, z>() -> q_gen_6027
<cons, cons>(q_gen_6027, q_gen_6056) -> q_gen_6056
<cons, nil>(q_gen_6044, q_gen_6043) -> q_gen_6056
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15
() -> length([nil, z]) -> 15
() -> leq([z, s(nn2)]) -> 15
() -> leq([z, z]) -> 15
() -> reverse([nil, nil]) -> 15
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 18
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 19
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 18
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 15
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 15
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 17
(leq([s(nn1), z])) -> BOT -> 17
}
Sat witness: Found: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), {
_lea -> cons(z, cons(z, nil))  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 25, which took 0.024490 s (model generation: 0.022859,  model checking: 0.001631):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019, q_gen_6024, q_gen_6025, q_gen_6032, q_gen_6033, q_gen_6034},
Q_f={q_gen_6013},
Delta=
{
<cons>(q_gen_6033, q_gen_6032) -> q_gen_6032
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<cons, cons>(q_gen_6024, q_gen_6018) -> q_gen_6018
<nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<z, z>() -> q_gen_6019
<s, s>(q_gen_6019) -> q_gen_6024
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6024, q_gen_6018) -> q_gen_6013
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6025
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6025
<s, z, s>(q_gen_6019) -> q_gen_6034
<z, z, z>() -> q_gen_6034
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011, q_gen_6058},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
<s, s>(q_gen_6058) -> q_gen_6058
<s, z>(q_gen_6011) -> q_gen_6058
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027, q_gen_6043, q_gen_6044, q_gen_6056},
Q_f={q_gen_6008},
Delta=
{
<cons>(q_gen_6044, q_gen_6043) -> q_gen_6043
<nil>() -> q_gen_6043
<z>() -> q_gen_6044
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<nil, cons>(q_gen_6044, q_gen_6043) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<s, s>(q_gen_6027) -> q_gen_6027
<z, z>() -> q_gen_6027
<cons, cons>(q_gen_6027, q_gen_6056) -> q_gen_6056
<cons, nil>(q_gen_6044, q_gen_6043) -> q_gen_6056
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18
() -> length([nil, z]) -> 16
() -> leq([z, s(nn2)]) -> 16
() -> leq([z, z]) -> 16
() -> reverse([nil, nil]) -> 16
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 18
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 19
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 18
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 16
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 16
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 17
(leq([s(nn1), z])) -> BOT -> 17
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(z, nil)
})

-------------------------------------------
Step 26, which took 0.018918 s (model generation: 0.016592,  model checking: 0.002326):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6017, q_gen_6018, q_gen_6019, q_gen_6032, q_gen_6033, q_gen_6034, q_gen_6055},
Q_f={q_gen_6013, q_gen_6017},
Delta=
{
<cons>(q_gen_6033, q_gen_6032) -> q_gen_6032
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6018
<nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<cons, cons, cons>(q_gen_6034, q_gen_6017) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6017
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6017
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6017
<s, z, s>(q_gen_6019) -> q_gen_6034
<z, z, z>() -> q_gen_6034
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6055
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011, q_gen_6058},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
<s, s>(q_gen_6058) -> q_gen_6058
<s, z>(q_gen_6011) -> q_gen_6058
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027, q_gen_6043, q_gen_6044, q_gen_6056},
Q_f={q_gen_6008},
Delta=
{
<cons>(q_gen_6044, q_gen_6043) -> q_gen_6043
<nil>() -> q_gen_6043
<z>() -> q_gen_6044
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<nil, cons>(q_gen_6044, q_gen_6043) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<s, s>(q_gen_6027) -> q_gen_6027
<z, z>() -> q_gen_6027
<cons, cons>(q_gen_6027, q_gen_6056) -> q_gen_6056
<cons, nil>(q_gen_6044, q_gen_6043) -> q_gen_6056
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18
() -> length([nil, z]) -> 17
() -> leq([z, s(nn2)]) -> 17
() -> leq([z, z]) -> 17
() -> reverse([nil, nil]) -> 17
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 21
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 19
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 19
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 17
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 17
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 18
(leq([s(nn1), z])) -> BOT -> 18
}
Sat witness: Found: ((append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]), {
_qea -> cons(z, cons(z, nil))  ;  _rea -> cons(z, cons(z, nil))  ;  h1 -> z  ;  t1 -> cons(z, cons(z, nil))
})

-------------------------------------------
Step 27, which took 0.043017 s (model generation: 0.038614,  model checking: 0.004403):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019, q_gen_6031, q_gen_6032, q_gen_6033, q_gen_6034, q_gen_6039},
Q_f={q_gen_6013},
Delta=
{
<cons>(q_gen_6033, q_gen_6032) -> q_gen_6032
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6039
<cons, cons, cons>(q_gen_6034, q_gen_6031) -> q_gen_6013
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6031
<cons, nil, cons>(q_gen_6019, q_gen_6039) -> q_gen_6031
<nil, cons, cons>(q_gen_6019, q_gen_6039) -> q_gen_6031
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6031
<s, z, s>(q_gen_6019) -> q_gen_6034
<z, z, z>() -> q_gen_6034
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011, q_gen_6058},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
<s, s>(q_gen_6058) -> q_gen_6058
<s, z>(q_gen_6011) -> q_gen_6058
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027, q_gen_6041, q_gen_6043, q_gen_6044},
Q_f={q_gen_6008},
Delta=
{
<cons>(q_gen_6044, q_gen_6043) -> q_gen_6043
<nil>() -> q_gen_6043
<z>() -> q_gen_6044
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<s, s>(q_gen_6027) -> q_gen_6027
<z, z>() -> q_gen_6027
<cons, cons>(q_gen_6027, q_gen_6041) -> q_gen_6041
<cons, nil>(q_gen_6044, q_gen_6043) -> q_gen_6041
<nil, cons>(q_gen_6044, q_gen_6043) -> q_gen_6041
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19
() -> length([nil, z]) -> 18
() -> leq([z, s(nn2)]) -> 18
() -> leq([z, z]) -> 18
() -> reverse([nil, nil]) -> 18
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 21
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 22
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 20
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 18
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 18
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 19
(leq([s(nn1), z])) -> BOT -> 19
}
Sat witness: Found: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), {
_lea -> cons(z, cons(z, cons(z, nil)))  ;  h1 -> s(z)  ;  l2 -> cons(z, cons(z, nil))  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 28, which took 0.042455 s (model generation: 0.040709,  model checking: 0.001746):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019, q_gen_6023, q_gen_6031, q_gen_6032, q_gen_6033, q_gen_6034},
Q_f={q_gen_6013},
Delta=
{
<cons>(q_gen_6033, q_gen_6032) -> q_gen_6032
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6023
<nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6023
<cons, cons, cons>(q_gen_6034, q_gen_6031) -> q_gen_6013
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6023) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6031
<cons, nil, cons>(q_gen_6019, q_gen_6023) -> q_gen_6031
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6031
<s, z, s>(q_gen_6019) -> q_gen_6034
<z, z, z>() -> q_gen_6034
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011, q_gen_6058},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
<s, s>(q_gen_6058) -> q_gen_6058
<s, z>(q_gen_6011) -> q_gen_6058
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027, q_gen_6043, q_gen_6044, q_gen_6056},
Q_f={q_gen_6008},
Delta=
{
<cons>(q_gen_6044, q_gen_6043) -> q_gen_6043
<nil>() -> q_gen_6043
<z>() -> q_gen_6044
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<nil, cons>(q_gen_6044, q_gen_6043) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<s, s>(q_gen_6027) -> q_gen_6027
<z, z>() -> q_gen_6027
<cons, cons>(q_gen_6027, q_gen_6056) -> q_gen_6056
<cons, nil>(q_gen_6044, q_gen_6043) -> q_gen_6056
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22
() -> length([nil, z]) -> 19
() -> leq([z, s(nn2)]) -> 19
() -> leq([z, z]) -> 19
() -> reverse([nil, nil]) -> 19
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 21
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 22
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 20
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 19
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 19
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 20
(leq([s(nn1), z])) -> BOT -> 20
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(z, cons(z, cons(z, nil)))
})

-------------------------------------------
Step 29, which took 0.057369 s (model generation: 0.048505,  model checking: 0.008864):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019, q_gen_6031, q_gen_6032, q_gen_6033, q_gen_6034, q_gen_6039},
Q_f={q_gen_6013},
Delta=
{
<cons>(q_gen_6033, q_gen_6032) -> q_gen_6032
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6039
<cons, cons, cons>(q_gen_6034, q_gen_6031) -> q_gen_6013
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6039) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6031
<cons, nil, cons>(q_gen_6019, q_gen_6039) -> q_gen_6031
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6031
<s, z, s>(q_gen_6019) -> q_gen_6034
<z, z, z>() -> q_gen_6034
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011, q_gen_6058},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
<s, s>(q_gen_6058) -> q_gen_6058
<s, z>(q_gen_6011) -> q_gen_6058
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027, q_gen_6043, q_gen_6044, q_gen_6056},
Q_f={q_gen_6008},
Delta=
{
<cons>(q_gen_6044, q_gen_6043) -> q_gen_6043
<nil>() -> q_gen_6043
<z>() -> q_gen_6044
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<nil, cons>(q_gen_6044, q_gen_6043) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<s, s>(q_gen_6027) -> q_gen_6027
<z, z>() -> q_gen_6027
<cons, cons>(q_gen_6027, q_gen_6056) -> q_gen_6056
<cons, nil>(q_gen_6044, q_gen_6043) -> q_gen_6056
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22
() -> length([nil, z]) -> 20
() -> leq([z, s(nn2)]) -> 20
() -> leq([z, z]) -> 20
() -> reverse([nil, nil]) -> 20
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 24
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 22
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 21
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 20
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 20
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 21
(leq([s(nn1), z])) -> BOT -> 21
}
Sat witness: Found: ((append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]), {
_qea -> cons(s(z), nil)  ;  _rea -> cons(s(z), cons(z, nil))  ;  h1 -> z  ;  t1 -> cons(s(z), nil)
})

-------------------------------------------
Step 30, which took 0.053644 s (model generation: 0.050912,  model checking: 0.002732):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019, q_gen_6031, q_gen_6032, q_gen_6033, q_gen_6034, q_gen_6039},
Q_f={q_gen_6013},
Delta=
{
<cons>(q_gen_6033, q_gen_6032) -> q_gen_6032
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6039
<cons, cons, cons>(q_gen_6034, q_gen_6031) -> q_gen_6013
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6039) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6031
<cons, nil, cons>(q_gen_6019, q_gen_6039) -> q_gen_6031
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6031
<s, z, s>(q_gen_6019) -> q_gen_6034
<z, z, z>() -> q_gen_6034
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011, q_gen_6058},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
<s, s>(q_gen_6058) -> q_gen_6058
<s, z>(q_gen_6011) -> q_gen_6058
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027, q_gen_6043, q_gen_6044, q_gen_6056},
Q_f={q_gen_6008},
Delta=
{
<cons>(q_gen_6044, q_gen_6043) -> q_gen_6043
<nil>() -> q_gen_6043
<z>() -> q_gen_6044
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<nil, cons>(q_gen_6044, q_gen_6043) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<s, s>(q_gen_6027) -> q_gen_6027
<s, z>(q_gen_6044) -> q_gen_6027
<z, s>(q_gen_6044) -> q_gen_6027
<z, z>() -> q_gen_6027
<cons, cons>(q_gen_6027, q_gen_6056) -> q_gen_6056
<cons, nil>(q_gen_6044, q_gen_6043) -> q_gen_6056
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22
() -> length([nil, z]) -> 21
() -> leq([z, s(nn2)]) -> 21
() -> leq([z, z]) -> 21
() -> reverse([nil, nil]) -> 21
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 24
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 25
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 22
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 21
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 21
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 22
(leq([s(nn1), z])) -> BOT -> 22
}
Sat witness: Found: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), {
_lea -> cons(z, cons(z, nil))  ;  h1 -> s(z)  ;  l2 -> cons(z, cons(z, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 31, which took 0.056139 s (model generation: 0.055711,  model checking: 0.000428):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019, q_gen_6032, q_gen_6033, q_gen_6034},
Q_f={q_gen_6013},
Delta=
{
<cons>(q_gen_6033, q_gen_6032) -> q_gen_6032
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6018
<nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6013
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
<s, z, s>(q_gen_6019) -> q_gen_6034
<z, z, z>() -> q_gen_6034
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6015, q_gen_6016, q_gen_6059},
Q_f={q_gen_6012, q_gen_6015},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<nil, z>() -> q_gen_6012
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6015
<cons, s>(q_gen_6016, q_gen_6015) -> q_gen_6059
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011, q_gen_6058},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
<s, s>(q_gen_6058) -> q_gen_6058
<s, z>(q_gen_6011) -> q_gen_6058
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027, q_gen_6043, q_gen_6044, q_gen_6057},
Q_f={q_gen_6008},
Delta=
{
<cons>(q_gen_6044, q_gen_6043) -> q_gen_6043
<nil>() -> q_gen_6043
<z>() -> q_gen_6044
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<cons, cons>(q_gen_6027, q_gen_6057) -> q_gen_6008
<nil, cons>(q_gen_6044, q_gen_6043) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<s, s>(q_gen_6027) -> q_gen_6027
<s, z>(q_gen_6044) -> q_gen_6027
<z, s>(q_gen_6044) -> q_gen_6027
<z, z>() -> q_gen_6027
<cons, nil>(q_gen_6044, q_gen_6043) -> q_gen_6057
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22
() -> length([nil, z]) -> 21
() -> leq([z, s(nn2)]) -> 21
() -> leq([z, z]) -> 21
() -> reverse([nil, nil]) -> 21
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 24
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 25
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 22
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 24
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 22
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 22
(leq([s(nn1), z])) -> BOT -> 22
}
Sat witness: Found: ((length([ll, _vea])) -> length([cons(x, ll), s(_vea)]), {
_vea -> s(z)  ;  ll -> cons(z, nil)  ;  x -> z
})

-------------------------------------------
Step 32, which took 0.063587 s (model generation: 0.062133,  model checking: 0.001454):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6017, q_gen_6018, q_gen_6019, q_gen_6032, q_gen_6033, q_gen_6034, q_gen_6055},
Q_f={q_gen_6013, q_gen_6017},
Delta=
{
<cons>(q_gen_6033, q_gen_6032) -> q_gen_6032
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6018
<nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<nil, nil, nil>() -> q_gen_6013
<cons, cons, cons>(q_gen_6034, q_gen_6017) -> q_gen_6017
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6017
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6017
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6017
<s, z, s>(q_gen_6019) -> q_gen_6034
<z, z, z>() -> q_gen_6034
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6055
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011, q_gen_6058},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
<s, s>(q_gen_6058) -> q_gen_6058
<s, z>(q_gen_6011) -> q_gen_6058
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027, q_gen_6042, q_gen_6043, q_gen_6044, q_gen_6057},
Q_f={q_gen_6008},
Delta=
{
<cons>(q_gen_6044, q_gen_6043) -> q_gen_6043
<nil>() -> q_gen_6043
<z>() -> q_gen_6044
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<cons, cons>(q_gen_6027, q_gen_6042) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<s, s>(q_gen_6027) -> q_gen_6027
<s, z>(q_gen_6044) -> q_gen_6027
<z, s>(q_gen_6044) -> q_gen_6027
<z, z>() -> q_gen_6027
<cons, cons>(q_gen_6027, q_gen_6057) -> q_gen_6042
<nil, cons>(q_gen_6044, q_gen_6043) -> q_gen_6042
<cons, nil>(q_gen_6044, q_gen_6043) -> q_gen_6057
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22
() -> length([nil, z]) -> 22
() -> leq([z, s(nn2)]) -> 22
() -> leq([z, z]) -> 22
() -> reverse([nil, nil]) -> 22
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 24
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 25
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 25
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 24
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 23
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 23
(leq([s(nn1), z])) -> BOT -> 23
}
Sat witness: Found: ((length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]), {
_afa -> cons(z, cons(z, nil))  ;  _bfa -> s(s(z))  ;  _zea -> s(s(s(z)))  ;  l1 -> cons(z, cons(z, cons(z, nil)))
})

-------------------------------------------
Step 33, which took 0.068141 s (model generation: 0.065362,  model checking: 0.002779):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019, q_gen_6022, q_gen_6032, q_gen_6033, q_gen_6034, q_gen_6039, q_gen_6040},
Q_f={q_gen_6013, q_gen_6022},
Delta=
{
<cons>(q_gen_6033, q_gen_6032) -> q_gen_6032
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6039
<cons, cons, cons>(q_gen_6034, q_gen_6040) -> q_gen_6013
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
<cons, cons, cons>(q_gen_6034, q_gen_6022) -> q_gen_6022
<cons, nil, cons>(q_gen_6019, q_gen_6039) -> q_gen_6022
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6022
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6022
<s, z, s>(q_gen_6019) -> q_gen_6034
<z, z, z>() -> q_gen_6034
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6040
<nil, cons, cons>(q_gen_6019, q_gen_6039) -> q_gen_6040
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011, q_gen_6058},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
<s, s>(q_gen_6058) -> q_gen_6058
<s, z>(q_gen_6011) -> q_gen_6058
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027, q_gen_6041, q_gen_6043, q_gen_6044},
Q_f={q_gen_6008},
Delta=
{
<cons>(q_gen_6044, q_gen_6043) -> q_gen_6043
<nil>() -> q_gen_6043
<z>() -> q_gen_6044
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<s, s>(q_gen_6027) -> q_gen_6027
<s, z>(q_gen_6044) -> q_gen_6027
<z, s>(q_gen_6044) -> q_gen_6027
<z, z>() -> q_gen_6027
<cons, cons>(q_gen_6027, q_gen_6041) -> q_gen_6041
<cons, nil>(q_gen_6044, q_gen_6043) -> q_gen_6041
<nil, cons>(q_gen_6044, q_gen_6043) -> q_gen_6041
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 23
() -> length([nil, z]) -> 23
() -> leq([z, s(nn2)]) -> 23
() -> leq([z, z]) -> 23
() -> reverse([nil, nil]) -> 23
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 27
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 25
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 25
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 25
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 24
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 24
(leq([s(nn1), z])) -> BOT -> 24
}
Sat witness: Found: ((append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]), {
_qea -> cons(z, nil)  ;  _rea -> cons(z, cons(z, cons(z, nil)))  ;  h1 -> z  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 34, which took 0.070233 s (model generation: 0.066568,  model checking: 0.003665):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019, q_gen_6022, q_gen_6023, q_gen_6031, q_gen_6032, q_gen_6033, q_gen_6034},
Q_f={q_gen_6013, q_gen_6022},
Delta=
{
<cons>(q_gen_6033, q_gen_6032) -> q_gen_6032
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<cons, cons>(q_gen_6019, q_gen_6023) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6023
<nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6023
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
<cons, cons, cons>(q_gen_6034, q_gen_6022) -> q_gen_6022
<cons, cons, cons>(q_gen_6034, q_gen_6031) -> q_gen_6022
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6022
<nil, cons, cons>(q_gen_6019, q_gen_6023) -> q_gen_6022
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6031
<cons, nil, cons>(q_gen_6019, q_gen_6023) -> q_gen_6031
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6031
<s, z, s>(q_gen_6019) -> q_gen_6034
<z, z, z>() -> q_gen_6034
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011, q_gen_6058},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
<s, s>(q_gen_6058) -> q_gen_6058
<s, z>(q_gen_6011) -> q_gen_6058
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027, q_gen_6043, q_gen_6044, q_gen_6056},
Q_f={q_gen_6008},
Delta=
{
<cons>(q_gen_6044, q_gen_6043) -> q_gen_6043
<nil>() -> q_gen_6043
<z>() -> q_gen_6044
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<nil, cons>(q_gen_6044, q_gen_6043) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<s, s>(q_gen_6027) -> q_gen_6027
<s, z>(q_gen_6044) -> q_gen_6027
<z, s>(q_gen_6044) -> q_gen_6027
<z, z>() -> q_gen_6027
<cons, cons>(q_gen_6027, q_gen_6056) -> q_gen_6056
<cons, nil>(q_gen_6044, q_gen_6043) -> q_gen_6056
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 24
() -> length([nil, z]) -> 24
() -> leq([z, s(nn2)]) -> 24
() -> leq([z, z]) -> 24
() -> reverse([nil, nil]) -> 24
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 27
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 28
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 26
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 26
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 25
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 25
(leq([s(nn1), z])) -> BOT -> 25
}
Sat witness: Found: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), {
_lea -> cons(z, cons(z, cons(z, nil)))  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> cons(z, cons(z, cons(z, nil)))
})

-------------------------------------------
Step 35, which took 0.113597 s (model generation: 0.110547,  model checking: 0.003050):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019, q_gen_6022, q_gen_6023, q_gen_6032, q_gen_6033, q_gen_6034, q_gen_6055},
Q_f={q_gen_6013, q_gen_6022},
Delta=
{
<cons>(q_gen_6033, q_gen_6032) -> q_gen_6032
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6023
<cons, cons>(q_gen_6019, q_gen_6023) -> q_gen_6023
<nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6023
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
<cons, cons, cons>(q_gen_6034, q_gen_6022) -> q_gen_6022
<cons, nil, cons>(q_gen_6019, q_gen_6023) -> q_gen_6022
<nil, cons, cons>(q_gen_6019, q_gen_6023) -> q_gen_6022
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6022
<s, z, s>(q_gen_6019) -> q_gen_6034
<z, z, z>() -> q_gen_6034
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6055
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011, q_gen_6058},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
<s, s>(q_gen_6058) -> q_gen_6058
<s, z>(q_gen_6011) -> q_gen_6058
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027, q_gen_6043, q_gen_6044, q_gen_6056},
Q_f={q_gen_6008},
Delta=
{
<cons>(q_gen_6044, q_gen_6043) -> q_gen_6043
<nil>() -> q_gen_6043
<z>() -> q_gen_6044
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<nil, cons>(q_gen_6044, q_gen_6043) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<s, s>(q_gen_6027) -> q_gen_6027
<s, z>(q_gen_6044) -> q_gen_6027
<z, s>(q_gen_6044) -> q_gen_6027
<z, z>() -> q_gen_6027
<cons, cons>(q_gen_6027, q_gen_6056) -> q_gen_6056
<cons, nil>(q_gen_6044, q_gen_6043) -> q_gen_6056
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 25
() -> length([nil, z]) -> 25
() -> leq([z, s(nn2)]) -> 25
() -> leq([z, z]) -> 25
() -> reverse([nil, nil]) -> 25
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 30
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 28
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 27
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 27
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 26
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 26
(leq([s(nn1), z])) -> BOT -> 26
}
Sat witness: Found: ((append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]), {
_qea -> cons(z, cons(s(z), cons(z, nil)))  ;  _rea -> cons(z, cons(s(z), cons(z, nil)))  ;  h1 -> z  ;  t1 -> cons(s(z), cons(z, cons(z, nil)))
})

-------------------------------------------
Step 36, which took 0.106157 s (model generation: 0.104655,  model checking: 0.001502):

Model:
|_
{
append -> 
{{{
Q={q_gen_6013, q_gen_6018, q_gen_6019, q_gen_6030, q_gen_6032, q_gen_6033, q_gen_6034, q_gen_6039, q_gen_6055},
Q_f={q_gen_6013, q_gen_6030},
Delta=
{
<cons>(q_gen_6033, q_gen_6032) -> q_gen_6032
<nil>() -> q_gen_6032
<z>() -> q_gen_6033
<cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6018
<nil, nil>() -> q_gen_6018
<s, s>(q_gen_6019) -> q_gen_6019
<z, z>() -> q_gen_6019
<nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6039
<cons, nil, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, cons, cons>(q_gen_6019, q_gen_6018) -> q_gen_6013
<nil, nil, nil>() -> q_gen_6013
<cons, cons, cons>(q_gen_6034, q_gen_6030) -> q_gen_6030
<cons, nil, cons>(q_gen_6019, q_gen_6039) -> q_gen_6030
<nil, cons, cons>(q_gen_6019, q_gen_6039) -> q_gen_6030
<nil, nil, cons>(q_gen_6033, q_gen_6032) -> q_gen_6030
<s, z, s>(q_gen_6019) -> q_gen_6034
<z, z, z>() -> q_gen_6034
<cons, cons, cons>(q_gen_6034, q_gen_6013) -> q_gen_6055
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6012, q_gen_6016},
Q_f={q_gen_6012},
Delta=
{
<s>(q_gen_6016) -> q_gen_6016
<z>() -> q_gen_6016
<cons, s>(q_gen_6016, q_gen_6012) -> q_gen_6012
<nil, z>() -> q_gen_6012
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_6009, q_gen_6011, q_gen_6058},
Q_f={q_gen_6009},
Delta=
{
<s>(q_gen_6011) -> q_gen_6011
<z>() -> q_gen_6011
<s, s>(q_gen_6009) -> q_gen_6009
<z, s>(q_gen_6011) -> q_gen_6009
<z, z>() -> q_gen_6009
<s, s>(q_gen_6058) -> q_gen_6058
<s, z>(q_gen_6011) -> q_gen_6058
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6008, q_gen_6027, q_gen_6043, q_gen_6044, q_gen_6056},
Q_f={q_gen_6008},
Delta=
{
<cons>(q_gen_6044, q_gen_6043) -> q_gen_6043
<nil>() -> q_gen_6043
<z>() -> q_gen_6044
<cons, cons>(q_gen_6027, q_gen_6008) -> q_gen_6008
<nil, cons>(q_gen_6044, q_gen_6043) -> q_gen_6008
<nil, nil>() -> q_gen_6008
<s, s>(q_gen_6027) -> q_gen_6027
<s, z>(q_gen_6044) -> q_gen_6027
<z, s>(q_gen_6044) -> q_gen_6027
<z, z>() -> q_gen_6027
<cons, cons>(q_gen_6027, q_gen_6056) -> q_gen_6056
<cons, nil>(q_gen_6044, q_gen_6043) -> q_gen_6056
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 26
() -> length([nil, z]) -> 26
() -> leq([z, s(nn2)]) -> 26
() -> leq([z, z]) -> 26
() -> reverse([nil, nil]) -> 26
(append([_qea, cons(h1, nil), _rea]) /\ reverse([t1, _qea])) -> reverse([cons(h1, t1), _rea]) -> 30
(append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]) -> 31
(length([_afa, _bfa]) /\ length([l1, _zea]) /\ reverse([l1, _afa])) -> leq([_zea, _bfa]) -> 28
(length([ll, _vea])) -> length([cons(x, ll), s(_vea)]) -> 28
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 27
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 27
(leq([s(nn1), z])) -> BOT -> 27
}
Sat witness: Found: ((append([t1, l2, _lea])) -> append([cons(h1, t1), l2, cons(h1, _lea)]), {
_lea -> cons(z, cons(z, nil))  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> cons(z, nil)
})

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