Solving ../../benchmarks/smtlib/true/isaplanner_prop54.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:
{
(minus, F:
{
minus(s(u), z, s(u)) <= True
minus(z, y, z) <= True
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed)
}
eq_nat(_hd, _id) <= minus(_fd, _gd, _hd) /\ minus(_fd, _gd, _id)
)
(plus, F:
{
plus(n, z, n) <= True
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd)
}
eq_nat(_md, _nd) <= plus(_kd, _ld, _md) /\ plus(_kd, _ld, _nd)
)
}

properties:
{
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od)
}


over-approximation: {minus, plus}
under-approximation: {}

Clause system for inference is:

{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od) -> 0
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed) -> 0
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd) -> 0
}


Solving took 60.829166 seconds.
Maybe:  timeout during teacher: {
minus(s(u), z, s(u)) <= True -> out of time
minus(z, y, z) <= True -> out of time
plus(n, z, n) <= True -> out of time
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od) -> out of time
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed) -> out of time
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd) -> out of time
}Last solver state:

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od) -> 0
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed) -> 0
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd) -> 0
}

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

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_2(x_1_0)
  _r_1(s(x_0_0), s(x_1_0)) <= _r_3(x_0_0)
  _r_1(s(x_0_0), z) <= _r_2(x_0_0)
  _r_1(z, s(x_1_0)) <= _r_2(x_1_0)
  _r_1(z, z) <= True
  _r_2(s(x_0_0)) <= True
  _r_3(z) <= True
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_0_0) /\ _r_3(x_2_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0) /\ _r_3(x_1_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_1_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_3(x_0_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  minus(z, s(x_1_0), z) <= True
  minus(z, z, z) <= True
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_2(x_1_0)
  _r_1(s(x_0_0), s(x_1_0)) <= _r_3(x_0_0)
  _r_1(s(x_0_0), z) <= _r_2(x_0_0)
  _r_1(z, s(x_1_0)) <= _r_2(x_1_0)
  _r_1(z, z) <= True
  _r_2(s(x_0_0)) <= True
  _r_3(z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_2_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_2_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



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






-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006071 s (model generation: 0.006007,  model checking: 0.000064):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od) -> 0
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed) -> 0
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

}

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

plus(n, z, n) <= True  :
Yes: {
n -> z
}

eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od)  :
No: ()

minus(s(u), s(x2), _ed) <= minus(u, x2, _ed)  :
No: ()

plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd)  :
No: ()


-------------------------------------------
Step 1, which took 0.006668 s (model generation: 0.006579,  model checking: 0.000089):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od) -> 0
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed) -> 0
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd) -> 0
}

Accumulated learning constraints:
{
minus(s(z), z, s(z)) <= True
minus(z, z, z) <= True
plus(z, z, z) <= True
}

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

minus(z, y, z) <= True  :
Yes: {
y -> s(_bodk_0)
}

plus(n, z, n) <= True  :
Yes: {
n -> s(_codk_0)
}

eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od)  :
No: ()

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

plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd)  :
Yes: {
_jd -> z  ;  mm -> z  ;  n -> z
}


-------------------------------------------
Step 2, which took 0.011616 s (model generation: 0.011518,  model checking: 0.000098):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od) -> 0
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed) -> 0
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd) -> 0
}

Accumulated learning constraints:
{
minus(s(z), s(z), z) <= True
minus(s(z), z, s(z)) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
}

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

plus(n, z, n) <= True  :
No: ()

eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od)  :
Yes: {
_od -> s(_modk_0)  ;  _pd -> s(z)  ;  m -> s(s(_bpdk_0))  ;  n -> z
}

minus(s(u), s(x2), _ed) <= minus(u, x2, _ed)  :
Yes: {
_ed -> s(_qodk_0)  ;  u -> s(_rodk_0)  ;  x2 -> z
}

plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd)  :
Yes: {
_jd -> s(_todk_0)  ;  mm -> z  ;  n -> s(_vodk_0)
}


-------------------------------------------
Step 3, which took 0.016990 s (model generation: 0.016892,  model checking: 0.000098):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od) -> 0
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed) -> 0
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd) -> 0
}

Accumulated learning constraints:
{
minus(s(s(z)), s(z), s(z)) <= True
minus(s(z), s(z), z) <= True
minus(s(z), z, s(z)) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= plus(s(s(z)), z, s(z))
}

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

plus(n, z, n) <= True  :
Yes: {
n -> s(s(_tpdk_0))
}

eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od)  :
Yes: {
_od -> s(_lpdk_0)  ;  _pd -> z  ;  m -> s(_npdk_0)  ;  n -> s(_opdk_0)
}

minus(s(u), s(x2), _ed) <= minus(u, x2, _ed)  :
No: ()

plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd)  :
No: ()


-------------------------------------------
Step 4, which took 0.027926 s (model generation: 0.027797,  model checking: 0.000129):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od) -> 0
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed) -> 0
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd) -> 0
}

Accumulated learning constraints:
{
minus(s(s(z)), s(z), s(z)) <= True
minus(s(z), s(z), z) <= True
minus(s(z), z, s(z)) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
plus(s(s(z)), z, s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= plus(s(s(z)), z, s(z))
False <= plus(s(z), s(z), s(z))
}

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

plus(n, z, n) <= True  :
No: ()

eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od)  :
Yes: {
_od -> s(_zpdk_0)  ;  _pd -> s(_aqdk_0)  ;  m -> z  ;  n -> s(_cqdk_0)
}

minus(s(u), s(x2), _ed) <= minus(u, x2, _ed)  :
No: ()

plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd)  :
No: ()


-------------------------------------------
Step 5, which took 0.023336 s (model generation: 0.023190,  model checking: 0.000146):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od) -> 0
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed) -> 0
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd) -> 0
}

Accumulated learning constraints:
{
minus(s(s(z)), s(z), s(z)) <= True
minus(s(z), s(z), z) <= True
minus(s(z), z, s(z)) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
plus(s(s(z)), z, s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= minus(s(z), s(z), s(z))
False <= plus(s(s(z)), z, s(z))
False <= plus(s(z), s(z), s(z))
}

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

plus(n, z, n) <= True  :
No: ()

eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od)  :
Yes: {
_od -> s(s(_esdk_0))  ;  _pd -> z  ;  m -> s(z)  ;  n -> s(_krdk_0)
}

minus(s(u), s(x2), _ed) <= minus(u, x2, _ed)  :
Yes: {
_ed -> s(s(_fsdk_0))  ;  u -> s(_trdk_0)  ;  x2 -> z
}

plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd)  :
Yes: {
_jd -> s(z)  ;  mm -> s(_wrdk_0)  ;  n -> s(s(_gsdk_0))
}


-------------------------------------------
Step 6, which took 0.039047 s (model generation: 0.038739,  model checking: 0.000308):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od) -> 0
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed) -> 0
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd) -> 0
}

Accumulated learning constraints:
{
minus(s(s(z)), s(z), s(z)) <= True
minus(s(z), s(z), z) <= True
minus(s(z), z, s(z)) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
plus(s(s(z)), z, s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= minus(s(s(z)), s(z), z)
False <= minus(s(z), s(z), s(z))
minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), z, s(s(z)))
plus(s(s(z)), s(s(z)), s(s(z))) <= plus(s(s(z)), s(z), s(z))
False <= plus(s(s(z)), z, s(z))
False <= plus(s(z), s(z), s(z))
}

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

plus(n, z, n) <= True  :
No: ()

eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od)  :
Yes: {
_od -> s(s(_budk_0))  ;  _pd -> s(_osdk_0)  ;  m -> z  ;  n -> s(_qsdk_0)
}

minus(s(u), s(x2), _ed) <= minus(u, x2, _ed)  :
Yes: {
_ed -> z  ;  u -> s(z)  ;  x2 -> s(_itdk_0)
}

plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd)  :
No: ()


-------------------------------------------
Step 7, which took 0.039552 s (model generation: 0.039227,  model checking: 0.000325):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od) -> 0
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed) -> 0
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd) -> 0
}

Accumulated learning constraints:
{
minus(s(s(z)), s(s(z)), z) <= True
minus(s(s(z)), s(z), s(z)) <= True
minus(s(z), s(z), z) <= True
minus(s(z), z, s(z)) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
plus(s(s(z)), z, s(s(z))) <= True
plus(s(z), s(z), s(s(z))) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
False <= minus(s(s(z)), s(z), z)
False <= minus(s(z), s(z), s(z))
minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), z, s(s(z)))
plus(s(s(z)), s(s(z)), s(s(z))) <= plus(s(s(z)), s(z), s(z))
False <= plus(s(s(z)), z, s(z))
False <= plus(s(z), s(z), s(z))
False <= plus(z, s(z), s(s(z)))
}

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

plus(n, z, n) <= True  :
No: ()

eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od)  :
Yes: {
_od -> s(z)  ;  _pd -> s(z)  ;  m -> s(s(_bwdk_0))  ;  n -> s(s(_fwdk_0))
}

minus(s(u), s(x2), _ed) <= minus(u, x2, _ed)  :
Yes: {
_ed -> z  ;  u -> z  ;  x2 -> s(_gvdk_0)
}

plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd)  :
Yes: {
_jd -> s(s(_jwdk_0))  ;  mm -> s(z)  ;  n -> s(_mvdk_0)
}


-------------------------------------------
Step 8, which took 0.046979 s (model generation: 0.046685,  model checking: 0.000294):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od) -> 0
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed) -> 0
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd) -> 0
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

plus(n, z, n) <= True  :
No: ()

eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od)  :
Yes: {
_od -> s(s(_sydk_0))  ;  _pd -> z  ;  m -> s(_zwdk_0)  ;  n -> s(s(_qydk_0))
}

minus(s(u), s(x2), _ed) <= minus(u, x2, _ed)  :
No: ()

plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd)  :
Yes: {
_jd -> s(z)  ;  mm -> s(_lydk_0)  ;  n -> z
}


-------------------------------------------
Step 9, which took 0.051015 s (model generation: 0.050257,  model checking: 0.000758):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od) -> 0
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed) -> 0
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd) -> 0
}

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

Current best model:
|_
name: None

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


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



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




Answer of teacher:

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

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

plus(n, z, n) <= True  :
No: ()

eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od)  :
Yes: {
_od -> s(s(_idek_0))  ;  _pd -> s(_izdk_0)  ;  m -> z  ;  n -> s(s(_jdek_0))
}

minus(s(u), s(x2), _ed) <= minus(u, x2, _ed)  :
No: ()

plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd)  :
No: ()


-------------------------------------------
Step 10, which took 0.050946 s (model generation: 0.050124,  model checking: 0.000822):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od) -> 0
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed) -> 0
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd) -> 0
}

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

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(s(x_0_0)) <= True
  _r_2(s(x_0_0)) <= _r_1(x_0_0)
  _r_2(z) <= True
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) /\ _r_2(x_1_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_1_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_0_0)
  minus(s(x_0_0), z, s(x_2_0)) <= True
  minus(z, s(x_1_0), z) <= True
  minus(z, z, z) <= True
}
]


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



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




Answer of teacher:

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

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

plus(n, z, n) <= True  :
No: ()

eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od)  :
Yes: {
_od -> s(s(_hiek_0))  ;  _pd -> s(z)  ;  m -> s(s(_riek_0))  ;  n -> z
}

minus(s(u), s(x2), _ed) <= minus(u, x2, _ed)  :
Yes: {
_ed -> s(_gfek_0)  ;  u -> s(s(_giek_0))  ;  x2 -> s(z)
}

plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd)  :
No: ()


-------------------------------------------
Step 11, which took 0.062529 s (model generation: 0.061288,  model checking: 0.001241):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od) -> 0
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed) -> 0
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd) -> 0
}

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

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(s(x_0_0)) <= True
  _r_2(s(x_0_0)) <= _r_1(x_0_0)
  _r_2(z) <= True
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) /\ _r_2(x_1_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0) /\ _r_2(x_0_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_1_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_0_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0)
  minus(z, s(x_1_0), z) <= True
  minus(z, z, z) <= True
}
]


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



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




Answer of teacher:

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

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

plus(n, z, n) <= True  :
No: ()

eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od)  :
Yes: {
_od -> s(z)  ;  _pd -> z  ;  m -> s(z)  ;  n -> s(s(_eqek_0))
}

minus(s(u), s(x2), _ed) <= minus(u, x2, _ed)  :
No: ()

plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd)  :
Yes: {
_jd -> s(s(_eqek_0))  ;  mm -> s(z)  ;  n -> s(s(z))
}


-------------------------------------------
Step 12, which took 0.088883 s (model generation: 0.087472,  model checking: 0.001411):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od) -> 0
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed) -> 0
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd) -> 0
}

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

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= True
  _r_1(s(x_0_0), z) <= _r_2(x_0_0)
  _r_1(z, s(x_1_0)) <= _r_2(x_1_0)
  _r_1(z, z) <= True
  _r_2(s(x_0_0)) <= True
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_0_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_2(x_0_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0, x_1_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_1_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  minus(z, s(x_1_0), z) <= True
  minus(z, z, z) <= True
}
]


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



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




Answer of teacher:

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

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

plus(n, z, n) <= True  :
No: ()

eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od)  :
Yes: {
_od -> s(s(s(_xwek_0)))  ;  _pd -> z  ;  m -> s(z)  ;  n -> s(s(_gwek_0))
}

minus(s(u), s(x2), _ed) <= minus(u, x2, _ed)  :
No: ()

plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd)  :
No: ()


-------------------------------------------
Step 13, which took 0.442956 s (model generation: 0.442405,  model checking: 0.000551):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od) -> 0
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed) -> 0
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd) -> 0
}

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

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= True
  _r_1(z, z) <= True
  _r_2(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0, x_1_0)
  _r_2(s(x_0_0), z) <= True
  _r_2(z, s(x_1_0)) <= True
  _r_3(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_3(z, s(x_1_0)) <= True
  _r_3(z, z) <= True
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0, x_1_0) /\ _r_2(x_0_0, x_2_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0, x_1_0) /\ _r_3(x_1_0, x_2_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_3(x_0_0, x_1_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_3(x_0_0, x_2_0)
  minus(z, s(x_1_0), z) <= True
  minus(z, z, z) <= True
}
]


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



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




Answer of teacher:

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

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

plus(n, z, n) <= True  :
No: ()

eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od)  :
Yes: {
_od -> s(s(z))  ;  _pd -> s(z)  ;  m -> z  ;  n -> s(s(s(_zbfk_0)))
}

minus(s(u), s(x2), _ed) <= minus(u, x2, _ed)  :
Yes: {
_ed -> z  ;  u -> s(z)  ;  x2 -> s(s(_dcfk_0))
}

plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd)  :
Yes: {
_jd -> s(z)  ;  mm -> s(s(_rcfk_0))  ;  n -> s(s(z))
}


-------------------------------------------
Step 14, which took 1.430986 s (model generation: 1.430136,  model checking: 0.000850):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od) -> 0
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed) -> 0
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd) -> 0
}

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

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(z, s(x_1_0)) <= True
  _r_1(z, z) <= True
  _r_2(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_2(z, z) <= True
  _r_3(s(x_0_0), s(x_1_0)) <= _r_3(x_0_0, x_1_0)
  _r_3(s(x_0_0), z) <= True
  _r_3(z, s(x_1_0)) <= True
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_3(x_0_0, x_1_0) /\ _r_3(x_0_0, x_2_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0, x_1_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_0_0, x_1_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0, x_2_0)
  minus(z, s(x_1_0), z) <= True
  minus(z, z, z) <= True
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(z, s(x_1_0)) <= True
  _r_1(z, z) <= True
  _r_2(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_2(z, z) <= True
  _r_3(s(x_0_0), s(x_1_0)) <= _r_3(x_0_0, x_1_0)
  _r_3(s(x_0_0), z) <= True
  _r_3(z, s(x_1_0)) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0, x_1_0) /\ _r_3(x_1_0, x_2_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_3(x_0_0, x_2_0) /\ _r_3(x_1_0, x_2_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0, x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_2(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



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




Answer of teacher:

minus(s(u), z, s(u)) <= True  :
Yes: {
u -> s(s(_tgfk_0))
}

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

plus(n, z, n) <= True  :
Yes: {
n -> s(s(s(_ugfk_0)))
}

eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od)  :
Yes: {
_od -> s(z)  ;  _pd -> z  ;  m -> s(s(z))  ;  n -> s(s(z))
}

minus(s(u), s(x2), _ed) <= minus(u, x2, _ed)  :
Yes: {
_ed -> s(s(z))  ;  u -> s(z)  ;  x2 -> s(s(_gifk_0))
}

plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd)  :
Yes: {
_jd -> s(s(z))  ;  mm -> s(s(z))  ;  n -> z
}


-------------------------------------------
Step 15, which took 1.697537 s (model generation: 1.696706,  model checking: 0.000831):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od) -> 0
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed) -> 0
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd) -> 0
}

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

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_3(x_1_0)
  _r_1(s(x_0_0), z) <= _r_3(x_0_0)
  _r_1(z, s(x_1_0)) <= True
  _r_2(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0, x_1_0)
  _r_2(z, z) <= True
  _r_3(s(x_0_0)) <= True
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) /\ _r_3(x_0_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_1_0, x_2_0) /\ _r_3(x_0_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0, x_1_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_0_0, x_1_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0, x_2_0)
  minus(z, s(x_1_0), z) <= True
  minus(z, z, z) <= True
}
]


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



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




Answer of teacher:

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

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

plus(n, z, n) <= True  :
No: ()

eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od)  :
Yes: {
_od -> s(s(s(_wmfk_0)))  ;  _pd -> z  ;  m -> s(_qjfk_0)  ;  n -> s(z)
}

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

plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd)  :
Yes: {
_jd -> s(z)  ;  mm -> s(s(s(_hnfk_0)))  ;  n -> s(_ylfk_0)
}


-------------------------------------------
Step 16, which took 3.713677 s (model generation: 3.712546,  model checking: 0.001131):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od) -> 0
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed) -> 0
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd) -> 0
}

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

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_3(x_1_0)
  _r_1(s(x_0_0), z) <= _r_3(x_0_0)
  _r_1(z, s(x_1_0)) <= True
  _r_2(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0, x_1_0)
  _r_2(z, z) <= True
  _r_3(s(x_0_0)) <= True
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_1_0, x_2_0) /\ _r_3(x_0_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_1_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_0_0, x_1_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0, x_2_0)
  minus(z, s(x_1_0), z) <= True
  minus(z, z, z) <= True
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_3(x_1_0)
  _r_1(s(x_0_0), z) <= _r_3(x_0_0)
  _r_1(z, s(x_1_0)) <= True
  _r_2(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0, x_1_0)
  _r_2(z, z) <= True
  _r_3(s(x_0_0)) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) /\ _r_1(x_1_0, x_2_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0, x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_2(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



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




Answer of teacher:

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

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

plus(n, z, n) <= True  :
No: ()

eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od)  :
Yes: {
_od -> s(z)  ;  _pd -> s(s(_ksfk_0))  ;  m -> z  ;  n -> s(z)
}

minus(s(u), s(x2), _ed) <= minus(u, x2, _ed)  :
No: ()

plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd)  :
Yes: {
_jd -> s(z)  ;  mm -> s(s(s(_btfk_0)))  ;  n -> s(s(s(_btfk_0)))
}


-------------------------------------------
Step 17, which took 52.037801 s (model generation: 52.036822,  model checking: 0.000979):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od) -> 0
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed) -> 0
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd) -> 0
}

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

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= True
  _r_1(s(x_0_0), z) <= _r_3(x_0_0)
  _r_1(z, s(x_1_0)) <= _r_3(x_1_0)
  _r_1(z, z) <= True
  _r_2(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0, x_1_0)
  _r_2(z, s(x_1_0)) <= True
  _r_2(z, z) <= True
  _r_3(s(x_0_0)) <= True
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) /\ _r_3(x_1_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_1_0, x_2_0) /\ _r_3(x_0_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_0_0, x_1_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0, x_2_0)
  minus(z, s(x_1_0), z) <= True
  minus(z, z, z) <= True
}
]


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



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




Answer of teacher:

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

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

plus(n, z, n) <= True  :
No: ()

eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od)  :
Yes: {
_od -> s(s(_yzfk_0))  ;  _pd -> s(s(z))  ;  m -> z  ;  n -> s(s(z))
}

minus(s(u), s(x2), _ed) <= minus(u, x2, _ed)  :
Yes: {
_ed -> s(z)  ;  u -> s(z)  ;  x2 -> s(s(_ebgk_0))
}

plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd)  :
No: ()


Total time: 60.829166
Learner time: 59.784390
Teacher time: 0.010126
Reasons for stopping: Maybe:  timeout during teacher: {
minus(s(u), z, s(u)) <= True -> out of time
minus(z, y, z) <= True -> out of time
plus(n, z, n) <= True -> out of time
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od) -> out of time
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed) -> out of time
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd) -> out of time
}Last solver state:

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
plus(n, z, n) <= True -> 0
eq_nat(_pd, m) <= minus(_od, n, _pd) /\ plus(m, n, _od) -> 0
minus(s(u), s(x2), _ed) <= minus(u, x2, _ed) -> 0
plus(n, s(mm), s(_jd)) <= plus(n, mm, _jd) -> 0
}

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

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_2(x_1_0)
  _r_1(s(x_0_0), s(x_1_0)) <= _r_3(x_0_0)
  _r_1(s(x_0_0), z) <= _r_2(x_0_0)
  _r_1(z, s(x_1_0)) <= _r_2(x_1_0)
  _r_1(z, z) <= True
  _r_2(s(x_0_0)) <= True
  _r_3(z) <= True
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_0_0) /\ _r_3(x_2_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0) /\ _r_3(x_1_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_1_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_3(x_0_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  minus(z, s(x_1_0), z) <= True
  minus(z, z, z) <= True
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_2(x_1_0)
  _r_1(s(x_0_0), s(x_1_0)) <= _r_3(x_0_0)
  _r_1(s(x_0_0), z) <= _r_2(x_0_0)
  _r_1(z, s(x_1_0)) <= _r_2(x_1_0)
  _r_1(z, z) <= True
  _r_2(s(x_0_0)) <= True
  _r_3(z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_2_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_2_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



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