Solving ../../benchmarks/smtlib/true/tree_member_leq_size.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: {
elt -> {a, b}  ;  etree -> {leaf, node}  ;  nat -> {s, z}
}
definition:
{
(leq, P:
{
leq(z, n2) <= True
leq(s(nn1), s(nn2)) <= leq(nn1, nn2)
leq(nn1, nn2) <= leq(s(nn1), s(nn2))
False <= leq(s(nn1), z)
}
)
(plus, F:
{
plus(n, z, n) <= True
plus(n, s(mm), s(_lma)) <= plus(n, mm, _lma)
}
eq_nat(_oma, _pma) <= plus(_mma, _nma, _oma) /\ plus(_mma, _nma, _pma)
)
(numnodes, F:
{
numnodes(leaf, z) <= True
numnodes(node(e, t1, t2), s(_sma)) <= numnodes(t1, _qma) /\ numnodes(t2, _rma) /\ plus(_qma, _rma, _sma)
}
eq_nat(_uma, _vma) <= numnodes(_tma, _uma) /\ numnodes(_tma, _vma)
)
(member, P:
{
member(e2, node(e2, t1, t2)) <= True
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)
False <= member(e, leaf)
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))
}
)
}

properties:
{
leq(s(z), _wma) <= member(e, t1) /\ numnodes(t1, _wma)
}


over-approximation: {member, numnodes, plus}
under-approximation: {leq}

Clause system for inference is:

{
member(e2, node(e2, t1, t2)) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
leq(s(z), _wma) <= member(e, t1) /\ numnodes(t1, _wma) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
numnodes(node(e, t1, t2), s(_sma)) <= numnodes(t1, _qma) /\ numnodes(t2, _rma) /\ plus(_qma, _rma, _sma) -> 0
plus(n, s(mm), s(_lma)) <= plus(n, mm, _lma) -> 0
}


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

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


;
member ->
[
member : <elt * etree>
{
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_1)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_2)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_4(x_0_0)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_2)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_0)
  _r_3(b) <= True
  _r_4(a) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_1)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_2)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_4(x_1_0)
  member(b, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_1)
  member(b, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_2)
  member(b, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  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: {elt, etree, nat}
_|
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005700 s (model generation: 0.005611,  model checking: 0.000089):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
leq(s(z), _wma) <= member(e, t1) /\ numnodes(t1, _wma) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
numnodes(node(e, t1, t2), s(_sma)) <= numnodes(t1, _qma) /\ numnodes(t2, _rma) /\ plus(_qma, _rma, _sma) -> 0
plus(n, s(mm), s(_lma)) <= plus(n, mm, _lma) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

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


;
member ->
[
member : <elt * etree>
{
  
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  
}
]


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



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




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
Yes: {
e2 -> b
}

numnodes(leaf, z) <= True  :
Yes: {

}

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

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

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

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

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
No: ()

leq(s(z), _wma) <= member(e, t1) /\ numnodes(t1, _wma)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
No: ()

numnodes(node(e, t1, t2), s(_sma)) <= numnodes(t1, _qma) /\ numnodes(t2, _rma) /\ plus(_qma, _rma, _sma)  :
No: ()

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


-------------------------------------------
Step 1, which took 0.007936 s (model generation: 0.007333,  model checking: 0.000603):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
leq(s(z), _wma) <= member(e, t1) /\ numnodes(t1, _wma) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
numnodes(node(e, t1, t2), s(_sma)) <= numnodes(t1, _qma) /\ numnodes(t2, _rma) /\ plus(_qma, _rma, _sma) -> 0
plus(n, s(mm), s(_lma)) <= plus(n, mm, _lma) -> 0
}

Accumulated learning constraints:
{
member(b, node(b, leaf, leaf)) <= True
numnodes(leaf, z) <= True
plus(z, z, z) <= True
}

Current best model:
|_
name: None

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


;
member ->
[
member : <elt * etree>
{
  member(b, node(x_1_0, x_1_1, x_1_2)) <= True
}
]


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


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



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




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
Yes: {
e2 -> a
}

numnodes(leaf, z) <= True  :
No: ()

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

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

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

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

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
No: ()

leq(s(z), _wma) <= member(e, t1) /\ numnodes(t1, _wma)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
Yes: {
e -> b  ;  e2 -> a  ;  t1 -> leaf  ;  t2 -> leaf
}

numnodes(node(e, t1, t2), s(_sma)) <= numnodes(t1, _qma) /\ numnodes(t2, _rma) /\ plus(_qma, _rma, _sma)  :
Yes: {
_qma -> z  ;  _rma -> z  ;  _sma -> z  ;  t1 -> leaf  ;  t2 -> leaf
}

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


-------------------------------------------
Step 2, which took 0.009361 s (model generation: 0.009192,  model checking: 0.000169):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
leq(s(z), _wma) <= member(e, t1) /\ numnodes(t1, _wma) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
numnodes(node(e, t1, t2), s(_sma)) <= numnodes(t1, _qma) /\ numnodes(t2, _rma) /\ plus(_qma, _rma, _sma) -> 0
plus(n, s(mm), s(_lma)) <= plus(n, mm, _lma) -> 0
}

Accumulated learning constraints:
{
member(a, node(a, leaf, leaf)) <= True
member(b, node(b, leaf, leaf)) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), s(z)) <= True
plus(s(z), z, s(z)) <= True
plus(z, s(z), s(z)) <= True
plus(z, z, z) <= True
member(b, leaf) <= member(b, node(a, leaf, leaf))
}

Current best model:
|_
name: None

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


;
member ->
[
member : <elt * etree>
{
  member(a, node(x_1_0, x_1_1, x_1_2)) <= True
  member(b, leaf) <= True
  member(b, node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
}
]


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



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




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

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

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

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

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

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
No: ()

leq(s(z), _wma) <= member(e, t1) /\ numnodes(t1, _wma)  :
Yes: {
_wma -> z  ;  e -> b  ;  t1 -> leaf
}

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> leaf  ;  t2 -> leaf
}

numnodes(node(e, t1, t2), s(_sma)) <= numnodes(t1, _qma) /\ numnodes(t2, _rma) /\ plus(_qma, _rma, _sma)  :
No: ()

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


-------------------------------------------
Step 3, which took 0.010363 s (model generation: 0.010220,  model checking: 0.000143):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
leq(s(z), _wma) <= member(e, t1) /\ numnodes(t1, _wma) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
numnodes(node(e, t1, t2), s(_sma)) <= numnodes(t1, _qma) /\ numnodes(t2, _rma) /\ plus(_qma, _rma, _sma) -> 0
plus(n, s(mm), s(_lma)) <= plus(n, mm, _lma) -> 0
}

Accumulated learning constraints:
{
member(a, node(a, leaf, leaf)) <= True
member(b, node(b, leaf, leaf)) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), 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
member(a, leaf) <= member(a, node(b, leaf, leaf))
leq(s(z), z) <= member(b, leaf)
member(b, leaf) <= member(b, node(a, leaf, leaf))
}

Current best model:
|_
name: None

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


;
member ->
[
member : <elt * etree>
{
  member(a, leaf) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= True
  member(b, leaf) <= True
  member(b, node(x_1_0, x_1_1, x_1_2)) <= True
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  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: {elt, etree, nat}
_|




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

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

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

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

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

}

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
No: ()

leq(s(z), _wma) <= member(e, t1) /\ numnodes(t1, _wma)  :
Yes: {
_wma -> s(_tdwgw_0)  ;  e -> b  ;  t1 -> node(_vdwgw_0, _vdwgw_1, _vdwgw_2)
}

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
No: ()

numnodes(node(e, t1, t2), s(_sma)) <= numnodes(t1, _qma) /\ numnodes(t2, _rma) /\ plus(_qma, _rma, _sma)  :
No: ()

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


-------------------------------------------
Step 4, which took 0.017933 s (model generation: 0.017707,  model checking: 0.000226):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
leq(s(z), _wma) <= member(e, t1) /\ numnodes(t1, _wma) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
numnodes(node(e, t1, t2), s(_sma)) <= numnodes(t1, _qma) /\ numnodes(t2, _rma) /\ plus(_qma, _rma, _sma) -> 0
plus(n, s(mm), s(_lma)) <= plus(n, mm, _lma) -> 0
}

Accumulated learning constraints:
{
member(a, node(a, leaf, leaf)) <= True
member(b, node(b, leaf, leaf)) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), 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 <= leq(s(z), z)
member(a, leaf) <= member(a, node(b, leaf, leaf))
False <= member(b, leaf)
False <= member(b, node(a, leaf, leaf))
}

Current best model:
|_
name: None

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


;
member ->
[
member : <elt * etree>
{
  _r_1(b) <= True
  member(a, leaf) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= True
  member(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_0)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  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: {elt, etree, nat}
_|




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

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

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

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

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

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
Yes: {
e -> b  ;  e2 -> a  ;  t1 -> node(b, _zdwgw_1, _zdwgw_2)
}

leq(s(z), _wma) <= member(e, t1) /\ numnodes(t1, _wma)  :
Yes: {
_wma -> z  ;  e -> a  ;  t1 -> leaf
}

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
Yes: {
e -> b  ;  e2 -> a  ;  t1 -> node(a, _pewgw_1, _pewgw_2)  ;  t2 -> node(b, _qewgw_1, _qewgw_2)
}

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
No: ()

numnodes(node(e, t1, t2), s(_sma)) <= numnodes(t1, _qma) /\ numnodes(t2, _rma) /\ plus(_qma, _rma, _sma)  :
No: ()

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


-------------------------------------------
Step 5, which took 0.042206 s (model generation: 0.041687,  model checking: 0.000519):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
leq(s(z), _wma) <= member(e, t1) /\ numnodes(t1, _wma) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
numnodes(node(e, t1, t2), s(_sma)) <= numnodes(t1, _qma) /\ numnodes(t2, _rma) /\ plus(_qma, _rma, _sma) -> 0
plus(n, s(mm), s(_lma)) <= plus(n, mm, _lma) -> 0
}

Accumulated learning constraints:
{
member(a, node(a, leaf, leaf)) <= True
member(b, node(a, node(a, leaf, leaf), node(b, leaf, leaf))) <= True
member(b, node(a, node(b, leaf, leaf), leaf)) <= True
member(b, node(b, leaf, leaf)) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), 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 <= leq(s(z), z)
False <= member(a, leaf)
False <= member(a, node(b, leaf, leaf))
False <= member(b, leaf)
False <= member(b, node(a, leaf, leaf))
}

Current best model:
|_
name: None

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


;
member ->
[
member : <elt * etree>
{
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= True
  _r_2(b) <= True
  _r_3(a) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
  member(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_1)
  member(b, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_0)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  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: {elt, etree, nat}
_|




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

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

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

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

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

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> node(a, _nfwgw_1, _nfwgw_2)
}

leq(s(z), _wma) <= member(e, t1) /\ numnodes(t1, _wma)  :
Yes: {
_wma -> s(_xfwgw_0)  ;  e -> b  ;  t1 -> node(_zfwgw_0, node(_yiwgw_0, _yiwgw_1, _yiwgw_2), _zfwgw_2)
}

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
Yes: {
e -> b  ;  e2 -> a  ;  t1 -> leaf  ;  t2 -> node(_ogwgw_0, node(_yiwgw_0, _yiwgw_1, _yiwgw_2), _ogwgw_2)
}

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
Yes: {
e -> b  ;  e2 -> a  ;  t1 -> node(a, leaf, _riwgw_2)  ;  t2 -> node(a, leaf, _siwgw_2)
}

numnodes(node(e, t1, t2), s(_sma)) <= numnodes(t1, _qma) /\ numnodes(t2, _rma) /\ plus(_qma, _rma, _sma)  :
No: ()

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


-------------------------------------------
Step 6, which took 0.077474 s (model generation: 0.076634,  model checking: 0.000840):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
leq(s(z), _wma) <= member(e, t1) /\ numnodes(t1, _wma) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
numnodes(node(e, t1, t2), s(_sma)) <= numnodes(t1, _qma) /\ numnodes(t2, _rma) /\ plus(_qma, _rma, _sma) -> 0
plus(n, s(mm), s(_lma)) <= plus(n, mm, _lma) -> 0
}

Accumulated learning constraints:
{
member(a, node(a, leaf, leaf)) <= True
member(a, node(b, node(a, leaf, leaf), leaf)) <= True
member(b, node(a, node(a, leaf, leaf), node(b, leaf, leaf))) <= True
member(b, node(a, node(b, leaf, leaf), leaf)) <= True
member(b, node(b, leaf, leaf)) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), 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 <= leq(s(z), z)
False <= member(a, leaf)
False <= member(a, node(b, leaf, leaf))
False <= member(b, leaf)
False <= member(b, node(a, leaf, leaf))
member(b, node(a, leaf, node(a, node(a, leaf, leaf), leaf))) <= member(b, node(a, node(a, leaf, leaf), leaf))
leq(s(z), s(z)) <= member(b, node(a, node(a, leaf, leaf), leaf)) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
False <= member(b, node(a, node(a, leaf, leaf), node(a, leaf, leaf)))
}

Current best model:
|_
name: None

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


;
member ->
[
member : <elt * etree>
{
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_0)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= True
  _r_3(b) <= True
  _r_4(a) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_1)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_4(x_1_0)
  member(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_1)
  member(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_2)
  member(b, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  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: {elt, etree, nat}
_|




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

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

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

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

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

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
Yes: {
e -> b  ;  e2 -> a  ;  t1 -> node(a, _xjwgw_1, node(b, _wowgw_1, _wowgw_2))  ;  t2 -> leaf
}

leq(s(z), _wma) <= member(e, t1) /\ numnodes(t1, _wma)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> leaf  ;  t2 -> node(_ekwgw_0, node(_uowgw_0, _uowgw_1, _uowgw_2), _ekwgw_2)
}

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> node(b, leaf, _pmwgw_2)  ;  t2 -> node(b, leaf, _qmwgw_2)
}

numnodes(node(e, t1, t2), s(_sma)) <= numnodes(t1, _qma) /\ numnodes(t2, _rma) /\ plus(_qma, _rma, _sma)  :
No: ()

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


-------------------------------------------
Step 7, which took 0.102317 s (model generation: 0.100555,  model checking: 0.001762):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
leq(s(z), _wma) <= member(e, t1) /\ numnodes(t1, _wma) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
numnodes(node(e, t1, t2), s(_sma)) <= numnodes(t1, _qma) /\ numnodes(t2, _rma) /\ plus(_qma, _rma, _sma) -> 0
plus(n, s(mm), s(_lma)) <= plus(n, mm, _lma) -> 0
}

Accumulated learning constraints:
{
member(a, node(a, leaf, leaf)) <= True
member(a, node(b, node(a, leaf, leaf), leaf)) <= True
member(b, node(a, node(a, leaf, leaf), node(b, leaf, leaf))) <= True
member(b, node(a, node(b, leaf, leaf), leaf)) <= True
member(b, node(b, leaf, leaf)) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), 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
leq(z, z) <= leq(s(z), s(z))
False <= leq(s(z), z)
False <= member(a, leaf)
member(a, node(b, leaf, node(a, node(a, leaf, leaf), leaf))) <= member(a, node(a, node(a, leaf, leaf), leaf))
False <= member(a, node(b, leaf, leaf))
False <= member(a, node(b, node(b, leaf, leaf), node(b, leaf, leaf)))
False <= member(b, leaf)
False <= member(b, node(a, leaf, leaf))
member(b, node(a, node(a, leaf, node(b, leaf, leaf)), leaf)) <= member(b, node(a, leaf, node(b, leaf, leaf)))
member(b, node(a, leaf, node(a, node(a, leaf, leaf), leaf))) <= member(b, node(a, node(a, leaf, leaf), leaf))
leq(s(z), s(z)) <= member(b, node(a, node(a, leaf, leaf), leaf)) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
False <= member(b, node(a, node(a, leaf, leaf), node(a, leaf, leaf)))
}

Current best model:
|_
name: None

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


;
member ->
[
member : <elt * etree>
{
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_0)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_4(x_0_0)
  _r_3(a) <= True
  _r_4(b) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_1)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_2)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
  member(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_1) /\ _r_2(x_1_2)
  member(b, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_1)
  member(b, node(x_1_0, x_1_1, x_1_2)) <= _r_4(x_1_0)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  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: {elt, etree, nat}
_|




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

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

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

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

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

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
Yes: {
e -> b  ;  e2 -> a  ;  t1 -> node(a, node(b, _saxgw_1, _saxgw_2), _hqwgw_2)  ;  t2 -> leaf
}

leq(s(z), _wma) <= member(e, t1) /\ numnodes(t1, _wma)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
Yes: {
e -> b  ;  e2 -> a  ;  t1 -> leaf  ;  t2 -> node(b, _urwgw_1, _urwgw_2)
}

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
No: ()

numnodes(node(e, t1, t2), s(_sma)) <= numnodes(t1, _qma) /\ numnodes(t2, _rma) /\ plus(_qma, _rma, _sma)  :
No: ()

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


-------------------------------------------
Step 8, which took 0.127220 s (model generation: 0.125984,  model checking: 0.001236):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
leq(s(z), _wma) <= member(e, t1) /\ numnodes(t1, _wma) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
numnodes(node(e, t1, t2), s(_sma)) <= numnodes(t1, _qma) /\ numnodes(t2, _rma) /\ plus(_qma, _rma, _sma) -> 0
plus(n, s(mm), s(_lma)) <= plus(n, mm, _lma) -> 0
}

Accumulated learning constraints:
{
member(a, node(a, leaf, leaf)) <= True
member(a, node(b, node(a, leaf, leaf), leaf)) <= True
member(b, node(a, leaf, node(b, leaf, leaf))) <= True
member(b, node(a, node(a, leaf, leaf), node(b, leaf, leaf))) <= True
member(b, node(a, node(a, leaf, node(b, leaf, leaf)), leaf)) <= True
member(b, node(a, node(a, node(b, leaf, leaf), leaf), leaf)) <= True
member(b, node(a, node(b, leaf, leaf), leaf)) <= True
member(b, node(b, leaf, leaf)) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), 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
leq(z, s(z)) <= leq(s(z), s(s(z)))
leq(z, z) <= leq(s(z), s(z))
False <= leq(s(z), z)
False <= member(a, leaf)
member(a, node(b, leaf, node(a, node(a, leaf, leaf), leaf))) <= member(a, node(a, node(a, leaf, leaf), leaf))
False <= member(a, node(b, leaf, leaf))
False <= member(a, node(b, node(b, leaf, leaf), node(b, leaf, leaf)))
False <= member(b, leaf)
False <= member(b, node(a, leaf, leaf))
member(b, node(a, leaf, node(a, node(a, leaf, leaf), leaf))) <= member(b, node(a, node(a, leaf, leaf), leaf))
leq(s(z), s(z)) <= member(b, node(a, node(a, leaf, leaf), leaf)) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
False <= member(b, node(a, node(a, leaf, leaf), node(a, leaf, leaf)))
}

Current best model:
|_
name: None

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


;
member ->
[
member : <elt * etree>
{
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_1)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_2)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_4(x_0_0)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_0)
  _r_3(a) <= True
  _r_4(b) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_1)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_2)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
  member(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_1)
  member(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_2)
  member(b, node(x_1_0, x_1_1, x_1_2)) <= _r_4(x_1_0)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  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: {elt, etree, nat}
_|




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

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

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

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

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

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> node(b, _ucxgw_1, node(a, _kjxgw_1, _kjxgw_2))  ;  t2 -> leaf
}

leq(s(z), _wma) <= member(e, t1) /\ numnodes(t1, _wma)  :
No: ()

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> leaf  ;  t2 -> node(b, _odxgw_1, node(a, _kjxgw_1, _kjxgw_2))
}

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
No: ()

numnodes(node(e, t1, t2), s(_sma)) <= numnodes(t1, _qma) /\ numnodes(t2, _rma) /\ plus(_qma, _rma, _sma)  :
No: ()

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


-------------------------------------------
Step 9, which took 0.158390 s (model generation: 0.157100,  model checking: 0.001290):

Clauses:
{
member(e2, node(e2, t1, t2)) <= True -> 0
numnodes(leaf, z) <= True -> 0
plus(n, z, n) <= True -> 0
leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0
leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0
False <= leq(s(nn1), z) -> 0
eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1) -> 0
leq(s(z), _wma) <= member(e, t1) /\ numnodes(t1, _wma) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2) -> 0
eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2)) -> 0
numnodes(node(e, t1, t2), s(_sma)) <= numnodes(t1, _qma) /\ numnodes(t2, _rma) /\ plus(_qma, _rma, _sma) -> 0
plus(n, s(mm), s(_lma)) <= plus(n, mm, _lma) -> 0
}

Accumulated learning constraints:
{
member(a, node(a, leaf, leaf)) <= True
member(a, node(b, node(a, leaf, leaf), leaf)) <= True
member(b, node(a, leaf, node(b, leaf, leaf))) <= True
member(b, node(a, node(a, leaf, leaf), node(b, leaf, leaf))) <= True
member(b, node(a, node(a, leaf, node(b, leaf, leaf)), leaf)) <= True
member(b, node(a, node(a, node(b, leaf, leaf), leaf), leaf)) <= True
member(b, node(a, node(b, leaf, leaf), leaf)) <= True
member(b, node(b, leaf, leaf)) <= True
numnodes(leaf, z) <= True
numnodes(node(a, leaf, leaf), 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 <= leq(s(s(z)), s(z))
leq(z, s(z)) <= leq(s(z), s(s(z)))
leq(z, z) <= leq(s(z), s(z))
False <= leq(s(z), z)
False <= member(a, leaf)
member(a, node(b, leaf, node(a, node(a, leaf, leaf), leaf))) <= member(a, node(a, node(a, leaf, leaf), leaf))
False <= member(a, node(b, leaf, leaf))
member(a, node(b, leaf, node(b, leaf, node(a, leaf, leaf)))) <= member(a, node(b, leaf, node(a, leaf, leaf)))
member(a, node(b, node(b, leaf, node(a, leaf, leaf)), leaf)) <= member(a, node(b, leaf, node(a, leaf, leaf)))
False <= member(a, node(b, node(b, leaf, leaf), node(b, leaf, leaf)))
False <= member(b, leaf)
False <= member(b, node(a, leaf, leaf))
member(b, node(a, leaf, node(a, node(a, leaf, leaf), leaf))) <= member(b, node(a, node(a, leaf, leaf), leaf))
leq(s(z), s(z)) <= member(b, node(a, node(a, leaf, leaf), leaf)) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z))
False <= member(b, node(a, node(a, leaf, leaf), node(a, leaf, leaf)))
}

Current best model:
|_
name: None

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


;
member ->
[
member : <elt * etree>
{
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_1)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_2)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_4(x_0_0)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_2)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_0)
  _r_3(a) <= True
  _r_4(b) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_1)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_2)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
  member(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_1)
  member(b, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_2)
  member(b, node(x_1_0, x_1_1, x_1_2)) <= _r_4(x_1_0)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  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: {elt, etree, nat}
_|




Answer of teacher:

member(e2, node(e2, t1, t2)) <= True  :
No: ()

numnodes(leaf, z) <= True  :
No: ()

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

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

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

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

eq_elt(e, e2) \/ member(e, node(e2, t1, t2)) <= member(e, t1)  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> node(b, node(a, _htxgw_1, _htxgw_2), leaf)  ;  t2 -> leaf
}

leq(s(z), _wma) <= member(e, t1) /\ numnodes(t1, _wma)  :
Yes: {
_wma -> s(_mmxgw_0)  ;  e -> a  ;  t1 -> node(a, _omxgw_1, _omxgw_2)
}

eq_elt(e, e2) \/ member(e, t1) \/ member(e, node(e2, t1, t2)) <= member(e, t2)  :
Yes: {
e -> a  ;  e2 -> b  ;  t1 -> leaf  ;  t2 -> node(b, node(a, _htxgw_1, _htxgw_2), leaf)
}

eq_elt(e, e2) \/ member(e, t1) \/ member(e, t2) <= member(e, node(e2, t1, t2))  :
No: ()

numnodes(node(e, t1, t2), s(_sma)) <= numnodes(t1, _qma) /\ numnodes(t2, _rma) /\ plus(_qma, _rma, _sma)  :
No: ()

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


Total time: 0.756619
Learner time: 0.552023
Teacher time: 0.006877
Reasons for stopping: Yes: |_
name: None

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


;
member ->
[
member : <elt * etree>
{
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_1)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_1(x_0_2)
  _r_1(node(x_0_0, x_0_1, x_0_2)) <= _r_4(x_0_0)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_1)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_2(x_0_2)
  _r_2(node(x_0_0, x_0_1, x_0_2)) <= _r_3(x_0_0)
  _r_3(b) <= True
  _r_4(a) <= True
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_1)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_2)
  member(a, node(x_1_0, x_1_1, x_1_2)) <= _r_4(x_1_0)
  member(b, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_1)
  member(b, node(x_1_0, x_1_1, x_1_2)) <= _r_2(x_1_2)
  member(b, node(x_1_0, x_1_1, x_1_2)) <= _r_3(x_1_0)
}
]


;
numnodes ->
[
numnodes : <etree * nat>
{
  numnodes(leaf, z) <= True
  numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True
}
]


;
plus ->
[
plus : <nat * nat * nat>
{
  plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True
  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: {elt, etree, nat}
_|