Solving ../../benchmarks/smtlib/true/isaplanner_prop79.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), _cpa) <= minus(u, x2, _cpa)
}
eq_nat(_fpa, _gpa) <= minus(_dpa, _epa, _fpa) /\ minus(_dpa, _epa, _gpa)
)
}

properties:
{
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)
}


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

Clause system for inference is:

{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 0
}


Solving took 60.989203 seconds.
Maybe:  timeout during learnerLast solver state:

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 0
}

Accumulated learning constraints:
{
minus(s(s(s(s(s(z))))), z, s(s(s(s(s(z)))))) <= True
minus(s(s(s(s(z)))), s(s(z)), s(s(z))) <= True
minus(s(s(s(s(z)))), z, s(s(s(s(z))))) <= True
minus(s(s(s(z))), s(s(s(z))), z) <= True
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(s(z)))), 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(s(z))), 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(s(z)), z) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= minus(s(s(s(s(z)))), s(s(s(z))), z) /\ minus(s(s(s(z))), s(s(s(z))), s(z))
False <= minus(s(s(s(s(z)))), s(s(z)), s(z)) /\ minus(s(s(s(z))), z, s(z))
False <= minus(s(s(s(s(z)))), s(s(z)), z)
False <= minus(s(s(s(s(z)))), s(z), s(z)) /\ minus(s(s(s(z))), s(z), s(z))
False <= minus(s(s(s(z))), s(s(z)), s(s(z)))
False <= minus(s(s(s(z))), s(s(z)), z) /\ minus(s(s(z)), s(s(z)), s(s(z)))
False <= minus(s(s(s(z))), s(z), z)
minus(s(s(s(s(z)))), s(z), s(s(s(s(z))))) <= minus(s(s(s(z))), z, s(s(s(s(z)))))
False <= minus(s(s(s(z))), z, z)
False <= minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(z)), s(s(s(z))), s(z))
minus(s(s(s(z))), s(s(s(z))), s(s(s(z)))) <= minus(s(s(z)), s(s(z)), s(s(s(z))))
False <= minus(s(s(z)), s(s(z)), s(z))
minus(s(s(s(z))), s(s(z)), s(s(s(z)))) <= minus(s(s(z)), s(z), s(s(s(z))))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z))))
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(s(z))), s(s(z)))
False <= minus(s(z), s(s(z)), s(s(z)))
False <= 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))
False <= minus(s(z), z, s(s(s(z))))
False <= minus(s(z), z, s(s(z)))
False <= minus(s(z), z, z)
}

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, s(x_1_0)) <= True
  _r_1(z, z) <= True
  _r_2(s(x_0_0), s(x_1_0)) <= True
  _r_2(z, z) <= True
  _r_3(s(x_0_0)) <= _r_4(x_0_0)
  _r_3(z) <= True
  _r_4(s(x_0_0)) <= _r_3(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, x_1_0) /\ _r_4(x_0_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_0_0) /\ _r_3(x_2_0) /\ _r_4(x_1_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0, x_2_0) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ _r_4(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_2_0) /\ _r_4(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), z, s(x_2_0)) <= _r_2(x_0_0, x_2_0) /\ _r_3(x_0_0) /\ _r_3(x_2_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_4(x_0_0) /\ _r_4(x_2_0)
  minus(z, s(x_1_0), z) <= True
  minus(z, z, z) <= True
}
]



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






-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.014371 s (model generation: 0.014285,  model checking: 0.000086):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

minus ->
[
minus : <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
}

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
No: ()

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


-------------------------------------------
Step 1, which took 0.016769 s (model generation: 0.016648,  model checking: 0.000121):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 0
}

Accumulated learning constraints:
{
minus(s(z), z, s(z)) <= True
minus(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
}
]



--
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(_mosk_0)
}

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
No: ()

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


-------------------------------------------
Step 2, which took 0.018356 s (model generation: 0.018164,  model checking: 0.000192):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 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
}

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



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




Answer of teacher:

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

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

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> s(_tosk_0)  ;  _ipa -> z  ;  _jpa -> s(_vosk_0)  ;  _kpa -> s(_wosk_0)  ;  k -> z  ;  m -> s(_yosk_0)  ;  n -> z
}

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


-------------------------------------------
Step 3, which took 0.023648 s (model generation: 0.023195,  model checking: 0.000453):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 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
False <= minus(s(s(z)), z, s(z))
}

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(z) <= True
  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)) <= _r_1(x_0_0)
  minus(z, s(x_1_0), z) <= True
  minus(z, z, z) <= True
}
]



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




Answer of teacher:

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

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

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> z  ;  _ipa -> z  ;  _jpa -> s(_ntsk_0)  ;  _kpa -> s(_otsk_0)  ;  k -> s(_ptsk_0)  ;  m -> s(_qtsk_0)  ;  n -> s(_rtsk_0)
}

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


-------------------------------------------
Step 4, which took 0.014715 s (model generation: 0.014407,  model checking: 0.000308):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 0
}

Accumulated learning constraints:
{
minus(s(s(z)), s(z), s(z)) <= True
minus(s(s(z)), z, s(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
False <= minus(s(s(z)), s(z), z) /\ minus(s(z), s(z), s(z)) /\ minus(z, s(s(z)), z)
False <= minus(s(s(z)), z, 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
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0, 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
}
]



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




Answer of teacher:

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

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

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> s(_xvsk_0)  ;  _ipa -> s(_yvsk_0)  ;  _jpa -> z  ;  _kpa -> z  ;  k -> s(_bwsk_0)  ;  m -> z  ;  n -> s(_dwsk_0)
}

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


-------------------------------------------
Step 5, which took 0.012450 s (model generation: 0.011997,  model checking: 0.000453):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 0
}

Accumulated learning constraints:
{
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
False <= minus(s(s(z)), s(z), z) /\ minus(s(z), s(z), s(z)) /\ minus(z, s(s(z)), z)
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(z)), s(z)) /\ minus(s(z), s(z), 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, s(x_1_0)) <= True
  _r_1(z, z) <= True
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_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), 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
}
]



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




Answer of teacher:

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

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

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> s(z)  ;  _ipa -> s(s(_wetk_0))  ;  _jpa -> z  ;  _kpa -> z  ;  k -> s(_gbtk_0)  ;  m -> z  ;  n -> s(z)
}

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


-------------------------------------------
Step 6, which took 0.025837 s (model generation: 0.025245,  model checking: 0.000592):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 0
}

Accumulated learning constraints:
{
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
False <= minus(s(s(z)), s(z), z) /\ minus(s(z), s(z), s(z)) /\ minus(z, s(s(z)), z)
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(z)), s(s(z))) /\ minus(s(z), s(z), s(z))
False <= minus(s(z), s(s(z)), s(z)) /\ minus(s(z), s(z), s(z))
minus(s(s(z)), s(s(z)), s(z)) <= minus(s(z), s(z), 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), z) <= True
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(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)) <= _r_1(x_0_0, x_2_0)
  minus(z, s(x_1_0), z) <= True
  minus(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: ()

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> z  ;  _ipa -> z  ;  _jpa -> s(z)  ;  _kpa -> s(z)  ;  k -> z  ;  m -> s(s(_dktk_0))  ;  n -> s(_ujtk_0)
}

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


-------------------------------------------
Step 7, which took 0.036069 s (model generation: 0.034985,  model checking: 0.001084):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 0
}

Accumulated learning constraints:
{
minus(s(s(s(z))), s(z), s(s(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
False <= minus(s(s(s(z))), s(z), z)
False <= minus(s(s(z)), s(z), z) /\ minus(s(z), s(z), s(z)) /\ minus(z, s(s(z)), z)
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(z)), s(s(z))) /\ minus(s(z), s(z), s(z))
False <= minus(s(z), s(s(z)), s(z)) /\ minus(s(z), s(z), s(z))
minus(s(s(z)), s(s(z)), s(z)) <= minus(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)) <= _r_1(x_2_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
}
]



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




Answer of teacher:

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

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

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> s(s(_ixtk_0))  ;  _ipa -> s(_hrtk_0)  ;  _jpa -> z  ;  _kpa -> z  ;  k -> z  ;  m -> z  ;  n -> z
}

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


-------------------------------------------
Step 8, which took 0.038225 s (model generation: 0.037402,  model checking: 0.000823):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 0
}

Accumulated learning constraints:
{
minus(s(s(s(z))), s(z), s(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
False <= minus(s(s(s(z))), s(z), z)
False <= minus(s(s(z)), s(z), z) /\ minus(s(z), s(z), s(z)) /\ minus(z, s(s(z)), z)
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(z)), s(s(z))) /\ minus(s(z), s(z), s(z))
False <= minus(s(z), s(s(z)), s(z)) /\ minus(s(z), s(z), s(z))
minus(s(s(z)), s(s(z)), s(z)) <= minus(s(z), s(z), s(z))
False <= minus(s(z), 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)) <= 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, 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
}
]



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




Answer of teacher:

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

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

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> z  ;  _ipa -> z  ;  _jpa -> s(z)  ;  _kpa -> s(z)  ;  k -> z  ;  m -> s(s(_wfuk_0))  ;  n -> s(s(_wfuk_0))
}

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


-------------------------------------------
Step 9, which took 0.038853 s (model generation: 0.036741,  model checking: 0.002112):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 0
}

Accumulated learning constraints:
{
minus(s(s(s(z))), s(z), s(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
False <= minus(s(s(s(z))), s(s(z)), z) /\ minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(s(z))), s(z), z)
False <= minus(s(s(z)), s(z), z) /\ minus(s(z), s(z), s(z)) /\ minus(z, s(s(z)), z)
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(z)), s(s(z))) /\ minus(s(z), s(z), s(z))
False <= minus(s(z), s(s(z)), s(z)) /\ minus(s(z), s(z), s(z))
minus(s(s(z)), s(s(z)), s(z)) <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(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) /\ _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)) <= _r_1(x_0_0) /\ _r_1(x_2_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) /\ _r_2(x_2_0)
  minus(z, s(x_1_0), z) <= True
  minus(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: ()

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> s(s(_eavk_0))  ;  _ipa -> s(_houk_0)  ;  _jpa -> z  ;  _kpa -> z  ;  k -> z  ;  m -> s(z)  ;  n -> s(z)
}

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


-------------------------------------------
Step 10, which took 0.060401 s (model generation: 0.042654,  model checking: 0.017747):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 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(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
False <= minus(s(s(s(z))), s(s(z)), z) /\ minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(s(z))), s(z), z)
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z) /\ minus(s(z), s(z), s(z)) /\ minus(z, s(s(z)), z)
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(z)), s(s(z))) /\ minus(s(z), s(z), s(z))
False <= minus(s(z), s(s(z)), s(z)) /\ minus(s(z), s(z), s(z))
minus(s(s(z)), s(s(z)), s(z)) <= minus(s(z), s(z), s(z))
False <= minus(s(z), 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_0_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_1_0) /\ _r_2(x_0_0)
  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(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) /\ _r_2(x_2_0)
  minus(z, s(x_1_0), z) <= True
  minus(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: ()

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> s(s(_hkal_0))  ;  _ipa -> s(s(_wkal_0))  ;  _jpa -> s(s(_hkal_0))  ;  _kpa -> z  ;  k -> s(s(_vkal_0))  ;  m -> s(s(_olal_0))  ;  n -> z
}

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


-------------------------------------------
Step 11, which took 0.062369 s (model generation: 0.045213,  model checking: 0.017156):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 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(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
False <= minus(s(s(s(z))), s(s(z)), z) /\ minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(s(z))), s(z), z)
False <= minus(s(s(s(z))), z, s(s(z))) /\ minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z) /\ minus(s(z), s(z), s(z)) /\ minus(z, s(s(z)), z)
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(z)), s(s(z))) /\ minus(s(z), s(z), s(z))
False <= minus(s(z), s(s(z)), s(z)) /\ minus(s(z), s(z), s(z))
minus(s(s(z)), s(s(z)), s(z)) <= minus(s(z), s(z), s(z))
False <= minus(s(z), 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_0_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_1_0) /\ _r_2(x_1_0)
  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(x_0_0, x_1_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_1_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) /\ _r_2(x_2_0)
  minus(s(x_0_0), z, z) <= True
  minus(z, s(x_1_0), z) <= True
  minus(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: ()

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> z  ;  _ipa -> z  ;  _jpa -> s(s(_vogl_0))  ;  _kpa -> s(s(_vogl_0))  ;  k -> z  ;  m -> s(s(_vogl_0))  ;  n -> z
}

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


-------------------------------------------
Step 12, which took 0.123178 s (model generation: 0.121768,  model checking: 0.001410):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 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(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
False <= minus(s(s(s(z))), s(s(z)), z) /\ minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(s(z))), s(z), z)
False <= minus(s(s(s(z))), z, s(s(z))) /\ minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(s(z))), z, z)
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z) /\ minus(s(z), s(z), s(z)) /\ minus(z, s(s(z)), z)
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(z)), s(s(z))) /\ minus(s(z), s(z), s(z))
False <= minus(s(z), s(s(z)), s(z)) /\ minus(s(z), s(z), s(z))
minus(s(s(z)), s(s(z)), s(z)) <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
minus(s(s(z)), s(z), z) <= minus(s(z), z, z)
}

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _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(s(x_0_0), z) <= True
  _r_3(s(x_0_0), 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), z) <= _r_1(x_0_0, x_1_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
}
]



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




Answer of teacher:

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

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

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> z  ;  _ipa -> z  ;  _jpa -> s(z)  ;  _kpa -> s(z)  ;  k -> z  ;  m -> s(s(s(_vxgl_0)))  ;  n -> s(s(z))
}

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


-------------------------------------------
Step 13, which took 0.179736 s (model generation: 0.178335,  model checking: 0.001401):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 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(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
False <= minus(s(s(s(s(z)))), s(s(z)), z)
False <= minus(s(s(s(z))), s(s(z)), z) /\ minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(s(z))), s(z), z)
False <= minus(s(s(s(z))), z, s(s(z))) /\ minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(s(z))), z, z)
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z) /\ minus(s(z), s(z), s(z)) /\ minus(z, s(s(z)), z)
minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z))))
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(z)), s(s(z))) /\ minus(s(z), s(z), s(z))
False <= minus(s(z), s(s(z)), s(z)) /\ minus(s(z), s(z), s(z))
minus(s(s(z)), s(s(z)), s(z)) <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
minus(s(s(z)), s(z), z) <= minus(s(z), z, z)
}

Current best model:
|_
name: None

minus ->
[
minus : <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
  _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_3(z, s(x_1_0)) <= True
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(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_3(x_0_0, 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
}
]



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




Answer of teacher:

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

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

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> z  ;  _ipa -> z  ;  _jpa -> s(z)  ;  _kpa -> s(z)  ;  k -> z  ;  m -> s(s(z))  ;  n -> s(s(s(z)))
}

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


-------------------------------------------
Step 14, which took 0.392051 s (model generation: 0.385422,  model checking: 0.006629):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 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(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
False <= minus(s(s(s(s(z)))), s(s(z)), z)
False <= minus(s(s(s(z))), s(s(s(z))), z) /\ minus(s(s(z)), s(s(s(z))), s(z))
False <= minus(s(s(s(z))), s(s(z)), z) /\ minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(s(z))), s(z), z)
False <= minus(s(s(s(z))), z, s(s(z))) /\ minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(s(z))), z, z)
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z) /\ minus(s(z), s(z), s(z)) /\ minus(z, s(s(z)), z)
minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z))))
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(z)), s(s(z))) /\ minus(s(z), s(z), s(z))
False <= minus(s(z), s(s(z)), s(z)) /\ minus(s(z), s(z), s(z))
minus(s(s(z)), s(s(z)), s(z)) <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
minus(s(s(z)), s(z), z) <= minus(s(z), z, z)
}

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(s(x_0_0)) <= _r_2(x_0_0)
  _r_2(s(x_0_0)) <= _r_3(x_0_0)
  _r_3(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), s(x_2_0)) <= _r_2(x_0_0) /\ _r_3(x_2_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_0_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_2(x_0_0) /\ _r_2(x_2_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_3(x_0_0) /\ _r_3(x_2_0)
  minus(z, s(x_1_0), z) <= True
  minus(z, z, z) <= True
}
]



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




Answer of teacher:

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

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

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> s(s(z))  ;  _ipa -> z  ;  _jpa -> s(z)  ;  _kpa -> s(z)  ;  k -> z  ;  m -> s(z)  ;  n -> z
}

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


-------------------------------------------
Step 15, which took 0.411085 s (model generation: 0.403665,  model checking: 0.007420):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 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
False <= minus(s(s(s(s(z)))), s(s(z)), z)
False <= minus(s(s(s(z))), s(s(s(z))), z) /\ minus(s(s(z)), s(s(s(z))), s(z))
False <= minus(s(s(s(z))), s(s(z)), z) /\ minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(s(z))), s(z), z)
False <= minus(s(s(s(z))), z, s(s(z))) /\ minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(s(z))), z, z)
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z))))
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(z)), s(s(z))) /\ minus(s(z), s(z), s(z))
False <= minus(s(z), s(s(z)), s(z)) /\ minus(s(z), s(z), s(z))
minus(s(s(z)), s(s(z)), s(z)) <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
False <= minus(s(z), z, z)
}

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0)
  _r_1(s(x_0_0), z) <= _r_3(x_0_0)
  _r_2(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) /\ _r_2(x_1_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(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)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) /\ _r_2(x_2_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_3(x_0_0) /\ _r_3(x_2_0)
  minus(z, s(x_1_0), z) <= True
  minus(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: ()

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> s(s(_pwll_0))  ;  _ipa -> s(z)  ;  _jpa -> s(z)  ;  _kpa -> z  ;  k -> s(_xokl_0)  ;  m -> s(z)  ;  n -> z
}

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


-------------------------------------------
Step 16, which took 0.401348 s (model generation: 0.390616,  model checking: 0.010732):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 0
}

Accumulated learning constraints:
{
minus(s(s(s(s(z)))), s(s(z)), s(s(z))) <= True
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
False <= minus(s(s(s(s(z)))), s(s(z)), z)
False <= minus(s(s(s(z))), s(s(s(z))), z) /\ minus(s(s(z)), s(s(s(z))), s(z))
False <= minus(s(s(s(z))), s(z), z)
False <= minus(s(s(s(z))), z, s(s(z))) /\ minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(s(z))), z, z)
False <= minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z))))
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
False <= minus(s(z), z, 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) /\ _r_3(x_2_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
}
]



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




Answer of teacher:

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

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

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> s(s(_appl_0))  ;  _ipa -> s(z)  ;  _jpa -> z  ;  _kpa -> z  ;  k -> z  ;  m -> z  ;  n -> s(s(_topl_0))
}

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


-------------------------------------------
Step 17, which took 0.440498 s (model generation: 0.438596,  model checking: 0.001902):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 0
}

Accumulated learning constraints:
{
minus(s(s(s(s(z)))), s(s(z)), s(s(z))) <= True
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
False <= minus(s(s(s(s(z)))), s(s(z)), z)
False <= minus(s(s(s(z))), s(s(s(z))), z) /\ minus(s(s(z)), s(s(s(z))), s(z))
False <= minus(s(s(s(z))), s(z), z)
False <= minus(s(s(s(z))), z, s(s(z))) /\ minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(s(z))), z, z)
False <= minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z))))
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(z)), s(s(z))) /\ minus(z, s(s(z)), z)
False <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
False <= minus(s(z), z, z)
}

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(s(x_0_0), z) <= 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), s(x_1_0)) <= _r_3(x_0_0, x_1_0)
  _r_3(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_1_0) /\ _r_1(x_0_0, x_2_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_0_0, x_1_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_2(x_0_0, x_2_0)
  minus(z, s(x_1_0), z) <= True
  minus(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: ()

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> s(s(z))  ;  _ipa -> s(z)  ;  _jpa -> z  ;  _kpa -> z  ;  k -> z  ;  m -> s(s(z))  ;  n -> s(s(z))
}

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


-------------------------------------------
Step 18, which took 0.249811 s (model generation: 0.221602,  model checking: 0.028209):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 0
}

Accumulated learning constraints:
{
minus(s(s(s(s(z)))), s(s(z)), s(s(z))) <= True
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
False <= minus(s(s(s(s(z)))), s(s(z)), z)
False <= minus(s(s(s(z))), s(s(s(z))), z) /\ minus(s(s(z)), s(s(s(z))), s(z))
False <= minus(s(s(s(z))), s(s(z)), s(s(z)))
False <= minus(s(s(s(z))), s(z), z)
False <= minus(s(s(s(z))), z, s(s(z))) /\ minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(s(z))), z, z)
False <= minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z))))
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(z)), s(s(z))) /\ minus(z, s(s(z)), z)
False <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
False <= minus(s(z), z, z)
}

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _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_2(z) <= True
  _r_3(s(x_0_0)) <= _r_2(x_0_0)
  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) /\ _r_2(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_0_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_0_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_3(x_0_0) /\ _r_3(x_1_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) /\ _r_2(x_2_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_3(x_0_0) /\ _r_3(x_2_0)
  minus(z, s(x_1_0), z) <= True
  minus(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: ()

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> s(s(z))  ;  _ipa -> s(z)  ;  _jpa -> z  ;  _kpa -> z  ;  k -> z  ;  m -> s(z)  ;  n -> s(s(s(z)))
}

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


-------------------------------------------
Step 19, which took 0.253760 s (model generation: 0.224881,  model checking: 0.028879):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 0
}

Accumulated learning constraints:
{
minus(s(s(s(s(z)))), s(s(z)), s(s(z))) <= True
minus(s(s(s(z))), s(s(s(z))), z) <= True
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
False <= minus(s(s(s(s(z)))), s(s(z)), z)
False <= minus(s(s(s(z))), s(s(z)), s(s(z)))
False <= minus(s(s(s(z))), s(z), z)
False <= minus(s(s(s(z))), z, s(s(z))) /\ minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(s(z))), z, z)
False <= minus(s(s(z)), s(s(s(z))), s(s(z))) /\ minus(s(z), s(s(s(z))), z)
False <= minus(s(s(z)), s(s(s(z))), s(z))
False <= minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z))))
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(z)), s(s(z))) /\ minus(z, s(s(z)), z)
False <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
False <= minus(s(z), z, z)
}

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, s(x_1_0)) <= True
  _r_1(z, z) <= True
  _r_2(s(x_0_0)) <= _r_3(x_0_0)
  _r_2(z) <= True
  _r_3(s(x_0_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_2_0) /\ _r_3(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_3(x_0_0) /\ _r_3(x_1_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0) /\ _r_2(x_1_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_2(x_2_0) /\ _r_3(x_1_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0, x_1_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) /\ _r_2(x_2_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_3(x_0_0) /\ _r_3(x_2_0)
  minus(z, s(x_1_0), z) <= True
  minus(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: ()

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> s(z)  ;  _ipa -> s(s(z))  ;  _jpa -> z  ;  _kpa -> z  ;  k -> s(s(z))  ;  m -> z  ;  n -> z
}

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


-------------------------------------------
Step 20, which took 0.210563 s (model generation: 0.193024,  model checking: 0.017539):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 0
}

Accumulated learning constraints:
{
minus(s(s(s(s(z)))), s(s(z)), s(s(z))) <= True
minus(s(s(s(z))), s(s(s(z))), z) <= True
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
False <= minus(s(s(s(s(z)))), s(s(z)), z)
False <= minus(s(s(s(z))), s(s(z)), s(s(z)))
False <= minus(s(s(s(z))), s(z), z)
False <= minus(s(s(s(z))), z, s(s(z))) /\ minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(s(z))), z, z)
False <= minus(s(s(z)), s(s(s(z))), s(s(z))) /\ minus(s(z), s(s(s(z))), z)
False <= minus(s(s(z)), s(s(s(z))), s(z))
False <= minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z))))
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(s(z))), s(s(z))) /\ minus(z, s(s(z)), z)
False <= minus(s(z), s(s(z)), s(s(z))) /\ minus(z, s(s(z)), z)
False <= minus(s(z), s(s(z)), s(z))
False <= minus(s(z), s(z), s(z))
False <= minus(s(z), z, s(s(z)))
False <= minus(s(z), z, z)
}

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(s(x_0_0), s(x_1_0)) <= _r_3(x_0_0)
  _r_1(s(x_0_0), s(x_1_0)) <= _r_3(x_1_0)
  _r_1(z, z) <= True
  _r_2(s(x_0_0)) <= _r_3(x_0_0)
  _r_2(z) <= True
  _r_3(s(x_0_0)) <= _r_2(x_0_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_0_0) /\ _r_2(x_2_0) /\ _r_3(x_1_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_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_0_0) /\ _r_2(x_1_0) /\ _r_3(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) /\ _r_3(x_1_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) /\ _r_2(x_2_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_3(x_0_0) /\ _r_3(x_2_0)
  minus(z, s(x_1_0), z) <= _r_2(x_1_0)
  minus(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(s(z))
}

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> s(z)  ;  _ipa -> s(s(z))  ;  _jpa -> z  ;  _kpa -> z  ;  k -> z  ;  m -> z  ;  n -> z
}

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


-------------------------------------------
Step 21, which took 0.283254 s (model generation: 0.244580,  model checking: 0.038674):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 0
}

Accumulated learning constraints:
{
minus(s(s(s(s(z)))), s(s(z)), s(s(z))) <= True
minus(s(s(s(z))), s(s(s(z))), z) <= True
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(s(z)), z) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= minus(s(s(s(s(z)))), s(s(z)), z)
False <= minus(s(s(s(z))), s(s(z)), s(s(z)))
False <= minus(s(s(s(z))), s(z), z)
False <= minus(s(s(s(z))), z, s(s(z))) /\ minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(s(z))), z, z)
False <= minus(s(s(z)), s(s(s(z))), s(s(z))) /\ minus(s(z), s(s(s(z))), z)
False <= minus(s(s(z)), s(s(s(z))), s(z))
False <= minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z))))
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(s(z))), s(s(z)))
False <= minus(s(z), s(s(z)), s(s(z)))
False <= 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(s(z)))) <= minus(s(z), z, s(s(s(z))))
False <= minus(s(z), z, s(s(z)))
False <= minus(s(z), z, z)
}

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(s(x_0_0), s(x_1_0)) <= _r_3(x_0_0)
  _r_1(s(x_0_0), s(x_1_0)) <= _r_3(x_1_0)
  _r_1(z, z) <= True
  _r_2(s(x_0_0)) <= _r_3(x_0_0)
  _r_2(z) <= True
  _r_3(s(x_0_0)) <= _r_2(x_0_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_0_0) /\ _r_2(x_2_0) /\ _r_3(x_1_0)
  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_2(x_1_0) /\ _r_3(x_2_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(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) /\ _r_3(x_1_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_0_0) /\ _r_2(x_2_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_3(x_0_0) /\ _r_3(x_2_0)
  minus(z, s(x_1_0), z) <= True
  minus(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: ()

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> z  ;  _ipa -> z  ;  _jpa -> s(s(z))  ;  _kpa -> s(s(z))  ;  k -> z  ;  m -> s(s(z))  ;  n -> s(s(z))
}

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


-------------------------------------------
Step 22, which took 7.860262 s (model generation: 7.842361,  model checking: 0.017901):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 0
}

Accumulated learning constraints:
{
minus(s(s(s(s(z)))), s(s(z)), s(s(z))) <= True
minus(s(s(s(z))), s(s(s(z))), z) <= True
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(s(z))), 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(s(z)), z) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= minus(s(s(s(s(z)))), s(s(z)), z)
False <= minus(s(s(s(z))), s(s(z)), s(s(z)))
False <= minus(s(s(s(z))), s(s(z)), z) /\ minus(s(s(z)), s(s(z)), s(s(z)))
False <= minus(s(s(s(z))), s(z), z)
False <= minus(s(s(s(z))), z, z)
False <= minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(z)), s(s(s(z))), s(z))
False <= minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z))))
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(s(z))), s(s(z)))
False <= minus(s(z), s(s(z)), s(s(z)))
False <= 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(s(z)))) <= minus(s(z), z, s(s(s(z))))
False <= minus(s(z), z, s(s(z)))
False <= minus(s(z), z, z)
}

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, s(x_1_0)) <= True
  _r_1(z, z) <= True
  _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) <= _r_4(x_0_0)
  _r_4(s(x_0_0)) <= True
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_1_0, x_2_0) /\ _r_4(x_0_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_3(x_0_0, x_1_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_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), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) /\ _r_4(x_0_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
}
]



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




Answer of teacher:

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

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

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> s(z)  ;  _ipa -> z  ;  _jpa -> s(z)  ;  _kpa -> s(z)  ;  k -> z  ;  m -> s(s(s(_yzzm_0)))  ;  n -> s(z)
}

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


-------------------------------------------
Step 23, which took 5.669954 s (model generation: 5.665059,  model checking: 0.004895):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 0
}

Accumulated learning constraints:
{
minus(s(s(s(s(z)))), s(s(z)), s(s(z))) <= True
minus(s(s(s(z))), s(s(s(z))), z) <= True
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(s(z))), 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(s(z)), z) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= minus(s(s(s(s(z)))), s(s(z)), z)
False <= minus(s(s(s(s(z)))), s(z), s(z)) /\ minus(s(s(s(z))), s(z), s(z))
False <= minus(s(s(s(z))), s(s(z)), s(s(z)))
False <= minus(s(s(s(z))), s(s(z)), z) /\ minus(s(s(z)), s(s(z)), s(s(z)))
False <= minus(s(s(s(z))), s(z), z)
False <= minus(s(s(s(z))), z, z)
False <= minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(z)), s(s(s(z))), s(z))
False <= minus(s(s(z)), s(s(z)), s(z))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z))))
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(s(z))), s(s(z)))
False <= minus(s(z), s(s(z)), s(s(z)))
False <= 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(s(z)))) <= minus(s(z), z, s(s(s(z))))
False <= minus(s(z), z, s(s(z)))
False <= minus(s(z), z, z)
}

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_3(x_0_0)
  _r_1(s(x_0_0), s(x_1_0), z) <= True
  _r_1(s(x_0_0), z, s(x_2_0)) <= True
  _r_1(s(x_0_0), z, z) <= _r_3(x_0_0)
  _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)) <= _r_4(x_0_0)
  _r_3(z) <= True
  _r_4(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, x_2_0) /\ _r_2(x_1_0, x_2_0) /\ _r_3(x_2_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, 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_3(x_0_0) /\ _r_3(x_2_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_4(x_0_0) /\ _r_4(x_2_0)
  minus(z, s(x_1_0), z) <= True
  minus(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: ()

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> s(s(s(_itbn_0)))  ;  _ipa -> s(z)  ;  _jpa -> z  ;  _kpa -> z  ;  k -> s(_jdbn_0)  ;  m -> z  ;  n -> z
}

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


-------------------------------------------
Step 24, which took 4.206210 s (model generation: 4.158664,  model checking: 0.047546):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 0
}

Accumulated learning constraints:
{
minus(s(s(s(s(z)))), s(s(z)), s(s(z))) <= True
minus(s(s(s(z))), s(s(s(z))), z) <= True
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(s(z))), 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(s(z)), z) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= minus(s(s(s(s(z)))), s(s(z)), z)
False <= minus(s(s(s(s(z)))), s(z), s(z)) /\ minus(s(s(s(z))), s(z), s(z))
False <= minus(s(s(s(z))), s(s(z)), s(s(z)))
False <= minus(s(s(s(z))), s(s(z)), z) /\ minus(s(s(z)), s(s(z)), s(s(z)))
False <= minus(s(s(s(z))), s(z), z)
False <= minus(s(s(s(z))), z, z)
False <= minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(z)), s(s(s(z))), s(z))
False <= minus(s(s(z)), s(s(z)), s(z))
minus(s(s(s(z))), s(s(z)), s(s(s(z)))) <= minus(s(s(z)), s(z), s(s(s(z))))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z))))
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(s(z))), s(s(z)))
False <= minus(s(z), s(s(z)), s(s(z)))
False <= 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))
False <= minus(s(z), z, s(s(s(z))))
False <= minus(s(z), z, s(s(z)))
False <= minus(s(z), z, z)
}

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(z) <= True
  _r_2(s(x_0_0)) <= _r_4(x_0_0)
  _r_3(s(x_0_0)) <= _r_1(x_0_0)
  _r_4(s(x_0_0)) <= _r_3(x_0_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0) /\ _r_1(x_2_0) /\ _r_3(x_0_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0) /\ _r_4(x_0_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_2_0) /\ _r_4(x_0_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)
  minus(s(x_0_0), s(x_1_0), z) <= _r_3(x_0_0) /\ _r_3(x_1_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_4(x_1_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0) /\ _r_1(x_2_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_3(x_0_0) /\ _r_3(x_2_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_4(x_0_0)
  minus(z, s(x_1_0), z) <= True
  minus(z, z, z) <= True
}
]



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




Answer of teacher:

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

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

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> z  ;  _ipa -> z  ;  _jpa -> s(z)  ;  _kpa -> s(z)  ;  k -> z  ;  m -> s(s(s(z)))  ;  n -> s(s(s(z)))
}

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


-------------------------------------------
Step 25, which took 7.720987 s (model generation: 7.641990,  model checking: 0.078997):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 0
}

Accumulated learning constraints:
{
minus(s(s(s(s(z)))), s(s(z)), s(s(z))) <= True
minus(s(s(s(s(z)))), z, s(s(s(s(z))))) <= True
minus(s(s(s(z))), s(s(s(z))), z) <= True
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(s(z)))), 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(s(z))), 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(s(z)), z) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= minus(s(s(s(s(z)))), s(s(s(z))), z) /\ minus(s(s(s(z))), s(s(s(z))), s(z))
False <= minus(s(s(s(s(z)))), s(s(z)), z)
False <= minus(s(s(s(s(z)))), s(z), s(z)) /\ minus(s(s(s(z))), s(z), s(z))
False <= minus(s(s(s(z))), s(s(z)), s(s(z)))
False <= minus(s(s(s(z))), s(s(z)), z) /\ minus(s(s(z)), s(s(z)), s(s(z)))
False <= minus(s(s(s(z))), s(z), z)
False <= minus(s(s(s(z))), z, z)
False <= minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(z)), s(s(s(z))), s(z))
False <= minus(s(s(z)), s(s(z)), s(z))
minus(s(s(s(z))), s(s(z)), s(s(s(z)))) <= minus(s(s(z)), s(z), s(s(s(z))))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z))))
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(s(z))), s(s(z)))
False <= minus(s(z), s(s(z)), s(s(z)))
False <= 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))
False <= minus(s(z), z, s(s(s(z))))
False <= minus(s(z), z, s(s(z)))
False <= minus(s(z), z, z)
}

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(z) <= True
  _r_2(s(x_0_0)) <= _r_1(x_0_0)
  _r_3(s(x_0_0)) <= _r_4(x_0_0)
  _r_4(s(x_0_0)) <= _r_2(x_0_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0) /\ _r_1(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) /\ _r_4(x_0_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_2_0) /\ _r_2(x_1_0) /\ _r_4(x_0_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_1_0) /\ _r_3(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_0_0) /\ _r_2(x_1_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_3(x_1_0)
  minus(s(x_0_0), s(x_1_0), z) <= _r_4(x_1_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0) /\ _r_1(x_2_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) /\ _r_2(x_2_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_3(x_2_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_4(x_0_0)
  minus(z, s(x_1_0), z) <= True
  minus(z, z, z) <= True
}
]



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




Answer of teacher:

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

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

eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa)  :
Yes: {
_hpa -> s(s(s(s(z))))  ;  _ipa -> s(_prjo_0)  ;  _jpa -> s(z)  ;  _kpa -> z  ;  k -> s(z)  ;  m -> s(s(s(z)))  ;  n -> z
}

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


-------------------------------------------
Step 26, which took 31.135201 s (model generation: 31.049651,  model checking: 0.085550):

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 0
}

Accumulated learning constraints:
{
minus(s(s(s(s(s(z))))), z, s(s(s(s(s(z)))))) <= True
minus(s(s(s(s(z)))), s(s(z)), s(s(z))) <= True
minus(s(s(s(s(z)))), z, s(s(s(s(z))))) <= True
minus(s(s(s(z))), s(s(s(z))), z) <= True
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(s(z)))), 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(s(z))), 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(s(z)), z) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= minus(s(s(s(s(z)))), s(s(s(z))), z) /\ minus(s(s(s(z))), s(s(s(z))), s(z))
False <= minus(s(s(s(s(z)))), s(s(z)), s(z)) /\ minus(s(s(s(z))), z, s(z))
False <= minus(s(s(s(s(z)))), s(s(z)), z)
False <= minus(s(s(s(s(z)))), s(z), s(z)) /\ minus(s(s(s(z))), s(z), s(z))
False <= minus(s(s(s(z))), s(s(z)), s(s(z)))
False <= minus(s(s(s(z))), s(s(z)), z) /\ minus(s(s(z)), s(s(z)), s(s(z)))
False <= minus(s(s(s(z))), s(z), z)
minus(s(s(s(s(z)))), s(z), s(s(s(s(z))))) <= minus(s(s(s(z))), z, s(s(s(s(z)))))
False <= minus(s(s(s(z))), z, z)
False <= minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(z)), s(s(s(z))), s(z))
False <= minus(s(s(z)), s(s(z)), s(z))
minus(s(s(s(z))), s(s(z)), s(s(s(z)))) <= minus(s(s(z)), s(z), s(s(s(z))))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z))))
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(s(z))), s(s(z)))
False <= minus(s(z), s(s(z)), s(s(z)))
False <= 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))
False <= minus(s(z), z, s(s(s(z))))
False <= minus(s(z), z, s(s(z)))
False <= minus(s(z), z, z)
}

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, s(x_1_0)) <= True
  _r_1(z, z) <= True
  _r_2(s(x_0_0), s(x_1_0)) <= True
  _r_2(z, z) <= True
  _r_3(s(x_0_0)) <= _r_4(x_0_0)
  _r_3(z) <= True
  _r_4(s(x_0_0)) <= _r_3(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, x_1_0) /\ _r_4(x_0_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_0_0) /\ _r_3(x_2_0) /\ _r_4(x_1_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0, x_2_0) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ _r_4(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_2_0) /\ _r_4(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), z, s(x_2_0)) <= _r_2(x_0_0, x_2_0) /\ _r_3(x_0_0) /\ _r_3(x_2_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_4(x_0_0) /\ _r_4(x_2_0)
  minus(z, s(x_1_0), z) <= True
  minus(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: ()

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


Total time: 60.989203
Learner time: 59.481150
Teacher time: 0.418811
Reasons for stopping: Maybe:  timeout during learnerLast solver state:

Clauses:
{
minus(s(u), z, s(u)) <= True -> 0
minus(z, y, z) <= True -> 0
eq_nat(_ipa, _kpa) <= minus(_hpa, s(k), _ipa) /\ minus(_jpa, k, _kpa) /\ minus(m, n, _jpa) /\ minus(s(m), n, _hpa) -> 0
minus(s(u), s(x2), _cpa) <= minus(u, x2, _cpa) -> 0
}

Accumulated learning constraints:
{
minus(s(s(s(s(s(z))))), z, s(s(s(s(s(z)))))) <= True
minus(s(s(s(s(z)))), s(s(z)), s(s(z))) <= True
minus(s(s(s(s(z)))), z, s(s(s(s(z))))) <= True
minus(s(s(s(z))), s(s(s(z))), z) <= True
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(s(z)))), 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(s(z))), 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(s(z)), z) <= True
minus(z, s(z), z) <= True
minus(z, z, z) <= True
False <= minus(s(s(s(s(z)))), s(s(s(z))), z) /\ minus(s(s(s(z))), s(s(s(z))), s(z))
False <= minus(s(s(s(s(z)))), s(s(z)), s(z)) /\ minus(s(s(s(z))), z, s(z))
False <= minus(s(s(s(s(z)))), s(s(z)), z)
False <= minus(s(s(s(s(z)))), s(z), s(z)) /\ minus(s(s(s(z))), s(z), s(z))
False <= minus(s(s(s(z))), s(s(z)), s(s(z)))
False <= minus(s(s(s(z))), s(s(z)), z) /\ minus(s(s(z)), s(s(z)), s(s(z)))
False <= minus(s(s(s(z))), s(z), z)
minus(s(s(s(s(z)))), s(z), s(s(s(s(z))))) <= minus(s(s(s(z))), z, s(s(s(s(z)))))
False <= minus(s(s(s(z))), z, z)
False <= minus(s(s(z)), s(s(s(z))), s(s(z)))
False <= minus(s(s(z)), s(s(s(z))), s(z))
minus(s(s(s(z))), s(s(s(z))), s(s(s(z)))) <= minus(s(s(z)), s(s(z)), s(s(s(z))))
False <= minus(s(s(z)), s(s(z)), s(z))
minus(s(s(s(z))), s(s(z)), s(s(s(z)))) <= minus(s(s(z)), s(z), s(s(s(z))))
False <= minus(s(s(z)), s(z), s(s(z)))
False <= minus(s(s(z)), s(z), z)
minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z))))
False <= minus(s(s(z)), z, s(z))
False <= minus(s(z), s(s(s(z))), s(s(z)))
False <= minus(s(z), s(s(z)), s(s(z)))
False <= 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))
False <= minus(s(z), z, s(s(s(z))))
False <= minus(s(z), z, s(s(z)))
False <= minus(s(z), z, z)
}

Current best model:
|_
name: None

minus ->
[
minus : <nat * nat * nat>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, s(x_1_0)) <= True
  _r_1(z, z) <= True
  _r_2(s(x_0_0), s(x_1_0)) <= True
  _r_2(z, z) <= True
  _r_3(s(x_0_0)) <= _r_4(x_0_0)
  _r_3(z) <= True
  _r_4(s(x_0_0)) <= _r_3(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, x_1_0) /\ _r_4(x_0_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_0_0) /\ _r_3(x_2_0) /\ _r_4(x_1_0)
  minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0, x_2_0) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ _r_4(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_2_0) /\ _r_4(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), z, s(x_2_0)) <= _r_2(x_0_0, x_2_0) /\ _r_3(x_0_0) /\ _r_3(x_2_0)
  minus(s(x_0_0), z, s(x_2_0)) <= _r_4(x_0_0) /\ _r_4(x_2_0)
  minus(z, s(x_1_0), z) <= True
  minus(z, z, z) <= True
}
]



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