Solving ../../benchmarks/true/nat_double_is_le.smt2...

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


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.134577 seconds.
Proved
Model:
|_
{
double -> 
{{{
Q={q_gen_4730, q_gen_4732, q_gen_4734, q_gen_4735},
Q_f={q_gen_4730, q_gen_4732},
Delta=
{
<s>(q_gen_4734) -> q_gen_4734
<z>() -> q_gen_4734
<z, z>() -> q_gen_4730
<s, s>(q_gen_4732) -> q_gen_4732
<z, s>(q_gen_4734) -> q_gen_4732
<s, s>(q_gen_4730) -> q_gen_4735
<s, s>(q_gen_4735) -> q_gen_4735
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_4728, q_gen_4729, q_gen_4736},
Q_f={q_gen_4728},
Delta=
{
<s>(q_gen_4729) -> q_gen_4729
<z>() -> q_gen_4729
<s, s>(q_gen_4728) -> q_gen_4728
<z, s>(q_gen_4729) -> q_gen_4728
<s, s>(q_gen_4736) -> q_gen_4736
<z, z>() -> q_gen_4736
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006732 s (model generation: 0.006443,  model checking: 0.000289):

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

}

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

}

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

}
--
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: Yes: (() -> le([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 1, which took 0.010330 s (model generation: 0.010246,  model checking: 0.000084):

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

}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_4728, q_gen_4729},
Q_f={q_gen_4728},
Delta=
{
<z>() -> q_gen_4729
<z, s>(q_gen_4729) -> q_gen_4728
}

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

}
--
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: Yes: (() -> double([z, z]), {

})

-------------------------------------------
Step 2, which took 0.010586 s (model generation: 0.010334,  model checking: 0.000252):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_4728, q_gen_4729},
Q_f={q_gen_4728},
Delta=
{
<z>() -> q_gen_4729
<z, s>(q_gen_4729) -> q_gen_4728
}

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

}
--
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: Yes: ((le([nn1, nn2])) -> le([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> s(z)
})

-------------------------------------------
Step 3, which took 0.013654 s (model generation: 0.010649,  model checking: 0.003005):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_4728, q_gen_4729},
Q_f={q_gen_4728},
Delta=
{
<z>() -> q_gen_4729
<s, s>(q_gen_4728) -> q_gen_4728
<z, s>(q_gen_4729) -> q_gen_4728
}

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

}
--
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: Yes: ((double([nn, _pm])) -> double([s(nn), s(s(_pm))]), {
_pm -> z  ;  nn -> z
})

-------------------------------------------
Step 4, which took 0.011385 s (model generation: 0.011195,  model checking: 0.000190):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_4728, q_gen_4729},
Q_f={q_gen_4728},
Delta=
{
<z>() -> q_gen_4729
<s, s>(q_gen_4728) -> q_gen_4728
<z, s>(q_gen_4729) -> q_gen_4728
}

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

}
--
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: Yes: ((double([n, _tm]) /\ le([z, n])) -> le([n, _tm]), {
_tm -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 5, which took 0.011917 s (model generation: 0.011887,  model checking: 0.000030):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_4728, q_gen_4729},
Q_f={q_gen_4728},
Delta=
{
<z>() -> q_gen_4729
<s, s>(q_gen_4728) -> q_gen_4728
<z, s>(q_gen_4729) -> q_gen_4728
<z, z>() -> q_gen_4728
}

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

}
--
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: Yes: ((le([z, z])) -> BOT, {

})

-------------------------------------------
Step 6, which took 0.011084 s (model generation: 0.010787,  model checking: 0.000297):

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

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_4728, q_gen_4729, q_gen_4737},
Q_f={q_gen_4728},
Delta=
{
<z>() -> q_gen_4729
<s, s>(q_gen_4728) -> q_gen_4728
<s, s>(q_gen_4737) -> q_gen_4728
<z, s>(q_gen_4729) -> q_gen_4728
<z, z>() -> q_gen_4737
}

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

}
--
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: Yes: ((le([s(nn1), s(nn2)])) -> le([nn1, nn2]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 7, which took 0.011962 s (model generation: 0.011800,  model checking: 0.000162):

Model:
|_
{
double -> 
{{{
Q={q_gen_4730, q_gen_4733, q_gen_4734},
Q_f={q_gen_4730},
Delta=
{
<z>() -> q_gen_4734
<s, s>(q_gen_4733) -> q_gen_4730
<z, z>() -> q_gen_4730
<s, s>(q_gen_4730) -> q_gen_4733
<z, s>(q_gen_4734) -> q_gen_4733
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_4728, q_gen_4729, q_gen_4736},
Q_f={q_gen_4728},
Delta=
{
<z>() -> q_gen_4729
<s, s>(q_gen_4728) -> q_gen_4728
<z, s>(q_gen_4729) -> q_gen_4728
<s, s>(q_gen_4736) -> q_gen_4736
<z, z>() -> q_gen_4736
}

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

}
--
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: Yes: (() -> le([z, s(nn2)]), {
nn2 -> s(z)
})

-------------------------------------------
Step 8, which took 0.015882 s (model generation: 0.012183,  model checking: 0.003699):

Model:
|_
{
double -> 
{{{
Q={q_gen_4730, q_gen_4733, q_gen_4734},
Q_f={q_gen_4730},
Delta=
{
<z>() -> q_gen_4734
<s, s>(q_gen_4733) -> q_gen_4730
<z, z>() -> q_gen_4730
<s, s>(q_gen_4730) -> q_gen_4733
<z, s>(q_gen_4734) -> q_gen_4733
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_4728, q_gen_4729, q_gen_4736},
Q_f={q_gen_4728},
Delta=
{
<s>(q_gen_4729) -> q_gen_4729
<z>() -> q_gen_4729
<s, s>(q_gen_4728) -> q_gen_4728
<z, s>(q_gen_4729) -> q_gen_4728
<s, s>(q_gen_4736) -> q_gen_4736
<z, z>() -> q_gen_4736
}

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

}
--
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: Yes: ((double([nn, _pm])) -> double([s(nn), s(s(_pm))]), {
_pm -> s(s(z))  ;  nn -> s(z)
})

-------------------------------------------
Step 9, which took 0.014076 s (model generation: 0.013766,  model checking: 0.000310):

Model:
|_
{
double -> 
{{{
Q={q_gen_4730, q_gen_4733, q_gen_4734, q_gen_4743},
Q_f={q_gen_4730},
Delta=
{
<z>() -> q_gen_4734
<s>(q_gen_4734) -> q_gen_4743
<s, s>(q_gen_4733) -> q_gen_4730
<z, s>(q_gen_4743) -> q_gen_4730
<z, z>() -> q_gen_4730
<s, s>(q_gen_4730) -> q_gen_4733
<z, s>(q_gen_4734) -> q_gen_4733
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_4728, q_gen_4729, q_gen_4736},
Q_f={q_gen_4728},
Delta=
{
<s>(q_gen_4729) -> q_gen_4729
<z>() -> q_gen_4729
<s, s>(q_gen_4728) -> q_gen_4728
<z, s>(q_gen_4729) -> q_gen_4728
<s, s>(q_gen_4736) -> q_gen_4736
<z, z>() -> q_gen_4736
}

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

}
--
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: Yes: ((double([n, _tm]) /\ le([z, n])) -> le([n, _tm]), {
_tm -> s(s(z))  ;  n -> s(s(z))
})

Total time: 0.134577
Reason for stopping: Proved