Solving ../../benchmarks/smtlib/true/leq_leq_eq.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:
{
(eqnat, P:
{
eqnat(z, z) <= True
eqnat(s(x2), s(y2)) <= eqnat(x2, y2)
eqnat(x2, y2) <= eqnat(s(x2), s(y2))
False <= eqnat(s(x2), z)
False <= eqnat(z, s(u))
}
)
(leq, P:
{
leq(z, y) <= True
leq(s(z), s(x2)) <= leq(z, x2)
leq(z, x2) <= leq(s(z), s(x2))
False <= leq(s(z), z)
}
)
}

properties:
{
eqnat(n, m) <= leq(m, n) /\ leq(n, m)
}


over-approximation: {leq}
under-approximation: {eqnat}

Clause system for inference is:

{
leq(z, y) <= True -> 0
eqnat(s(x2), s(y2)) <= eqnat(x2, y2) -> 0
eqnat(x2, y2) <= eqnat(s(x2), s(y2)) -> 0
False <= eqnat(s(x2), z) -> 0
False <= eqnat(z, s(u)) -> 0
eqnat(n, m) <= leq(m, n) /\ leq(n, m) -> 0
leq(s(z), s(x2)) <= leq(z, x2) -> 0
leq(z, x2) <= leq(s(z), s(x2)) -> 0
}


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

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


;
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
}
]



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

Clauses:
{
leq(z, y) <= True -> 0
eqnat(s(x2), s(y2)) <= eqnat(x2, y2) -> 0
eqnat(x2, y2) <= eqnat(s(x2), s(y2)) -> 0
False <= eqnat(s(x2), z) -> 0
False <= eqnat(z, s(u)) -> 0
eqnat(n, m) <= leq(m, n) /\ leq(n, m) -> 0
leq(s(z), s(x2)) <= leq(z, x2) -> 0
leq(z, x2) <= leq(s(z), s(x2)) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

eqnat(s(x2), s(y2)) <= eqnat(x2, y2)  :
No: ()

eqnat(x2, y2) <= eqnat(s(x2), s(y2))  :
No: ()

False <= eqnat(s(x2), z)  :
No: ()

False <= eqnat(z, s(u))  :
No: ()

eqnat(n, m) <= leq(m, n) /\ leq(n, m)  :
No: ()

leq(s(z), s(x2)) <= leq(z, x2)  :
No: ()

leq(z, x2) <= leq(s(z), s(x2))  :
No: ()


-------------------------------------------
Step 1, which took 0.007580 s (model generation: 0.007474,  model checking: 0.000106):

Clauses:
{
leq(z, y) <= True -> 0
eqnat(s(x2), s(y2)) <= eqnat(x2, y2) -> 0
eqnat(x2, y2) <= eqnat(s(x2), s(y2)) -> 0
False <= eqnat(s(x2), z) -> 0
False <= eqnat(z, s(u)) -> 0
eqnat(n, m) <= leq(m, n) /\ leq(n, m) -> 0
leq(s(z), s(x2)) <= leq(z, x2) -> 0
leq(z, x2) <= leq(s(z), s(x2)) -> 0
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

leq(z, y) <= True  :
Yes: {
y -> s(_oofs_0)
}

eqnat(s(x2), s(y2)) <= eqnat(x2, y2)  :
No: ()

eqnat(x2, y2) <= eqnat(s(x2), s(y2))  :
No: ()

False <= eqnat(s(x2), z)  :
No: ()

False <= eqnat(z, s(u))  :
No: ()

eqnat(n, m) <= leq(m, n) /\ leq(n, m)  :
Yes: {
m -> z  ;  n -> z
}

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

leq(z, x2) <= leq(s(z), s(x2))  :
No: ()


-------------------------------------------
Step 2, which took 0.008498 s (model generation: 0.008383,  model checking: 0.000115):

Clauses:
{
leq(z, y) <= True -> 0
eqnat(s(x2), s(y2)) <= eqnat(x2, y2) -> 0
eqnat(x2, y2) <= eqnat(s(x2), s(y2)) -> 0
False <= eqnat(s(x2), z) -> 0
False <= eqnat(z, s(u)) -> 0
eqnat(n, m) <= leq(m, n) /\ leq(n, m) -> 0
leq(s(z), s(x2)) <= leq(z, x2) -> 0
leq(z, x2) <= leq(s(z), s(x2)) -> 0
}

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

Current best model:
|_
name: None

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


;
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
}
]



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




Answer of teacher:

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

eqnat(s(x2), s(y2)) <= eqnat(x2, y2)  :
Yes: {
x2 -> z  ;  y2 -> z
}

eqnat(x2, y2) <= eqnat(s(x2), s(y2))  :
No: ()

False <= eqnat(s(x2), z)  :
No: ()

False <= eqnat(z, s(u))  :
No: ()

eqnat(n, m) <= leq(m, n) /\ leq(n, m)  :
Yes: {
m -> s(_vofs_0)  ;  n -> s(_wofs_0)
}

leq(s(z), s(x2)) <= leq(z, x2)  :
No: ()

leq(z, x2) <= leq(s(z), s(x2))  :
Yes: {
x2 -> z  ;  z -> s(_yofs_0)
}


-------------------------------------------
Step 3, which took 0.017518 s (model generation: 0.017408,  model checking: 0.000110):

Clauses:
{
leq(z, y) <= True -> 0
eqnat(s(x2), s(y2)) <= eqnat(x2, y2) -> 0
eqnat(x2, y2) <= eqnat(s(x2), s(y2)) -> 0
False <= eqnat(s(x2), z) -> 0
False <= eqnat(z, s(u)) -> 0
eqnat(n, m) <= leq(m, n) /\ leq(n, m) -> 0
leq(s(z), s(x2)) <= leq(z, x2) -> 0
leq(z, x2) <= leq(s(z), s(x2)) -> 0
}

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

Current best model:
|_
name: None

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


;
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
}
]



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




Answer of teacher:

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

eqnat(s(x2), s(y2)) <= eqnat(x2, y2)  :
No: ()

eqnat(x2, y2) <= eqnat(s(x2), s(y2))  :
Yes: {
x2 -> z  ;  y2 -> s(_cpfs_0)
}

False <= eqnat(s(x2), z)  :
No: ()

False <= eqnat(z, s(u))  :
No: ()

eqnat(n, m) <= leq(m, n) /\ leq(n, m)  :
Yes: {
m -> z  ;  n -> s(_epfs_0)
}

leq(s(z), s(x2)) <= leq(z, x2)  :
No: ()

leq(z, x2) <= leq(s(z), s(x2))  :
No: ()


-------------------------------------------
Step 4, which took 0.009713 s (model generation: 0.009634,  model checking: 0.000079):

Clauses:
{
leq(z, y) <= True -> 0
eqnat(s(x2), s(y2)) <= eqnat(x2, y2) -> 0
eqnat(x2, y2) <= eqnat(s(x2), s(y2)) -> 0
False <= eqnat(s(x2), z) -> 0
False <= eqnat(z, s(u)) -> 0
eqnat(n, m) <= leq(m, n) /\ leq(n, m) -> 0
leq(s(z), s(x2)) <= leq(z, x2) -> 0
leq(z, x2) <= leq(s(z), s(x2)) -> 0
}

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

Current best model:
|_
name: None

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


;
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
}
]



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




Answer of teacher:

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

eqnat(s(x2), s(y2)) <= eqnat(x2, y2)  :
No: ()

eqnat(x2, y2) <= eqnat(s(x2), s(y2))  :
No: ()

False <= eqnat(s(x2), z)  :
Yes: {

}

False <= eqnat(z, s(u))  :
Yes: {

}

eqnat(n, m) <= leq(m, n) /\ leq(n, m)  :
No: ()

leq(s(z), s(x2)) <= leq(z, x2)  :
No: ()

leq(z, x2) <= leq(s(z), s(x2))  :
No: ()


-------------------------------------------
Step 5, which took 0.008791 s (model generation: 0.007904,  model checking: 0.000887):

Clauses:
{
leq(z, y) <= True -> 0
eqnat(s(x2), s(y2)) <= eqnat(x2, y2) -> 0
eqnat(x2, y2) <= eqnat(s(x2), s(y2)) -> 0
False <= eqnat(s(x2), z) -> 0
False <= eqnat(z, s(u)) -> 0
eqnat(n, m) <= leq(m, n) /\ leq(n, m) -> 0
leq(s(z), s(x2)) <= leq(z, x2) -> 0
leq(z, x2) <= leq(s(z), s(x2)) -> 0
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

eqnat(s(x2), s(y2)) <= eqnat(x2, y2)  :
No: ()

eqnat(x2, y2) <= eqnat(s(x2), s(y2))  :
No: ()

False <= eqnat(s(x2), z)  :
No: ()

False <= eqnat(z, s(u))  :
No: ()

eqnat(n, m) <= leq(m, n) /\ leq(n, m)  :
No: ()

leq(s(z), s(x2)) <= leq(z, x2)  :
Yes: {
x2 -> s(_vpfs_0)  ;  z -> z
}

leq(z, x2) <= leq(s(z), s(x2))  :
No: ()


Total time: 0.071136
Learner time: 0.057198
Teacher time: 0.001407
Reasons for stopping: Yes: |_
name: None

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


;
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
}
]



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