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, _of])) -> double([s(nn), s(s(_of))])}
(double([_pf, _qf]) /\ double([_pf, _rf])) -> eq_nat([_qf, _rf])
)
(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, _sf])) -> is_even([_sf])}


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

Clause system for inference is:

{
() -> double([z, z]) -> 0
() -> is_even([z]) -> 0
(double([n, _sf])) -> is_even([_sf]) -> 0
(double([nn, _of])) -> double([s(nn), s(s(_of))]) -> 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.073207 seconds.
Proved
Model:
|_
{
double -> 
{{{
Q={q_gen_1086, q_gen_1090, q_gen_1091, q_gen_1096},
Q_f={q_gen_1086},
Delta=
{
<s>(q_gen_1096) -> q_gen_1091
<z>() -> q_gen_1091
<s>(q_gen_1091) -> q_gen_1096
<s, s>(q_gen_1090) -> q_gen_1086
<z, s>(q_gen_1096) -> q_gen_1086
<z, z>() -> q_gen_1086
<s, s>(q_gen_1086) -> q_gen_1090
<z, s>(q_gen_1091) -> q_gen_1090
}

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

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005310 s (model generation: 0.005134,  model checking: 0.000176):

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 0
() -> is_even([z]) -> 3
(double([n, _sf])) -> is_even([_sf]) -> 1
(double([nn, _of])) -> double([s(nn), s(s(_of))]) -> 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.005241 s (model generation: 0.005210,  model checking: 0.000031):

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 3
() -> is_even([z]) -> 3
(double([n, _sf])) -> is_even([_sf]) -> 1
(double([nn, _of])) -> double([s(nn), s(s(_of))]) -> 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.006261 s (model generation: 0.006176,  model checking: 0.000085):

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

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

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 3
() -> is_even([z]) -> 3
(double([n, _sf])) -> is_even([_sf]) -> 1
(double([nn, _of])) -> double([s(nn), s(s(_of))]) -> 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.007930 s (model generation: 0.005444,  model checking: 0.002486):

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

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

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 3
() -> is_even([z]) -> 3
(double([n, _sf])) -> is_even([_sf]) -> 1
(double([nn, _of])) -> double([s(nn), s(s(_of))]) -> 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, _of])) -> double([s(nn), s(s(_of))]), {
_of -> z  ;  nn -> z
})

-------------------------------------------
Step 4, which took 0.005720 s (model generation: 0.005673,  model checking: 0.000047):

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

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

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 3
() -> is_even([z]) -> 3
(double([n, _sf])) -> is_even([_sf]) -> 2
(double([nn, _of])) -> double([s(nn), s(s(_of))]) -> 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.006205 s (model generation: 0.006036,  model checking: 0.000169):

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

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

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 3
() -> is_even([z]) -> 3
(double([n, _sf])) -> is_even([_sf]) -> 5
(double([nn, _of])) -> double([s(nn), s(s(_of))]) -> 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, _sf])) -> is_even([_sf]), {
_sf -> s(z)  ;  n -> s(z)
})

-------------------------------------------
Step 6, which took 0.004706 s (model generation: 0.004346,  model checking: 0.000360):

Model:
|_
{
double -> 
{{{
Q={q_gen_1086, q_gen_1090, q_gen_1091},
Q_f={q_gen_1086},
Delta=
{
<z>() -> q_gen_1091
<s, s>(q_gen_1090) -> q_gen_1086
<z, z>() -> q_gen_1086
<s, s>(q_gen_1086) -> q_gen_1090
<z, s>(q_gen_1091) -> q_gen_1090
}

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

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 4
() -> is_even([z]) -> 4
(double([n, _sf])) -> is_even([_sf]) -> 5
(double([nn, _of])) -> double([s(nn), s(s(_of))]) -> 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, _of])) -> double([s(nn), s(s(_of))]), {
_of -> s(s(z))  ;  nn -> s(z)
})

-------------------------------------------
Step 7, which took 0.009164 s (model generation: 0.007204,  model checking: 0.001960):

Model:
|_
{
double -> 
{{{
Q={q_gen_1086, q_gen_1090, q_gen_1091, q_gen_1096},
Q_f={q_gen_1086},
Delta=
{
<z>() -> q_gen_1091
<s>(q_gen_1091) -> q_gen_1096
<s, s>(q_gen_1090) -> q_gen_1086
<z, s>(q_gen_1096) -> q_gen_1086
<z, z>() -> q_gen_1086
<s, s>(q_gen_1086) -> q_gen_1090
<z, s>(q_gen_1091) -> q_gen_1090
}

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

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 5
() -> is_even([z]) -> 5
(double([n, _sf])) -> is_even([_sf]) -> 6
(double([nn, _of])) -> double([s(nn), s(s(_of))]) -> 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, _of])) -> double([s(nn), s(s(_of))]), {
_of -> s(s(z))  ;  nn -> z
})

-------------------------------------------
Step 8, which took 0.006620 s (model generation: 0.006072,  model checking: 0.000548):

Model:
|_
{
double -> 
{{{
Q={q_gen_1086, q_gen_1089, q_gen_1091, q_gen_1092},
Q_f={q_gen_1086, q_gen_1089},
Delta=
{
<s>(q_gen_1091) -> q_gen_1091
<z>() -> q_gen_1091
<z, z>() -> q_gen_1086
<s, s>(q_gen_1089) -> q_gen_1089
<z, s>(q_gen_1091) -> q_gen_1089
<s, s>(q_gen_1086) -> q_gen_1092
}

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

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 6
() -> is_even([z]) -> 6
(double([n, _sf])) -> is_even([_sf]) -> 9
(double([nn, _of])) -> double([s(nn), s(s(_of))]) -> 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, _sf])) -> is_even([_sf]), {
_sf -> s(z)  ;  n -> z
})

-------------------------------------------
Step 9, which took 0.008095 s (model generation: 0.007415,  model checking: 0.000680):

Model:
|_
{
double -> 
{{{
Q={q_gen_1086, q_gen_1089, q_gen_1090, q_gen_1091},
Q_f={q_gen_1086, q_gen_1089},
Delta=
{
<s>(q_gen_1091) -> q_gen_1091
<z>() -> q_gen_1091
<z, z>() -> q_gen_1086
<s, s>(q_gen_1089) -> q_gen_1089
<s, s>(q_gen_1090) -> q_gen_1089
<s, s>(q_gen_1086) -> q_gen_1090
<z, s>(q_gen_1091) -> q_gen_1090
}

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

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

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

Teacher's answer:
New clause system:
{
() -> double([z, z]) -> 7
() -> is_even([z]) -> 7
(double([n, _sf])) -> is_even([_sf]) -> 12
(double([nn, _of])) -> double([s(nn), s(s(_of))]) -> 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, _sf])) -> is_even([_sf]), {
_sf -> s(s(s(z)))  ;  n -> s(s(s(z)))
})

Total time: 0.073207
Reason for stopping: Proved