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


Learning problem is:

env: {
nat -> {s, z}
}
definition:
{
(double, F:
{() -> double([z, z])
(double([nn, _sr])) -> double([s(nn), s(s(_sr))])}
(double([_tr, _ur]) /\ double([_tr, _vr])) -> eq_nat([_ur, _vr])
)
(is_even, P:
{() -> is_even([z])
(is_even([n3])) -> is_even([s(s(n3))])
(is_even([s(s(n3))])) -> is_even([n3])
(is_even([s(z)])) -> BOT}
)
}

properties:
{(double([n, _wr])) -> is_even([_wr])}


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

Clause system for inference is:

{
() -> double([z, z]) -> 0
() -> is_even([z]) -> 0
(double([n, _wr])) -> is_even([_wr]) -> 0
(double([nn, _sr])) -> double([s(nn), s(s(_sr))]) -> 0
(is_even([n3])) -> is_even([s(s(n3))]) -> 0
(is_even([s(s(n3))])) -> is_even([n3]) -> 0
(is_even([s(z)])) -> BOT -> 0
}


Solving took 0.146682 seconds.
Proved
Model:
|_
{
double -> 
{{{
Q={q_gen_4826, q_gen_4830, q_gen_4831, q_gen_4836},
Q_f={q_gen_4826},
Delta=
{
<s>(q_gen_4836) -> q_gen_4831
<z>() -> q_gen_4831
<s>(q_gen_4831) -> q_gen_4836
<s, s>(q_gen_4830) -> q_gen_4826
<z, s>(q_gen_4836) -> q_gen_4826
<z, z>() -> q_gen_4826
<s, s>(q_gen_4826) -> q_gen_4830
<z, s>(q_gen_4831) -> q_gen_4830
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  is_even -> 
{{{
Q={q_gen_4825, q_gen_4828},
Q_f={q_gen_4825},
Delta=
{
<s>(q_gen_4828) -> q_gen_4825
<z>() -> q_gen_4825
<s>(q_gen_4825) -> q_gen_4828
}

Datatype: <nat>
Convolution form: left
}}}

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.008992 s (model generation: 0.008927,  model checking: 0.000065):

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

}

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

}

Datatype: <nat>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 0
() -> is_even([z]) -> 3
(double([n, _wr])) -> is_even([_wr]) -> 1
(double([nn, _sr])) -> double([s(nn), s(s(_sr))]) -> 1
(is_even([n3])) -> is_even([s(s(n3))]) -> 1
(is_even([s(s(n3))])) -> is_even([n3]) -> 1
(is_even([s(z)])) -> BOT -> 1
}
Sat witness: Found: (() -> is_even([z]), {

})

-------------------------------------------
Step 1, which took 0.010415 s (model generation: 0.010370,  model checking: 0.000045):

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

}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  is_even -> 
{{{
Q={q_gen_4825},
Q_f={q_gen_4825},
Delta=
{
<z>() -> q_gen_4825
}

Datatype: <nat>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 3
() -> is_even([z]) -> 3
(double([n, _wr])) -> is_even([_wr]) -> 1
(double([nn, _sr])) -> double([s(nn), s(s(_sr))]) -> 1
(is_even([n3])) -> is_even([s(s(n3))]) -> 1
(is_even([s(s(n3))])) -> is_even([n3]) -> 1
(is_even([s(z)])) -> BOT -> 1
}
Sat witness: Found: (() -> double([z, z]), {

})

-------------------------------------------
Step 2, which took 0.012188 s (model generation: 0.012072,  model checking: 0.000116):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  is_even -> 
{{{
Q={q_gen_4825},
Q_f={q_gen_4825},
Delta=
{
<z>() -> q_gen_4825
}

Datatype: <nat>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 3
() -> is_even([z]) -> 3
(double([n, _wr])) -> is_even([_wr]) -> 1
(double([nn, _sr])) -> double([s(nn), s(s(_sr))]) -> 1
(is_even([n3])) -> is_even([s(s(n3))]) -> 4
(is_even([s(s(n3))])) -> is_even([n3]) -> 2
(is_even([s(z)])) -> BOT -> 2
}
Sat witness: Found: ((is_even([n3])) -> is_even([s(s(n3))]), {
n3 -> z
})

-------------------------------------------
Step 3, which took 0.013710 s (model generation: 0.013628,  model checking: 0.000082):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  is_even -> 
{{{
Q={q_gen_4825},
Q_f={q_gen_4825},
Delta=
{
<s>(q_gen_4825) -> q_gen_4825
<z>() -> q_gen_4825
}

Datatype: <nat>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 3
() -> is_even([z]) -> 3
(double([n, _wr])) -> is_even([_wr]) -> 1
(double([nn, _sr])) -> double([s(nn), s(s(_sr))]) -> 4
(is_even([n3])) -> is_even([s(s(n3))]) -> 4
(is_even([s(s(n3))])) -> is_even([n3]) -> 2
(is_even([s(z)])) -> BOT -> 2
}
Sat witness: Found: ((double([nn, _sr])) -> double([s(nn), s(s(_sr))]), {
_sr -> z  ;  nn -> z
})

-------------------------------------------
Step 4, which took 0.015122 s (model generation: 0.015081,  model checking: 0.000041):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  is_even -> 
{{{
Q={q_gen_4825},
Q_f={q_gen_4825},
Delta=
{
<s>(q_gen_4825) -> q_gen_4825
<z>() -> q_gen_4825
}

Datatype: <nat>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 3
() -> is_even([z]) -> 3
(double([n, _wr])) -> is_even([_wr]) -> 2
(double([nn, _sr])) -> double([s(nn), s(s(_sr))]) -> 4
(is_even([n3])) -> is_even([s(s(n3))]) -> 4
(is_even([s(s(n3))])) -> is_even([n3]) -> 2
(is_even([s(z)])) -> BOT -> 5
}
Sat witness: Found: ((is_even([s(z)])) -> BOT, {

})

-------------------------------------------
Step 5, which took 0.010676 s (model generation: 0.010568,  model checking: 0.000108):

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

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  is_even -> 
{{{
Q={q_gen_4825, q_gen_4828},
Q_f={q_gen_4825},
Delta=
{
<s>(q_gen_4828) -> q_gen_4825
<z>() -> q_gen_4825
<s>(q_gen_4825) -> q_gen_4828
}

Datatype: <nat>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 3
() -> is_even([z]) -> 3
(double([n, _wr])) -> is_even([_wr]) -> 5
(double([nn, _sr])) -> double([s(nn), s(s(_sr))]) -> 4
(is_even([n3])) -> is_even([s(s(n3))]) -> 4
(is_even([s(s(n3))])) -> is_even([n3]) -> 3
(is_even([s(z)])) -> BOT -> 5
}
Sat witness: Found: ((double([n, _wr])) -> is_even([_wr]), {
_wr -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 6, which took 0.013801 s (model generation: 0.013390,  model checking: 0.000411):

Model:
|_
{
double -> 
{{{
Q={q_gen_4826, q_gen_4830, q_gen_4831},
Q_f={q_gen_4826},
Delta=
{
<z>() -> q_gen_4831
<s, s>(q_gen_4830) -> q_gen_4826
<z, z>() -> q_gen_4826
<s, s>(q_gen_4826) -> q_gen_4830
<z, s>(q_gen_4831) -> q_gen_4830
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  is_even -> 
{{{
Q={q_gen_4825, q_gen_4828},
Q_f={q_gen_4825},
Delta=
{
<s>(q_gen_4828) -> q_gen_4825
<z>() -> q_gen_4825
<s>(q_gen_4825) -> q_gen_4828
}

Datatype: <nat>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 4
() -> is_even([z]) -> 4
(double([n, _wr])) -> is_even([_wr]) -> 5
(double([nn, _sr])) -> double([s(nn), s(s(_sr))]) -> 7
(is_even([n3])) -> is_even([s(s(n3))]) -> 5
(is_even([s(s(n3))])) -> is_even([n3]) -> 4
(is_even([s(z)])) -> BOT -> 5
}
Sat witness: Found: ((double([nn, _sr])) -> double([s(nn), s(s(_sr))]), {
_sr -> s(s(z))  ;  nn -> s(z)
})

-------------------------------------------
Step 7, which took 0.014346 s (model generation: 0.013969,  model checking: 0.000377):

Model:
|_
{
double -> 
{{{
Q={q_gen_4826, q_gen_4830, q_gen_4831, q_gen_4836},
Q_f={q_gen_4826},
Delta=
{
<z>() -> q_gen_4831
<s>(q_gen_4831) -> q_gen_4836
<s, s>(q_gen_4830) -> q_gen_4826
<z, s>(q_gen_4836) -> q_gen_4826
<z, z>() -> q_gen_4826
<s, s>(q_gen_4826) -> q_gen_4830
<z, s>(q_gen_4831) -> q_gen_4830
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  is_even -> 
{{{
Q={q_gen_4825, q_gen_4828},
Q_f={q_gen_4825},
Delta=
{
<s>(q_gen_4828) -> q_gen_4825
<z>() -> q_gen_4825
<s>(q_gen_4825) -> q_gen_4828
}

Datatype: <nat>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 5
() -> is_even([z]) -> 5
(double([n, _wr])) -> is_even([_wr]) -> 6
(double([nn, _sr])) -> double([s(nn), s(s(_sr))]) -> 10
(is_even([n3])) -> is_even([s(s(n3))]) -> 6
(is_even([s(s(n3))])) -> is_even([n3]) -> 5
(is_even([s(z)])) -> BOT -> 6
}
Sat witness: Found: ((double([nn, _sr])) -> double([s(nn), s(s(_sr))]), {
_sr -> s(s(z))  ;  nn -> z
})

-------------------------------------------
Step 8, which took 0.014685 s (model generation: 0.014469,  model checking: 0.000216):

Model:
|_
{
double -> 
{{{
Q={q_gen_4826, q_gen_4829, q_gen_4831, q_gen_4832},
Q_f={q_gen_4826, q_gen_4829},
Delta=
{
<s>(q_gen_4831) -> q_gen_4831
<z>() -> q_gen_4831
<z, z>() -> q_gen_4826
<s, s>(q_gen_4829) -> q_gen_4829
<z, s>(q_gen_4831) -> q_gen_4829
<s, s>(q_gen_4826) -> q_gen_4832
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  is_even -> 
{{{
Q={q_gen_4825, q_gen_4828},
Q_f={q_gen_4825},
Delta=
{
<s>(q_gen_4828) -> q_gen_4825
<z>() -> q_gen_4825
<s>(q_gen_4825) -> q_gen_4828
}

Datatype: <nat>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 6
() -> is_even([z]) -> 6
(double([n, _wr])) -> is_even([_wr]) -> 9
(double([nn, _sr])) -> double([s(nn), s(s(_sr))]) -> 10
(is_even([n3])) -> is_even([s(s(n3))]) -> 7
(is_even([s(s(n3))])) -> is_even([n3]) -> 6
(is_even([s(z)])) -> BOT -> 7
}
Sat witness: Found: ((double([n, _wr])) -> is_even([_wr]), {
_wr -> s(z)  ;  n -> z
})

-------------------------------------------
Step 9, which took 0.014904 s (model generation: 0.013689,  model checking: 0.001215):

Model:
|_
{
double -> 
{{{
Q={q_gen_4826, q_gen_4829, q_gen_4830, q_gen_4831},
Q_f={q_gen_4826, q_gen_4829},
Delta=
{
<s>(q_gen_4831) -> q_gen_4831
<z>() -> q_gen_4831
<z, z>() -> q_gen_4826
<s, s>(q_gen_4829) -> q_gen_4829
<s, s>(q_gen_4830) -> q_gen_4829
<s, s>(q_gen_4826) -> q_gen_4830
<z, s>(q_gen_4831) -> q_gen_4830
}

Datatype: <nat, nat>
Convolution form: left
}}}
  ;  is_even -> 
{{{
Q={q_gen_4825, q_gen_4828},
Q_f={q_gen_4825},
Delta=
{
<s>(q_gen_4828) -> q_gen_4825
<z>() -> q_gen_4825
<s>(q_gen_4825) -> q_gen_4828
}

Datatype: <nat>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 7
() -> is_even([z]) -> 7
(double([n, _wr])) -> is_even([_wr]) -> 12
(double([nn, _sr])) -> double([s(nn), s(s(_sr))]) -> 10
(is_even([n3])) -> is_even([s(s(n3))]) -> 8
(is_even([s(s(n3))])) -> is_even([n3]) -> 7
(is_even([s(z)])) -> BOT -> 8
}
Sat witness: Found: ((double([n, _wr])) -> is_even([_wr]), {
_wr -> s(s(s(z)))  ;  n -> s(s(s(z)))
})

Total time: 0.146682
Reason for stopping: Proved