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


Learning problem is:

env: {
nat -> {s, z}
}
definition:
{
(plus, F:
{() -> plus([n, z, n])
(plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)])}
(plus([_kk, _lk, _mk]) /\ plus([_kk, _lk, _nk])) -> eq_nat([_mk, _nk])
)
(le, P:
{() -> le([z, s(nn2)])
(le([nn1, nn2])) -> le([s(nn1), s(nn2)])
(le([s(nn1), s(nn2)])) -> le([nn1, nn2])
(le([s(nn1), z])) -> BOT
(le([z, z])) -> BOT}
)
}

properties:
{(plus([n, s(m), _ok])) -> le([n, _ok])}


over-approximation: {plus}
under-approximation: {le}

Clause system for inference is:

{
() -> le([z, s(nn2)]) -> 0
() -> plus([n, z, n]) -> 0
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 0
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 0
(le([s(nn1), z])) -> BOT -> 0
(le([z, z])) -> BOT -> 0
(plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]) -> 0
(plus([n, s(m), _ok])) -> le([n, _ok]) -> 0
}


Solving took 0.283084 seconds.
Proved
Model:
|_
{
le -> 
{{{
Q={q_gen_2377, q_gen_2378, q_gen_2392},
Q_f={q_gen_2377},
Delta=
{
<s>(q_gen_2378) -> q_gen_2378
<z>() -> q_gen_2378
<s, s>(q_gen_2377) -> q_gen_2377
<z, s>(q_gen_2378) -> q_gen_2377
<s, s>(q_gen_2392) -> q_gen_2392
<z, z>() -> q_gen_2392
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2376, q_gen_2379, q_gen_2380, q_gen_2390, q_gen_2391, q_gen_2396},
Q_f={q_gen_2376, q_gen_2379},
Delta=
{
<s>(q_gen_2390) -> q_gen_2390
<z>() -> q_gen_2390
<s, s>(q_gen_2380) -> q_gen_2380
<z, z>() -> q_gen_2380
<s, s>(q_gen_2396) -> q_gen_2396
<z, s>(q_gen_2390) -> q_gen_2396
<s, z, s>(q_gen_2380) -> q_gen_2376
<z, z, z>() -> q_gen_2376
<s, s, s>(q_gen_2379) -> q_gen_2379
<s, z, s>(q_gen_2396) -> q_gen_2379
<z, s, s>(q_gen_2380) -> q_gen_2379
<z, s, s>(q_gen_2396) -> q_gen_2379
<z, z, s>(q_gen_2390) -> q_gen_2379
<s, s, s>(q_gen_2376) -> q_gen_2391
<s, s, s>(q_gen_2391) -> q_gen_2391
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005076 s (model generation: 0.004523,  model checking: 0.000553):

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 0
() -> plus([n, z, n]) -> 3
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 1
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 1
(le([s(nn1), z])) -> BOT -> 1
(le([z, z])) -> BOT -> 1
(plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]) -> 1
(plus([n, s(m), _ok])) -> le([n, _ok]) -> 1
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> z
})

-------------------------------------------
Step 1, which took 0.004344 s (model generation: 0.004277,  model checking: 0.000067):

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 3
() -> plus([n, z, n]) -> 3
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 1
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 1
(le([s(nn1), z])) -> BOT -> 1
(le([z, z])) -> BOT -> 1
(plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]) -> 1
(plus([n, s(m), _ok])) -> le([n, _ok]) -> 1
}
Sat witness: Found: (() -> le([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 2, which took 0.004948 s (model generation: 0.004724,  model checking: 0.000224):

Model:
|_
{
le -> 
{{{
Q={q_gen_2377, q_gen_2378},
Q_f={q_gen_2377},
Delta=
{
<z>() -> q_gen_2378
<z, s>(q_gen_2378) -> q_gen_2377
}

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

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 3
() -> plus([n, z, n]) -> 3
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 1
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 1
(le([s(nn1), z])) -> BOT -> 1
(le([z, z])) -> BOT -> 1
(plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]) -> 4
(plus([n, s(m), _ok])) -> le([n, _ok]) -> 2
}
Sat witness: Found: ((plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]), {
_jk -> z  ;  mm -> z  ;  n -> z
})

-------------------------------------------
Step 3, which took 0.005086 s (model generation: 0.004622,  model checking: 0.000464):

Model:
|_
{
le -> 
{{{
Q={q_gen_2377, q_gen_2378},
Q_f={q_gen_2377},
Delta=
{
<z>() -> q_gen_2378
<z, s>(q_gen_2378) -> q_gen_2377
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2376, q_gen_2380},
Q_f={q_gen_2376},
Delta=
{
<z, z>() -> q_gen_2380
<z, s, s>(q_gen_2380) -> q_gen_2376
<z, z, z>() -> q_gen_2376
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 3
() -> plus([n, z, n]) -> 3
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 2
(le([s(nn1), z])) -> BOT -> 2
(le([z, z])) -> BOT -> 2
(plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]) -> 4
(plus([n, s(m), _ok])) -> le([n, _ok]) -> 2
}
Sat witness: Found: ((le([nn1, nn2])) -> le([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> s(z)
})

-------------------------------------------
Step 4, which took 0.004117 s (model generation: 0.003909,  model checking: 0.000208):

Model:
|_
{
le -> 
{{{
Q={q_gen_2377, q_gen_2378},
Q_f={q_gen_2377},
Delta=
{
<z>() -> q_gen_2378
<s, s>(q_gen_2377) -> q_gen_2377
<z, s>(q_gen_2378) -> q_gen_2377
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2376, q_gen_2380},
Q_f={q_gen_2376},
Delta=
{
<z, z>() -> q_gen_2380
<z, s, s>(q_gen_2380) -> q_gen_2376
<z, z, z>() -> q_gen_2376
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 3
() -> plus([n, z, n]) -> 6
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 3
(le([s(nn1), z])) -> BOT -> 3
(le([z, z])) -> BOT -> 3
(plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]) -> 4
(plus([n, s(m), _ok])) -> le([n, _ok]) -> 3
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(s(z))
})

-------------------------------------------
Step 5, which took 0.005495 s (model generation: 0.005395,  model checking: 0.000100):

Model:
|_
{
le -> 
{{{
Q={q_gen_2377, q_gen_2378},
Q_f={q_gen_2377},
Delta=
{
<z>() -> q_gen_2378
<s, s>(q_gen_2377) -> q_gen_2377
<z, s>(q_gen_2378) -> q_gen_2377
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2376, q_gen_2380},
Q_f={q_gen_2376},
Delta=
{
<s, s>(q_gen_2380) -> q_gen_2380
<z, z>() -> q_gen_2380
<s, z, s>(q_gen_2380) -> q_gen_2376
<z, s, s>(q_gen_2380) -> q_gen_2376
<z, z, z>() -> q_gen_2376
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 3
() -> plus([n, z, n]) -> 6
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 3
(le([s(nn1), z])) -> BOT -> 3
(le([z, z])) -> BOT -> 3
(plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]) -> 4
(plus([n, s(m), _ok])) -> le([n, _ok]) -> 6
}
Sat witness: Found: ((plus([n, s(m), _ok])) -> le([n, _ok]), {
_ok -> s(s(z))  ;  m -> s(z)  ;  n -> z
})

-------------------------------------------
Step 6, which took 0.007957 s (model generation: 0.007459,  model checking: 0.000498):

Model:
|_
{
le -> 
{{{
Q={q_gen_2377, q_gen_2378},
Q_f={q_gen_2377},
Delta=
{
<s>(q_gen_2378) -> q_gen_2378
<z>() -> q_gen_2378
<s, s>(q_gen_2377) -> q_gen_2377
<z, s>(q_gen_2378) -> q_gen_2377
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2376, q_gen_2380},
Q_f={q_gen_2376},
Delta=
{
<s, s>(q_gen_2380) -> q_gen_2380
<z, z>() -> q_gen_2380
<s, z, s>(q_gen_2380) -> q_gen_2376
<z, s, s>(q_gen_2380) -> q_gen_2376
<z, z, z>() -> q_gen_2376
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 4
() -> plus([n, z, n]) -> 6
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 4
(le([s(nn1), z])) -> BOT -> 4
(le([z, z])) -> BOT -> 4
(plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]) -> 7
(plus([n, s(m), _ok])) -> le([n, _ok]) -> 6
}
Sat witness: Found: ((plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]), {
_jk -> s(z)  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 7, which took 0.011438 s (model generation: 0.011063,  model checking: 0.000375):

Model:
|_
{
le -> 
{{{
Q={q_gen_2377, q_gen_2378},
Q_f={q_gen_2377},
Delta=
{
<s>(q_gen_2378) -> q_gen_2378
<z>() -> q_gen_2378
<s, s>(q_gen_2377) -> q_gen_2377
<z, s>(q_gen_2378) -> q_gen_2377
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2376, q_gen_2380, q_gen_2390},
Q_f={q_gen_2376},
Delta=
{
<z>() -> q_gen_2390
<s, s>(q_gen_2380) -> q_gen_2380
<z, z>() -> q_gen_2380
<s, s, s>(q_gen_2376) -> q_gen_2376
<s, z, s>(q_gen_2380) -> q_gen_2376
<z, s, s>(q_gen_2380) -> q_gen_2376
<z, z, s>(q_gen_2390) -> q_gen_2376
<z, z, z>() -> q_gen_2376
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 5
() -> plus([n, z, n]) -> 6
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 5
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 5
(le([s(nn1), z])) -> BOT -> 5
(le([z, z])) -> BOT -> 5
(plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]) -> 7
(plus([n, s(m), _ok])) -> le([n, _ok]) -> 9
}
Sat witness: Found: ((plus([n, s(m), _ok])) -> le([n, _ok]), {
_ok -> s(z)  ;  m -> z  ;  n -> s(z)
})

-------------------------------------------
Step 8, which took 0.011763 s (model generation: 0.011725,  model checking: 0.000038):

Model:
|_
{
le -> 
{{{
Q={q_gen_2377, q_gen_2378},
Q_f={q_gen_2377},
Delta=
{
<s>(q_gen_2378) -> q_gen_2378
<z>() -> q_gen_2378
<s, s>(q_gen_2377) -> q_gen_2377
<z, s>(q_gen_2378) -> q_gen_2377
<z, z>() -> q_gen_2377
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2376, q_gen_2380, q_gen_2390},
Q_f={q_gen_2376},
Delta=
{
<z>() -> q_gen_2390
<s, s>(q_gen_2380) -> q_gen_2380
<z, z>() -> q_gen_2380
<s, s, s>(q_gen_2376) -> q_gen_2376
<s, z, s>(q_gen_2380) -> q_gen_2376
<z, s, s>(q_gen_2380) -> q_gen_2376
<z, z, s>(q_gen_2390) -> q_gen_2376
<z, z, z>() -> q_gen_2376
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 5
() -> plus([n, z, n]) -> 6
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 5
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 5
(le([s(nn1), z])) -> BOT -> 5
(le([z, z])) -> BOT -> 8
(plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]) -> 7
(plus([n, s(m), _ok])) -> le([n, _ok]) -> 9
}
Sat witness: Found: ((le([z, z])) -> BOT, {

})

-------------------------------------------
Step 9, which took 0.006091 s (model generation: 0.006007,  model checking: 0.000084):

Model:
|_
{
le -> 
{{{
Q={q_gen_2377, q_gen_2378, q_gen_2393},
Q_f={q_gen_2377},
Delta=
{
<s>(q_gen_2378) -> q_gen_2378
<z>() -> q_gen_2378
<s, s>(q_gen_2377) -> q_gen_2377
<s, s>(q_gen_2393) -> q_gen_2377
<z, s>(q_gen_2378) -> q_gen_2377
<z, z>() -> q_gen_2393
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2376, q_gen_2380, q_gen_2390},
Q_f={q_gen_2376},
Delta=
{
<z>() -> q_gen_2390
<s, s>(q_gen_2380) -> q_gen_2380
<z, z>() -> q_gen_2380
<s, s, s>(q_gen_2376) -> q_gen_2376
<s, z, s>(q_gen_2380) -> q_gen_2376
<z, s, s>(q_gen_2380) -> q_gen_2376
<z, z, s>(q_gen_2390) -> q_gen_2376
<z, z, z>() -> q_gen_2376
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 5
() -> plus([n, z, n]) -> 6
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 5
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 8
(le([s(nn1), z])) -> BOT -> 6
(le([z, z])) -> BOT -> 8
(plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]) -> 7
(plus([n, s(m), _ok])) -> le([n, _ok]) -> 9
}
Sat witness: Found: ((le([s(nn1), s(nn2)])) -> le([nn1, nn2]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 10, which took 0.013918 s (model generation: 0.012347,  model checking: 0.001571):

Model:
|_
{
le -> 
{{{
Q={q_gen_2377, q_gen_2378, q_gen_2392},
Q_f={q_gen_2377},
Delta=
{
<s>(q_gen_2378) -> q_gen_2378
<z>() -> q_gen_2378
<s, s>(q_gen_2377) -> q_gen_2377
<z, s>(q_gen_2378) -> q_gen_2377
<s, s>(q_gen_2392) -> q_gen_2392
<z, z>() -> q_gen_2392
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2376, q_gen_2380, q_gen_2389, q_gen_2390},
Q_f={q_gen_2376},
Delta=
{
<z>() -> q_gen_2390
<s, s>(q_gen_2380) -> q_gen_2380
<z, z>() -> q_gen_2380
<s, s, s>(q_gen_2389) -> q_gen_2376
<s, z, s>(q_gen_2380) -> q_gen_2376
<z, s, s>(q_gen_2380) -> q_gen_2376
<z, z, z>() -> q_gen_2376
<s, s, s>(q_gen_2376) -> q_gen_2389
<z, z, s>(q_gen_2390) -> q_gen_2389
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 6
() -> plus([n, z, n]) -> 7
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 6
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 8
(le([s(nn1), z])) -> BOT -> 7
(le([z, z])) -> BOT -> 8
(plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]) -> 10
(plus([n, s(m), _ok])) -> le([n, _ok]) -> 9
}
Sat witness: Found: ((plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]), {
_jk -> s(s(z))  ;  mm -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 11, which took 0.013095 s (model generation: 0.012662,  model checking: 0.000433):

Model:
|_
{
le -> 
{{{
Q={q_gen_2377, q_gen_2378, q_gen_2392},
Q_f={q_gen_2377},
Delta=
{
<s>(q_gen_2378) -> q_gen_2378
<z>() -> q_gen_2378
<s, s>(q_gen_2377) -> q_gen_2377
<z, s>(q_gen_2378) -> q_gen_2377
<s, s>(q_gen_2392) -> q_gen_2392
<z, z>() -> q_gen_2392
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2376, q_gen_2379, q_gen_2380, q_gen_2389, q_gen_2390},
Q_f={q_gen_2376, q_gen_2379},
Delta=
{
<z>() -> q_gen_2390
<s, s>(q_gen_2380) -> q_gen_2380
<z, s>(q_gen_2390) -> q_gen_2380
<z, z>() -> q_gen_2380
<z, z, z>() -> q_gen_2376
<s, s, s>(q_gen_2379) -> q_gen_2379
<s, s, s>(q_gen_2389) -> q_gen_2379
<s, z, s>(q_gen_2380) -> q_gen_2379
<z, s, s>(q_gen_2380) -> q_gen_2379
<s, s, s>(q_gen_2376) -> q_gen_2389
<z, z, s>(q_gen_2390) -> q_gen_2389
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 7
() -> plus([n, z, n]) -> 8
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 7
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 9
(le([s(nn1), z])) -> BOT -> 8
(le([z, z])) -> BOT -> 9
(plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]) -> 10
(plus([n, s(m), _ok])) -> le([n, _ok]) -> 12
}
Sat witness: Found: ((plus([n, s(m), _ok])) -> le([n, _ok]), {
_ok -> s(s(z))  ;  m -> s(z)  ;  n -> s(s(z))
})

-------------------------------------------
Step 12, which took 0.016808 s (model generation: 0.015634,  model checking: 0.001174):

Model:
|_
{
le -> 
{{{
Q={q_gen_2377, q_gen_2378, q_gen_2392},
Q_f={q_gen_2377},
Delta=
{
<s>(q_gen_2378) -> q_gen_2378
<z>() -> q_gen_2378
<s, s>(q_gen_2377) -> q_gen_2377
<z, s>(q_gen_2378) -> q_gen_2377
<s, s>(q_gen_2392) -> q_gen_2392
<z, z>() -> q_gen_2392
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2376, q_gen_2379, q_gen_2380, q_gen_2390, q_gen_2391},
Q_f={q_gen_2376, q_gen_2379},
Delta=
{
<z>() -> q_gen_2390
<s, s>(q_gen_2380) -> q_gen_2380
<z, s>(q_gen_2390) -> q_gen_2380
<z, z>() -> q_gen_2380
<z, z, z>() -> q_gen_2376
<s, s, s>(q_gen_2379) -> q_gen_2379
<s, z, s>(q_gen_2380) -> q_gen_2379
<z, s, s>(q_gen_2380) -> q_gen_2379
<z, z, s>(q_gen_2390) -> q_gen_2379
<s, s, s>(q_gen_2376) -> q_gen_2391
<s, s, s>(q_gen_2391) -> q_gen_2391
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 8
() -> plus([n, z, n]) -> 9
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 8
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 10
(le([s(nn1), z])) -> BOT -> 9
(le([z, z])) -> BOT -> 10
(plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]) -> 13
(plus([n, s(m), _ok])) -> le([n, _ok]) -> 12
}
Sat witness: Found: ((plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]), {
_jk -> s(s(z))  ;  mm -> z  ;  n -> s(z)
})

-------------------------------------------
Step 13, which took 0.020354 s (model generation: 0.019569,  model checking: 0.000785):

Model:
|_
{
le -> 
{{{
Q={q_gen_2377, q_gen_2378, q_gen_2392},
Q_f={q_gen_2377},
Delta=
{
<s>(q_gen_2378) -> q_gen_2378
<z>() -> q_gen_2378
<s, s>(q_gen_2377) -> q_gen_2377
<z, s>(q_gen_2378) -> q_gen_2377
<s, s>(q_gen_2392) -> q_gen_2392
<z, z>() -> q_gen_2392
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2376, q_gen_2379, q_gen_2380, q_gen_2390, q_gen_2391},
Q_f={q_gen_2376, q_gen_2379},
Delta=
{
<s>(q_gen_2390) -> q_gen_2390
<z>() -> q_gen_2390
<s, s>(q_gen_2380) -> q_gen_2380
<z, s>(q_gen_2390) -> q_gen_2380
<z, z>() -> q_gen_2380
<z, z, z>() -> q_gen_2376
<s, s, s>(q_gen_2379) -> q_gen_2379
<s, z, s>(q_gen_2380) -> q_gen_2379
<z, s, s>(q_gen_2380) -> q_gen_2379
<z, z, s>(q_gen_2390) -> q_gen_2379
<s, s, s>(q_gen_2376) -> q_gen_2391
<s, s, s>(q_gen_2391) -> q_gen_2391
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 9
() -> plus([n, z, n]) -> 10
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 9
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 11
(le([s(nn1), z])) -> BOT -> 10
(le([z, z])) -> BOT -> 11
(plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]) -> 13
(plus([n, s(m), _ok])) -> le([n, _ok]) -> 15
}
Sat witness: Found: ((plus([n, s(m), _ok])) -> le([n, _ok]), {
_ok -> s(s(z))  ;  m -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 14, which took 0.023110 s (model generation: 0.022057,  model checking: 0.001053):

Model:
|_
{
le -> 
{{{
Q={q_gen_2377, q_gen_2378, q_gen_2392},
Q_f={q_gen_2377},
Delta=
{
<s>(q_gen_2378) -> q_gen_2378
<z>() -> q_gen_2378
<s, s>(q_gen_2377) -> q_gen_2377
<z, s>(q_gen_2378) -> q_gen_2377
<s, s>(q_gen_2392) -> q_gen_2392
<z, z>() -> q_gen_2392
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2376, q_gen_2379, q_gen_2380, q_gen_2390, q_gen_2391},
Q_f={q_gen_2376, q_gen_2379},
Delta=
{
<s>(q_gen_2390) -> q_gen_2390
<z>() -> q_gen_2390
<s, s>(q_gen_2380) -> q_gen_2380
<z, s>(q_gen_2390) -> q_gen_2380
<z, z>() -> q_gen_2380
<s, s, s>(q_gen_2379) -> q_gen_2376
<s, z, s>(q_gen_2380) -> q_gen_2376
<z, z, z>() -> q_gen_2376
<z, s, s>(q_gen_2380) -> q_gen_2379
<z, z, s>(q_gen_2390) -> q_gen_2379
<s, s, s>(q_gen_2376) -> q_gen_2391
<s, s, s>(q_gen_2391) -> q_gen_2391
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 10
() -> plus([n, z, n]) -> 11
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 10
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 12
(le([s(nn1), z])) -> BOT -> 11
(le([z, z])) -> BOT -> 12
(plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]) -> 16
(plus([n, s(m), _ok])) -> le([n, _ok]) -> 15
}
Sat witness: Found: ((plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]), {
_jk -> s(s(z))  ;  mm -> z  ;  n -> s(s(z))
})

-------------------------------------------
Step 15, which took 0.024230 s (model generation: 0.023492,  model checking: 0.000738):

Model:
|_
{
le -> 
{{{
Q={q_gen_2377, q_gen_2378, q_gen_2392, q_gen_2393},
Q_f={q_gen_2377},
Delta=
{
<s>(q_gen_2378) -> q_gen_2378
<z>() -> q_gen_2378
<s, s>(q_gen_2377) -> q_gen_2377
<s, s>(q_gen_2392) -> q_gen_2377
<z, s>(q_gen_2378) -> q_gen_2377
<s, s>(q_gen_2393) -> q_gen_2392
<z, z>() -> q_gen_2393
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2376, q_gen_2379, q_gen_2380, q_gen_2389, q_gen_2390},
Q_f={q_gen_2376, q_gen_2379},
Delta=
{
<s>(q_gen_2390) -> q_gen_2390
<z>() -> q_gen_2390
<s, s>(q_gen_2380) -> q_gen_2380
<z, s>(q_gen_2390) -> q_gen_2380
<z, z>() -> q_gen_2380
<s, s, s>(q_gen_2379) -> q_gen_2376
<z, z, z>() -> q_gen_2376
<s, s, s>(q_gen_2389) -> q_gen_2379
<s, z, s>(q_gen_2380) -> q_gen_2379
<z, s, s>(q_gen_2380) -> q_gen_2379
<s, s, s>(q_gen_2376) -> q_gen_2389
<z, z, s>(q_gen_2390) -> q_gen_2389
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 11
() -> plus([n, z, n]) -> 12
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 11
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 15
(le([s(nn1), z])) -> BOT -> 12
(le([z, z])) -> BOT -> 13
(plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]) -> 16
(plus([n, s(m), _ok])) -> le([n, _ok]) -> 15
}
Sat witness: Found: ((le([s(nn1), s(nn2)])) -> le([nn1, nn2]), {
nn1 -> s(z)  ;  nn2 -> s(z)
})

-------------------------------------------
Step 16, which took 0.024414 s (model generation: 0.023959,  model checking: 0.000455):

Model:
|_
{
le -> 
{{{
Q={q_gen_2377, q_gen_2378, q_gen_2392},
Q_f={q_gen_2377},
Delta=
{
<s>(q_gen_2378) -> q_gen_2378
<z>() -> q_gen_2378
<s, s>(q_gen_2377) -> q_gen_2377
<z, s>(q_gen_2378) -> q_gen_2377
<s, s>(q_gen_2392) -> q_gen_2392
<z, z>() -> q_gen_2392
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2376, q_gen_2380, q_gen_2382, q_gen_2383, q_gen_2387, q_gen_2390},
Q_f={q_gen_2376, q_gen_2382},
Delta=
{
<s>(q_gen_2390) -> q_gen_2390
<z>() -> q_gen_2390
<z, z>() -> q_gen_2380
<s, s>(q_gen_2380) -> q_gen_2383
<z, s>(q_gen_2390) -> q_gen_2383
<z, s, s>(q_gen_2380) -> q_gen_2376
<z, z, z>() -> q_gen_2376
<s, s, s>(q_gen_2382) -> q_gen_2382
<s, z, s>(q_gen_2383) -> q_gen_2382
<z, s, s>(q_gen_2383) -> q_gen_2382
<z, z, s>(q_gen_2390) -> q_gen_2382
<s, s, s>(q_gen_2376) -> q_gen_2387
<s, s, s>(q_gen_2387) -> q_gen_2387
<s, z, s>(q_gen_2380) -> q_gen_2387
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 12
() -> plus([n, z, n]) -> 15
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 12
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 15
(le([s(nn1), z])) -> BOT -> 13
(le([z, z])) -> BOT -> 13
(plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]) -> 16
(plus([n, s(m), _ok])) -> le([n, _ok]) -> 15
}
Sat witness: Found: (() -> plus([n, z, n]), {
n -> s(z)
})

-------------------------------------------
Step 17, which took 0.025366 s (model generation: 0.022814,  model checking: 0.002552):

Model:
|_
{
le -> 
{{{
Q={q_gen_2377, q_gen_2378, q_gen_2392},
Q_f={q_gen_2377},
Delta=
{
<s>(q_gen_2378) -> q_gen_2378
<z>() -> q_gen_2378
<s, s>(q_gen_2377) -> q_gen_2377
<z, s>(q_gen_2378) -> q_gen_2377
<s, s>(q_gen_2392) -> q_gen_2392
<z, z>() -> q_gen_2392
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2376, q_gen_2380, q_gen_2389, q_gen_2390, q_gen_2391, q_gen_2396},
Q_f={q_gen_2376, q_gen_2389},
Delta=
{
<s>(q_gen_2390) -> q_gen_2390
<z>() -> q_gen_2390
<s, s>(q_gen_2380) -> q_gen_2380
<z, z>() -> q_gen_2380
<z, s>(q_gen_2390) -> q_gen_2396
<s, s, s>(q_gen_2389) -> q_gen_2376
<s, z, s>(q_gen_2380) -> q_gen_2376
<z, s, s>(q_gen_2380) -> q_gen_2376
<z, z, z>() -> q_gen_2376
<s, z, s>(q_gen_2396) -> q_gen_2389
<z, s, s>(q_gen_2396) -> q_gen_2389
<z, z, s>(q_gen_2390) -> q_gen_2389
<s, s, s>(q_gen_2376) -> q_gen_2391
<s, s, s>(q_gen_2391) -> q_gen_2391
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 13
() -> plus([n, z, n]) -> 16
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 13
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 16
(le([s(nn1), z])) -> BOT -> 14
(le([z, z])) -> BOT -> 14
(plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]) -> 19
(plus([n, s(m), _ok])) -> le([n, _ok]) -> 16
}
Sat witness: Found: ((plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]), {
_jk -> s(s(z))  ;  mm -> s(z)  ;  n -> z
})

-------------------------------------------
Step 18, which took 0.025228 s (model generation: 0.024109,  model checking: 0.001119):

Model:
|_
{
le -> 
{{{
Q={q_gen_2377, q_gen_2378, q_gen_2392},
Q_f={q_gen_2377},
Delta=
{
<s>(q_gen_2378) -> q_gen_2378
<z>() -> q_gen_2378
<s, s>(q_gen_2377) -> q_gen_2377
<z, s>(q_gen_2378) -> q_gen_2377
<s, s>(q_gen_2392) -> q_gen_2392
<z, z>() -> q_gen_2392
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  plus -> 
{{{
Q={q_gen_2376, q_gen_2380, q_gen_2382, q_gen_2383, q_gen_2390, q_gen_2391},
Q_f={q_gen_2376, q_gen_2382},
Delta=
{
<s>(q_gen_2390) -> q_gen_2390
<z>() -> q_gen_2390
<z, z>() -> q_gen_2380
<s, s>(q_gen_2380) -> q_gen_2383
<s, s>(q_gen_2383) -> q_gen_2383
<z, s>(q_gen_2390) -> q_gen_2383
<s, z, s>(q_gen_2380) -> q_gen_2376
<z, s, s>(q_gen_2380) -> q_gen_2376
<z, z, z>() -> q_gen_2376
<s, s, s>(q_gen_2382) -> q_gen_2382
<s, z, s>(q_gen_2383) -> q_gen_2382
<z, s, s>(q_gen_2383) -> q_gen_2382
<z, z, s>(q_gen_2390) -> q_gen_2382
<s, s, s>(q_gen_2376) -> q_gen_2391
<s, s, s>(q_gen_2391) -> q_gen_2391
}

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

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

Teacher's answer:
New clause system:
{
() -> le([z, s(nn2)]) -> 14
() -> plus([n, z, n]) -> 16
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 14
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 16
(le([s(nn1), z])) -> BOT -> 15
(le([z, z])) -> BOT -> 15
(plus([n, mm, _jk])) -> plus([n, s(mm), s(_jk)]) -> 19
(plus([n, s(m), _ok])) -> le([n, _ok]) -> 19
}
Sat witness: Found: ((plus([n, s(m), _ok])) -> le([n, _ok]), {
_ok -> s(s(s(z)))  ;  m -> z  ;  n -> s(s(s(z)))
})

Total time: 0.283084
Reason for stopping: Proved