Solving ../../benchmarks/smtlib/true/isaplanner_prop24.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: Some(60.) (sec)
Teacher_type: Checks all clauses every time
Approximation method: remove every clause that can be safely removed



Learning problem is:

env: {
nat -> {s, z}
}
definition:
{
(leq, P:
{
leq(z, n2) <= True
leq(s(nn1), s(nn2)) <= leq(nn1, nn2)
leq(nn1, nn2) <= leq(s(nn1), s(nn2))
False <= leq(s(nn1), z)
}
)
(max, F:
{
max(s(u), z, s(u)) <= True
max(z, y, y) <= True
max(s(u), s(x2), s(_rya)) <= max(u, x2, _rya)
}
eq_nat(_uya, _vya) <= max(_sya, _tya, _uya) /\ max(_sya, _tya, _vya)
)
}

properties:
{
eq_nat(_xya, i) <= leq(j, i) /\ max(i, j, _xya)
leq(j, i) <= max(i, j, i)
}


over-approximation: {max}
under-approximation: {}

Clause system for inference is:

{
leq(z, n2) <= True -> 0
max(s(u), z, s(u)) <= True -> 0
max(z, y, y) <= True -> 0
eq_nat(_xya, i) <= leq(j, i) /\ max(i, j, _xya) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
leq(j, i) <= max(i, j, i) -> 0
max(s(u), s(x2), s(_rya)) <= max(u, x2, _rya) -> 0
}


Solving took 0.083934 seconds.
Yes: |_
name: None

leq ->
[
leq : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0)
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]


;
max ->
[
max : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= True
  max(s(x_0_0), s(x_1_0), s(x_2_0)) <= max(x_0_0, x_1_0, x_2_0)
  max(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  max(z, s(x_1_0), s(x_2_0)) <= True
  max(z, z, z) <= True
}
]



--
Equality automata are defined for: {nat}
_|
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005762 s (model generation: 0.005706,  model checking: 0.000056):

Clauses:
{
leq(z, n2) <= True -> 0
max(s(u), z, s(u)) <= True -> 0
max(z, y, y) <= True -> 0
eq_nat(_xya, i) <= leq(j, i) /\ max(i, j, _xya) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
leq(j, i) <= max(i, j, i) -> 0
max(s(u), s(x2), s(_rya)) <= max(u, x2, _rya) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

leq ->
[
leq : <nat * nat>
{
  
}
]


;
max ->
[
max : <nat * nat * nat>
{
  
}
]



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




Answer of teacher:

leq(z, n2) <= True  :
Yes: {
n2 -> z
}

max(s(u), z, s(u)) <= True  :
Yes: {

}

max(z, y, y) <= True  :
Yes: {
y -> z
}

eq_nat(_xya, i) <= leq(j, i) /\ max(i, j, _xya)  :
No: ()

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
No: ()

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
No: ()

leq(j, i) <= max(i, j, i)  :
No: ()

max(s(u), s(x2), s(_rya)) <= max(u, x2, _rya)  :
No: ()


-------------------------------------------
Step 1, which took 0.006802 s (model generation: 0.006724,  model checking: 0.000078):

Clauses:
{
leq(z, n2) <= True -> 0
max(s(u), z, s(u)) <= True -> 0
max(z, y, y) <= True -> 0
eq_nat(_xya, i) <= leq(j, i) /\ max(i, j, _xya) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
leq(j, i) <= max(i, j, i) -> 0
max(s(u), s(x2), s(_rya)) <= max(u, x2, _rya) -> 0
}

Accumulated learning constraints:
{
leq(z, z) <= True
max(s(z), z, s(z)) <= True
max(z, z, z) <= True
}

Current best model:
|_
name: None

leq ->
[
leq : <nat * nat>
{
  leq(z, z) <= True
}
]


;
max ->
[
max : <nat * nat * nat>
{
  max(s(x_0_0), z, s(x_2_0)) <= True
  max(z, z, z) <= True
}
]



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




Answer of teacher:

leq(z, n2) <= True  :
Yes: {
n2 -> s(_kzze_0)
}

max(s(u), z, s(u)) <= True  :
No: ()

max(z, y, y) <= True  :
Yes: {
y -> s(_lzze_0)
}

eq_nat(_xya, i) <= leq(j, i) /\ max(i, j, _xya)  :
No: ()

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
Yes: {
nn1 -> z  ;  nn2 -> z
}

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
No: ()

leq(j, i) <= max(i, j, i)  :
Yes: {
i -> s(_ozze_0)  ;  j -> z
}

max(s(u), s(x2), s(_rya)) <= max(u, x2, _rya)  :
Yes: {
_rya -> z  ;  u -> z  ;  x2 -> z
}


-------------------------------------------
Step 2, which took 0.007460 s (model generation: 0.007311,  model checking: 0.000149):

Clauses:
{
leq(z, n2) <= True -> 0
max(s(u), z, s(u)) <= True -> 0
max(z, y, y) <= True -> 0
eq_nat(_xya, i) <= leq(j, i) /\ max(i, j, _xya) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
leq(j, i) <= max(i, j, i) -> 0
max(s(u), s(x2), s(_rya)) <= max(u, x2, _rya) -> 0
}

Accumulated learning constraints:
{
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
}

Current best model:
|_
name: None

leq ->
[
leq : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= True
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]


;
max ->
[
max : <nat * nat * nat>
{
  max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  max(s(x_0_0), z, s(x_2_0)) <= True
  max(z, s(x_1_0), s(x_2_0)) <= True
  max(z, z, z) <= True
}
]



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




Answer of teacher:

leq(z, n2) <= True  :
No: ()

max(s(u), z, s(u)) <= True  :
No: ()

max(z, y, y) <= True  :
No: ()

eq_nat(_xya, i) <= leq(j, i) /\ max(i, j, _xya)  :
Yes: {
_xya -> s(z)  ;  i -> s(s(_jaaf_0))  ;  j -> z
}

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
No: ()

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
Yes: {
nn1 -> s(_caaf_0)  ;  nn2 -> z
}

False <= leq(s(nn1), z)  :
No: ()

leq(j, i) <= max(i, j, i)  :
No: ()

max(s(u), s(x2), s(_rya)) <= max(u, x2, _rya)  :
No: ()


-------------------------------------------
Step 3, which took 0.008742 s (model generation: 0.008158,  model checking: 0.000584):

Clauses:
{
leq(z, n2) <= True -> 0
max(s(u), z, s(u)) <= True -> 0
max(z, y, y) <= True -> 0
eq_nat(_xya, i) <= leq(j, i) /\ max(i, j, _xya) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
leq(j, i) <= max(i, j, i) -> 0
max(s(u), s(x2), s(_rya)) <= max(u, x2, _rya) -> 0
}

Accumulated learning constraints:
{
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
leq(s(z), z) <= leq(s(s(z)), s(z))
False <= leq(z, s(s(z))) /\ max(s(s(z)), z, s(z))
}

Current best model:
|_
name: None

leq ->
[
leq : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0)
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]


;
max ->
[
max : <nat * nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0)
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
  max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  max(s(x_0_0), z, s(x_2_0)) <= leq(x_0_0, x_2_0)
  max(z, s(x_1_0), s(x_2_0)) <= True
  max(z, z, z) <= True
}
]



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




Answer of teacher:

leq(z, n2) <= True  :
No: ()

max(s(u), z, s(u)) <= True  :
No: ()

max(z, y, y) <= True  :
No: ()

eq_nat(_xya, i) <= leq(j, i) /\ max(i, j, _xya)  :
Yes: {
_xya -> s(s(_rbaf_0))  ;  i -> s(z)  ;  j -> s(z)
}

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
No: ()

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
No: ()

leq(j, i) <= max(i, j, i)  :
Yes: {
i -> s(z)  ;  j -> s(s(_ubaf_0))
}

max(s(u), s(x2), s(_rya)) <= max(u, x2, _rya)  :
No: ()


-------------------------------------------
Step 4, which took 0.009459 s (model generation: 0.009072,  model checking: 0.000387):

Clauses:
{
leq(z, n2) <= True -> 0
max(s(u), z, s(u)) <= True -> 0
max(z, y, y) <= True -> 0
eq_nat(_xya, i) <= leq(j, i) /\ max(i, j, _xya) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
leq(j, i) <= max(i, j, i) -> 0
max(s(u), s(x2), s(_rya)) <= max(u, x2, _rya) -> 0
}

Accumulated learning constraints:
{
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
leq(s(z), z) <= leq(s(s(z)), s(z))
False <= leq(z, s(s(z))) /\ max(s(s(z)), z, s(z))
leq(s(s(z)), s(z)) <= max(s(z), s(s(z)), s(z))
False <= max(s(z), s(z), s(s(z)))
}

Current best model:
|_
name: None

leq ->
[
leq : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0)
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]


;
max ->
[
max : <nat * nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0)
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
  max(s(x_0_0), s(x_1_0), s(x_2_0)) <= max(x_0_0, x_1_0, x_2_0)
  max(s(x_0_0), z, s(x_2_0)) <= leq(x_0_0, x_2_0)
  max(z, s(x_1_0), s(x_2_0)) <= True
  max(z, z, z) <= True
}
]



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




Answer of teacher:

leq(z, n2) <= True  :
No: ()

max(s(u), z, s(u)) <= True  :
No: ()

max(z, y, y) <= True  :
No: ()

eq_nat(_xya, i) <= leq(j, i) /\ max(i, j, _xya)  :
Yes: {
_xya -> s(s(_edaf_0))  ;  i -> s(z)  ;  j -> z
}

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
No: ()

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
No: ()

leq(j, i) <= max(i, j, i)  :
No: ()

max(s(u), s(x2), s(_rya)) <= max(u, x2, _rya)  :
No: ()


-------------------------------------------
Step 5, which took 0.012159 s (model generation: 0.012049,  model checking: 0.000110):

Clauses:
{
leq(z, n2) <= True -> 0
max(s(u), z, s(u)) <= True -> 0
max(z, y, y) <= True -> 0
eq_nat(_xya, i) <= leq(j, i) /\ max(i, j, _xya) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
leq(j, i) <= max(i, j, i) -> 0
max(s(u), s(x2), s(_rya)) <= max(u, x2, _rya) -> 0
}

Accumulated learning constraints:
{
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
leq(s(z), z) <= leq(s(s(z)), s(z))
False <= leq(z, s(s(z))) /\ max(s(s(z)), z, s(z))
leq(s(s(z)), s(z)) <= max(s(z), s(s(z)), s(z))
False <= max(s(z), s(z), s(s(z)))
False <= max(s(z), z, s(s(z)))
}

Current best model:
|_
name: None

leq ->
[
leq : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= True
  leq(s(x_0_0), z) <= True
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]


;
max ->
[
max : <nat * nat * nat>
{
  _r_1(z, z) <= True
  max(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  max(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  max(z, s(x_1_0), s(x_2_0)) <= True
  max(z, z, z) <= True
}
]



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




Answer of teacher:

leq(z, n2) <= True  :
No: ()

max(s(u), z, s(u)) <= True  :
Yes: {
u -> s(_meaf_0)
}

max(z, y, y) <= True  :
No: ()

eq_nat(_xya, i) <= leq(j, i) /\ max(i, j, _xya)  :
Yes: {
_xya -> s(_udaf_0)  ;  i -> z  ;  j -> s(_wdaf_0)
}

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
No: ()

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
No: ()

False <= leq(s(nn1), z)  :
Yes: {

}

leq(j, i) <= max(i, j, i)  :
No: ()

max(s(u), s(x2), s(_rya)) <= max(u, x2, _rya)  :
Yes: {
_rya -> s(_geaf_0)  ;  u -> z  ;  x2 -> s(_ieaf_0)
}


-------------------------------------------
Step 6, which took 0.014901 s (model generation: 0.014678,  model checking: 0.000223):

Clauses:
{
leq(z, n2) <= True -> 0
max(s(u), z, s(u)) <= True -> 0
max(z, y, y) <= True -> 0
eq_nat(_xya, i) <= leq(j, i) /\ max(i, j, _xya) -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
leq(j, i) <= max(i, j, i) -> 0
max(s(u), s(x2), s(_rya)) <= max(u, x2, _rya) -> 0
}

Accumulated learning constraints:
{
leq(s(z), s(z)) <= True
leq(z, s(z)) <= True
leq(z, z) <= True
max(s(s(z)), z, s(s(z))) <= True
max(s(z), s(s(z)), s(s(z))) <= True
max(s(z), s(z), s(z)) <= True
max(s(z), z, s(z)) <= True
max(z, s(z), s(z)) <= True
max(z, z, z) <= True
False <= leq(s(s(z)), s(z))
False <= leq(s(z), z)
False <= leq(z, s(s(z))) /\ max(s(s(z)), z, s(z))
False <= max(s(z), s(s(z)), s(z))
False <= max(s(z), s(z), s(s(z)))
False <= max(s(z), z, s(s(z)))
}

Current best model:
|_
name: None

leq ->
[
leq : <nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= True
  _r_1(z, z) <= True
  leq(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]


;
max ->
[
max : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= True
  _r_1(z, z) <= True
  max(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  max(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  max(z, s(x_1_0), s(x_2_0)) <= True
  max(z, z, z) <= True
}
]



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




Answer of teacher:

leq(z, n2) <= True  :
No: ()

max(s(u), z, s(u)) <= True  :
No: ()

max(z, y, y) <= True  :
No: ()

eq_nat(_xya, i) <= leq(j, i) /\ max(i, j, _xya)  :
Yes: {
_xya -> s(s(z))  ;  i -> s(s(s(_yfaf_0)))  ;  j -> z
}

leq(s(nn1), s(nn2)) <= leq(nn1, nn2)  :
Yes: {
nn1 -> z  ;  nn2 -> s(_weaf_0)
}

leq(nn1, nn2) <= leq(s(nn1), s(nn2))  :
Yes: {
nn1 -> s(z)  ;  nn2 -> s(s(_cgaf_0))
}

False <= leq(s(nn1), z)  :
No: ()

leq(j, i) <= max(i, j, i)  :
No: ()

max(s(u), s(x2), s(_rya)) <= max(u, x2, _rya)  :
Yes: {
_rya -> s(z)  ;  u -> s(z)  ;  x2 -> z
}


Total time: 0.083934
Learner time: 0.063698
Teacher time: 0.001587
Reasons for stopping: Yes: |_
name: None

leq ->
[
leq : <nat * nat>
{
  leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0)
  leq(z, s(x_1_0)) <= True
  leq(z, z) <= True
}
]


;
max ->
[
max : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= True
  max(s(x_0_0), s(x_1_0), s(x_2_0)) <= max(x_0_0, x_1_0, x_2_0)
  max(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  max(z, s(x_1_0), s(x_2_0)) <= True
  max(z, z, z) <= True
}
]



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