Solving ../../benchmarks/smtlib/true/plus_commutative.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:
{
(plus, F:
{
plus(n, z, n) <= True
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia)
}
eq_nat(_xia, _yia) <= plus(_via, _wia, _xia) /\ plus(_via, _wia, _yia)
)
}

properties:
{
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia)
}


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

Clause system for inference is:

{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}


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

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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






-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.008692 s (model generation: 0.008616,  model checking: 0.000076):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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



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




Answer of teacher:

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

eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia)  :
No: ()

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


-------------------------------------------
Step 1, which took 0.012320 s (model generation: 0.012222,  model checking: 0.000098):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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



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




Answer of teacher:

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

eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia)  :
No: ()

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


-------------------------------------------
Step 2, which took 0.020806 s (model generation: 0.020647,  model checking: 0.000159):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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:

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

eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia)  :
Yes: {
_aja -> s(s(_oqpaa_0))  ;  _zia -> s(z)  ;  m -> s(_aqpaa_0)  ;  n -> z
}

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


-------------------------------------------
Step 3, which took 0.015669 s (model generation: 0.015577,  model checking: 0.000092):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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_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:

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

eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia)  :
Yes: {
_aja -> s(s(_irpaa_0))  ;  _zia -> s(z)  ;  m -> s(_sqpaa_0)  ;  n -> s(_tqpaa_0)
}

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


-------------------------------------------
Step 4, which took 0.019718 s (model generation: 0.019590,  model checking: 0.000128):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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



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




Answer of teacher:

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

eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia)  :
Yes: {
_aja -> s(s(_kspaa_0))  ;  _zia -> s(z)  ;  m -> z  ;  n -> s(z)
}

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


-------------------------------------------
Step 5, which took 0.022184 s (model generation: 0.022000,  model checking: 0.000184):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

plus ->
[
plus : <nat * nat * nat>
{
  _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:

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

eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia)  :
Yes: {
_aja -> s(s(s(_vtpaa_0)))  ;  _zia -> s(s(z))  ;  m -> s(z)  ;  n -> s(z)
}

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


-------------------------------------------
Step 6, which took 0.027372 s (model generation: 0.026987,  model checking: 0.000385):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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



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




Answer of teacher:

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

eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia)  :
Yes: {
_aja -> s(s(_cxpaa_0))  ;  _zia -> s(z)  ;  m -> s(s(z))  ;  n -> s(s(z))
}

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


-------------------------------------------
Step 7, which took 0.033948 s (model generation: 0.032860,  model checking: 0.001088):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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_0_0) /\ _r_2(x_1_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0) /\ _r_2(x_0_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_2_0) /\ plus(x_0_0, x_1_0, 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_1_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_2(x_2_0)
  plus(z, z, s(x_2_0)) <= _r_2(x_2_0)
  plus(z, z, z) <= True
}
]



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




Answer of teacher:

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

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

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


-------------------------------------------
Step 8, which took 0.032436 s (model generation: 0.031759,  model checking: 0.000677):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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

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

eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia)  :
Yes: {
_aja -> s(s(_dmqaa_0))  ;  _zia -> s(z)  ;  m -> s(z)  ;  n -> s(s(z))
}

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


-------------------------------------------
Step 9, which took 0.037442 s (model generation: 0.036464,  model checking: 0.000978):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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



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




Answer of teacher:

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

eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia)  :
Yes: {
_aja -> s(s(_pvqaa_0))  ;  _zia -> s(z)  ;  m -> s(s(z))  ;  n -> s(z)
}

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


-------------------------------------------
Step 10, which took 0.051246 s (model generation: 0.047586,  model checking: 0.003660):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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



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




Answer of teacher:

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

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

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


-------------------------------------------
Step 11, which took 0.054065 s (model generation: 0.050026,  model checking: 0.004039):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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



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




Answer of teacher:

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

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

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


-------------------------------------------
Step 12, which took 0.122624 s (model generation: 0.122349,  model checking: 0.000275):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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

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

eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia)  :
Yes: {
_aja -> s(s(s(_gftaa_0)))  ;  _zia -> s(s(z))  ;  m -> s(_sdtaa_0)  ;  n -> s(s(_vetaa_0))
}

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


-------------------------------------------
Step 13, which took 0.104750 s (model generation: 0.104391,  model checking: 0.000359):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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(z, s(x_1_0)) <= _r_3(x_1_0)
  _r_3(z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0, x_1_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(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(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:

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

eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia)  :
Yes: {
_aja -> s(s(s(_chtaa_0)))  ;  _zia -> s(s(z))  ;  m -> z  ;  n -> s(s(_bitaa_0))
}

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


-------------------------------------------
Step 14, which took 0.153545 s (model generation: 0.152986,  model checking: 0.000559):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

plus ->
[
plus : <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(z, s(x_1_0)) <= _r_3(x_1_0)
  _r_3(z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0, x_1_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(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(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:

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

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

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


-------------------------------------------
Step 15, which took 0.205902 s (model generation: 0.203673,  model checking: 0.002229):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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



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




Answer of teacher:

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

eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia)  :
Yes: {
_aja -> s(s(_rauaa_0))  ;  _zia -> s(z)  ;  m -> s(s(s(z)))  ;  n -> s(s(s(z)))
}

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


-------------------------------------------
Step 16, which took 0.307901 s (model generation: 0.306695,  model checking: 0.001206):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

plus ->
[
plus : <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)) <= _r_3(x_1_0)
  _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(z) <= True
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_1(x_1_0, 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_1_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:

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

eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia)  :
No: ()

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


-------------------------------------------
Step 17, which took 0.486344 s (model generation: 0.476272,  model checking: 0.010072):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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)) <= _r_3(x_0_0)
  _r_3(s(x_0_0)) <= _r_2(x_0_0)
  _r_3(z) <= True
  plus(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)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_2(x_1_0) /\ _r_3(x_2_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0) /\ _r_3(x_1_0) /\ _r_3(x_2_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_2_0) /\ _r_3(x_0_0) /\ _r_3(x_1_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) /\ _r_2(x_2_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_3(x_0_0) /\ _r_3(x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_2(x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_3(x_1_0)
  plus(z, z, z) <= True
}
]



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




Answer of teacher:

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

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

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


-------------------------------------------
Step 18, which took 0.394737 s (model generation: 0.380506,  model checking: 0.014231):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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)) <= _r_3(x_0_0)
  _r_3(s(x_0_0)) <= _r_2(x_0_0)
  _r_3(z) <= True
  plus(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)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_2(x_1_0) /\ _r_3(x_2_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0) /\ _r_3(x_1_0) /\ _r_3(x_2_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_2_0) /\ _r_3(x_0_0) /\ _r_3(x_1_0)
  plus(s(x_0_0), z, 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) /\ _r_3(x_0_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_3(x_1_0) /\ _r_3(x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_2(x_1_0) /\ _r_2(x_2_0)
  plus(z, z, z) <= True
}
]



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




Answer of teacher:

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

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

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


-------------------------------------------
Step 19, which took 0.439479 s (model generation: 0.434550,  model checking: 0.004929):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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



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




Answer of teacher:

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

eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia)  :
Yes: {
_aja -> s(s(_odyaa_0))  ;  _zia -> s(z)  ;  m -> z  ;  n -> s(s(s(z)))
}

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


-------------------------------------------
Step 20, which took 0.537943 s (model generation: 0.533399,  model checking: 0.004544):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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



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




Answer of teacher:

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

eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia)  :
Yes: {
_aja -> s(s(s(s(z))))  ;  _zia -> s(s(s(z)))  ;  m -> s(s(z))  ;  n -> s(_tfyaa_0)
}

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


-------------------------------------------
Step 21, which took 0.470713 s (model generation: 0.457950,  model checking: 0.012763):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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)) <= _r_3(x_0_0)
  _r_3(s(x_0_0)) <= _r_1(x_0_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) /\ _r_1(x_1_0) /\ _r_3(x_2_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0) /\ _r_2(x_0_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_2_0) /\ _r_3(x_0_0) /\ _r_3(x_1_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_2_0) /\ _r_3(x_0_0)
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_2_0) /\ _r_3(x_1_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0) /\ _r_1(x_2_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_3(x_0_0) /\ _r_3(x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0) /\ _r_1(x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_2(x_1_0) /\ _r_2(x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_3(x_1_0) /\ _r_3(x_2_0)
  plus(z, z, z) <= True
}
]



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




Answer of teacher:

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

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

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


-------------------------------------------
Step 22, which took 0.544687 s (model generation: 0.534471,  model checking: 0.010216):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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



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




Answer of teacher:

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

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

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


-------------------------------------------
Step 23, which took 0.658928 s (model generation: 0.640501,  model checking: 0.018427):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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



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




Answer of teacher:

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

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

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


-------------------------------------------
Step 24, which took 0.806989 s (model generation: 0.759810,  model checking: 0.047179):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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



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




Answer of teacher:

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

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

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


-------------------------------------------
Step 25, which took 23.430915 s (model generation: 23.430554,  model checking: 0.000361):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

plus ->
[
plus : <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)) <= _r_4(x_1_0)
  _r_2(s(x_0_0), s(x_1_0)) <= True
  _r_3(s(x_0_0), s(x_1_0)) <= _r_3(x_0_0, x_1_0)
  _r_3(z, z) <= True
  _r_4(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), s(x_1_0), s(x_2_0)) <= _r_2(x_1_0, x_2_0)
  plus(s(x_0_0), z, s(x_2_0)) <= _r_3(x_0_0, x_2_0)
  plus(z, s(x_1_0), s(x_2_0)) <= _r_3(x_1_0, x_2_0)
  plus(z, z, z) <= True
}
]



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




Answer of teacher:

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

eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia)  :
Yes: {
_aja -> s(s(s(_zfpba_0)))  ;  _zia -> s(s(z))  ;  m -> s(s(_ofpba_0))  ;  n -> s(s(_mfpba_0))
}

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


-------------------------------------------
Step 26, which took 30.080578 s (model generation: 30.078021,  model checking: 0.002557):

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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

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

eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia)  :
Yes: {
_aja -> s(z)  ;  _zia -> s(s(z))  ;  m -> s(s(s(z)))  ;  n -> s(s(s(s(_jspba_0))))
}

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


Total time: 60.133046
Learner time: 58.940462
Teacher time: 0.141471
Reasons for stopping: Maybe:  timeout during learnerLast solver state:

Clauses:
{
plus(n, z, n) <= True -> 0
eq_nat(_zia, _aja) <= plus(m, n, _aja) /\ plus(n, m, _zia) -> 0
plus(n, s(mm), s(_uia)) <= plus(n, mm, _uia) -> 0
}

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

Current best model:
|_
name: None

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