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


Learning problem is:

env: {
nat -> {s, z}
}
definition:
{
(double, F:
{() -> double([z, z])
(double([nn, _pm])) -> double([s(nn), s(s(_pm))])}
(double([_qm, _rm]) /\ double([_qm, _sm])) -> eq_nat([_rm, _sm])
)
(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:
{(double([n, _tm]) /\ le([z, n])) -> le([n, _tm])}


over-approximation: {double}
under-approximation: {}

Clause system for inference is:

{
() -> double([z, z]) -> 0
() -> le([z, s(nn2)]) -> 0
(double([n, _tm]) /\ le([z, n])) -> le([n, _tm]) -> 0
(double([nn, _pm])) -> double([s(nn), s(s(_pm))]) -> 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
}


Solving took 0.131758 seconds.
Proved
Model:
|_
{
double -> 
{{{
Q={q_gen_2584, q_gen_2586, q_gen_2588, q_gen_2589},
Q_f={q_gen_2584, q_gen_2586},
Delta=
{
<s>(q_gen_2588) -> q_gen_2588
<z>() -> q_gen_2588
<z, z>() -> q_gen_2584
<s, s>(q_gen_2586) -> q_gen_2586
<z, s>(q_gen_2588) -> q_gen_2586
<s, s>(q_gen_2584) -> q_gen_2589
<s, s>(q_gen_2589) -> q_gen_2589
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  le -> 
{{{
Q={q_gen_2582, q_gen_2583, q_gen_2590},
Q_f={q_gen_2582},
Delta=
{
<s>(q_gen_2583) -> q_gen_2583
<z>() -> q_gen_2583
<s, s>(q_gen_2582) -> q_gen_2582
<z, s>(q_gen_2583) -> q_gen_2582
<s, s>(q_gen_2590) -> q_gen_2590
<z, z>() -> q_gen_2590
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.010009 s (model generation: 0.009770,  model checking: 0.000239):

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 0
() -> le([z, s(nn2)]) -> 3
(double([n, _tm]) /\ le([z, n])) -> le([n, _tm]) -> 1
(double([nn, _pm])) -> double([s(nn), s(s(_pm))]) -> 1
(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
}
Sat witness: Found: (() -> le([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 1, which took 0.010221 s (model generation: 0.010132,  model checking: 0.000089):

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

}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  le -> 
{{{
Q={q_gen_2582, q_gen_2583},
Q_f={q_gen_2582},
Delta=
{
<z>() -> q_gen_2583
<z, s>(q_gen_2583) -> q_gen_2582
}

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 3
() -> le([z, s(nn2)]) -> 3
(double([n, _tm]) /\ le([z, n])) -> le([n, _tm]) -> 1
(double([nn, _pm])) -> double([s(nn), s(s(_pm))]) -> 1
(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
}
Sat witness: Found: (() -> double([z, z]), {

})

-------------------------------------------
Step 2, which took 0.010907 s (model generation: 0.010651,  model checking: 0.000256):

Model:
|_
{
double -> 
{{{
Q={q_gen_2584},
Q_f={q_gen_2584},
Delta=
{
<z, z>() -> q_gen_2584
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  le -> 
{{{
Q={q_gen_2582, q_gen_2583},
Q_f={q_gen_2582},
Delta=
{
<z>() -> q_gen_2583
<z, s>(q_gen_2583) -> q_gen_2582
}

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 3
() -> le([z, s(nn2)]) -> 3
(double([n, _tm]) /\ le([z, n])) -> le([n, _tm]) -> 1
(double([nn, _pm])) -> double([s(nn), s(s(_pm))]) -> 1
(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
}
Sat witness: Found: ((le([nn1, nn2])) -> le([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> s(z)
})

-------------------------------------------
Step 3, which took 0.010523 s (model generation: 0.010383,  model checking: 0.000140):

Model:
|_
{
double -> 
{{{
Q={q_gen_2584},
Q_f={q_gen_2584},
Delta=
{
<z, z>() -> q_gen_2584
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  le -> 
{{{
Q={q_gen_2582, q_gen_2583},
Q_f={q_gen_2582},
Delta=
{
<z>() -> q_gen_2583
<s, s>(q_gen_2582) -> q_gen_2582
<z, s>(q_gen_2583) -> q_gen_2582
}

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 3
() -> le([z, s(nn2)]) -> 3
(double([n, _tm]) /\ le([z, n])) -> le([n, _tm]) -> 1
(double([nn, _pm])) -> double([s(nn), s(s(_pm))]) -> 4
(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
}
Sat witness: Found: ((double([nn, _pm])) -> double([s(nn), s(s(_pm))]), {
_pm -> z  ;  nn -> z
})

-------------------------------------------
Step 4, which took 0.011055 s (model generation: 0.010870,  model checking: 0.000185):

Model:
|_
{
double -> 
{{{
Q={q_gen_2584, q_gen_2588},
Q_f={q_gen_2584},
Delta=
{
<z>() -> q_gen_2588
<s, s>(q_gen_2584) -> q_gen_2584
<z, s>(q_gen_2588) -> q_gen_2584
<z, z>() -> q_gen_2584
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  le -> 
{{{
Q={q_gen_2582, q_gen_2583},
Q_f={q_gen_2582},
Delta=
{
<z>() -> q_gen_2583
<s, s>(q_gen_2582) -> q_gen_2582
<z, s>(q_gen_2583) -> q_gen_2582
}

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 3
() -> le([z, s(nn2)]) -> 3
(double([n, _tm]) /\ le([z, n])) -> le([n, _tm]) -> 4
(double([nn, _pm])) -> double([s(nn), s(s(_pm))]) -> 4
(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
}
Sat witness: Found: ((double([n, _tm]) /\ le([z, n])) -> le([n, _tm]), {
_tm -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 5, which took 0.012047 s (model generation: 0.012018,  model checking: 0.000029):

Model:
|_
{
double -> 
{{{
Q={q_gen_2584, q_gen_2588},
Q_f={q_gen_2584},
Delta=
{
<z>() -> q_gen_2588
<s, s>(q_gen_2584) -> q_gen_2584
<z, s>(q_gen_2588) -> q_gen_2584
<z, z>() -> q_gen_2584
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  le -> 
{{{
Q={q_gen_2582, q_gen_2583},
Q_f={q_gen_2582},
Delta=
{
<z>() -> q_gen_2583
<s, s>(q_gen_2582) -> q_gen_2582
<z, s>(q_gen_2583) -> q_gen_2582
<z, z>() -> q_gen_2582
}

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 3
() -> le([z, s(nn2)]) -> 3
(double([n, _tm]) /\ le([z, n])) -> le([n, _tm]) -> 4
(double([nn, _pm])) -> double([s(nn), s(s(_pm))]) -> 4
(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 -> 5
}
Sat witness: Found: ((le([z, z])) -> BOT, {

})

-------------------------------------------
Step 6, which took 0.011854 s (model generation: 0.011693,  model checking: 0.000161):

Model:
|_
{
double -> 
{{{
Q={q_gen_2584, q_gen_2588},
Q_f={q_gen_2584},
Delta=
{
<z>() -> q_gen_2588
<s, s>(q_gen_2584) -> q_gen_2584
<z, s>(q_gen_2588) -> q_gen_2584
<z, z>() -> q_gen_2584
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  le -> 
{{{
Q={q_gen_2582, q_gen_2583, q_gen_2591},
Q_f={q_gen_2582},
Delta=
{
<z>() -> q_gen_2583
<s, s>(q_gen_2582) -> q_gen_2582
<s, s>(q_gen_2591) -> q_gen_2582
<z, s>(q_gen_2583) -> q_gen_2582
<z, z>() -> q_gen_2591
}

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 3
() -> le([z, s(nn2)]) -> 3
(double([n, _tm]) /\ le([z, n])) -> le([n, _tm]) -> 4
(double([nn, _pm])) -> double([s(nn), s(s(_pm))]) -> 4
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 5
(le([s(nn1), z])) -> BOT -> 3
(le([z, z])) -> BOT -> 5
}
Sat witness: Found: ((le([s(nn1), s(nn2)])) -> le([nn1, nn2]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 7, which took 0.011924 s (model generation: 0.011764,  model checking: 0.000160):

Model:
|_
{
double -> 
{{{
Q={q_gen_2584, q_gen_2587, q_gen_2588},
Q_f={q_gen_2584},
Delta=
{
<z>() -> q_gen_2588
<s, s>(q_gen_2587) -> q_gen_2584
<z, z>() -> q_gen_2584
<s, s>(q_gen_2584) -> q_gen_2587
<z, s>(q_gen_2588) -> q_gen_2587
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  le -> 
{{{
Q={q_gen_2582, q_gen_2583, q_gen_2590},
Q_f={q_gen_2582},
Delta=
{
<z>() -> q_gen_2583
<s, s>(q_gen_2582) -> q_gen_2582
<z, s>(q_gen_2583) -> q_gen_2582
<s, s>(q_gen_2590) -> q_gen_2590
<z, z>() -> q_gen_2590
}

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 3
() -> le([z, s(nn2)]) -> 6
(double([n, _tm]) /\ le([z, n])) -> le([n, _tm]) -> 4
(double([nn, _pm])) -> double([s(nn), s(s(_pm))]) -> 4
(le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4
(le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 5
(le([s(nn1), z])) -> BOT -> 4
(le([z, z])) -> BOT -> 5
}
Sat witness: Found: (() -> le([z, s(nn2)]), {
nn2 -> s(z)
})

-------------------------------------------
Step 8, which took 0.013039 s (model generation: 0.012540,  model checking: 0.000499):

Model:
|_
{
double -> 
{{{
Q={q_gen_2584, q_gen_2587, q_gen_2588},
Q_f={q_gen_2584},
Delta=
{
<z>() -> q_gen_2588
<s, s>(q_gen_2587) -> q_gen_2584
<z, z>() -> q_gen_2584
<s, s>(q_gen_2584) -> q_gen_2587
<z, s>(q_gen_2588) -> q_gen_2587
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  le -> 
{{{
Q={q_gen_2582, q_gen_2583, q_gen_2590},
Q_f={q_gen_2582},
Delta=
{
<s>(q_gen_2583) -> q_gen_2583
<z>() -> q_gen_2583
<s, s>(q_gen_2582) -> q_gen_2582
<z, s>(q_gen_2583) -> q_gen_2582
<s, s>(q_gen_2590) -> q_gen_2590
<z, z>() -> q_gen_2590
}

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 4
() -> le([z, s(nn2)]) -> 6
(double([n, _tm]) /\ le([z, n])) -> le([n, _tm]) -> 4
(double([nn, _pm])) -> double([s(nn), s(s(_pm))]) -> 7
(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
}
Sat witness: Found: ((double([nn, _pm])) -> double([s(nn), s(s(_pm))]), {
_pm -> s(s(z))  ;  nn -> s(z)
})

-------------------------------------------
Step 9, which took 0.013865 s (model generation: 0.013657,  model checking: 0.000208):

Model:
|_
{
double -> 
{{{
Q={q_gen_2584, q_gen_2587, q_gen_2588, q_gen_2597},
Q_f={q_gen_2584},
Delta=
{
<z>() -> q_gen_2588
<s>(q_gen_2588) -> q_gen_2597
<s, s>(q_gen_2587) -> q_gen_2584
<z, s>(q_gen_2597) -> q_gen_2584
<z, z>() -> q_gen_2584
<s, s>(q_gen_2584) -> q_gen_2587
<z, s>(q_gen_2588) -> q_gen_2587
}

Datatype: <nat, nat>
Convolution form: right
}}}
  ;  le -> 
{{{
Q={q_gen_2582, q_gen_2583, q_gen_2590},
Q_f={q_gen_2582},
Delta=
{
<s>(q_gen_2583) -> q_gen_2583
<z>() -> q_gen_2583
<s, s>(q_gen_2582) -> q_gen_2582
<z, s>(q_gen_2583) -> q_gen_2582
<s, s>(q_gen_2590) -> q_gen_2590
<z, z>() -> q_gen_2590
}

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 4
() -> le([z, s(nn2)]) -> 6
(double([n, _tm]) /\ le([z, n])) -> le([n, _tm]) -> 7
(double([nn, _pm])) -> double([s(nn), s(s(_pm))]) -> 7
(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
}
Sat witness: Found: ((double([n, _tm]) /\ le([z, n])) -> le([n, _tm]), {
_tm -> s(s(z))  ;  n -> s(s(z))
})

Total time: 0.131758
Reason for stopping: Proved