Solving ../../benchmarks/smtlib/true/tree_strict_subtree_trans.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}  ;  nattree -> {leaf, node}
}
definition:
{
(strict_subtree, P:
{
strict_subtree(leaf, node(eb, tb1, tb2)) <= True
strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= strict_subtree(ta1, tb1) /\ strict_subtree(ta2, tb2)
strict_subtree(ta2, tb2) <= strict_subtree(ta1, tb1) /\ strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))
False <= strict_subtree(leaf, leaf)
False <= strict_subtree(node(ea, ta1, ta2), leaf)
eq_nat(ea, eb) <= strict_subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))
strict_subtree(ta1, tb1) <= strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))
}
)
}

properties:
{
strict_subtree(t1, t3) <= strict_subtree(t1, t2) /\ strict_subtree(t2, t3)
}


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

Clause system for inference is:

{
strict_subtree(leaf, node(eb, tb1, tb2)) <= True -> 0
strict_subtree(t1, t3) <= strict_subtree(t1, t2) /\ strict_subtree(t2, t3) -> 0
strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= strict_subtree(ta1, tb1) /\ strict_subtree(ta2, tb2) -> 0
strict_subtree(ta2, tb2) <= strict_subtree(ta1, tb1) /\ strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= strict_subtree(leaf, leaf) -> 0
False <= strict_subtree(node(ea, ta1, ta2), leaf) -> 0
eq_nat(ea, eb) <= strict_subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
strict_subtree(ta1, tb1) <= strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}


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

strict_subtree ->
[
strict_subtree : <nattree * nattree>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= True
  strict_subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
  strict_subtree(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_0_0, x_1_0) /\ strict_subtree(x_0_1, x_1_1) /\ strict_subtree(x_0_2, x_1_2)
}
]



--
Equality automata are defined for: {nat, nattree}
_|
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006541 s (model generation: 0.006443,  model checking: 0.000098):

Clauses:
{
strict_subtree(leaf, node(eb, tb1, tb2)) <= True -> 0
strict_subtree(t1, t3) <= strict_subtree(t1, t2) /\ strict_subtree(t2, t3) -> 0
strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= strict_subtree(ta1, tb1) /\ strict_subtree(ta2, tb2) -> 0
strict_subtree(ta2, tb2) <= strict_subtree(ta1, tb1) /\ strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= strict_subtree(leaf, leaf) -> 0
False <= strict_subtree(node(ea, ta1, ta2), leaf) -> 0
eq_nat(ea, eb) <= strict_subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
strict_subtree(ta1, tb1) <= strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{

}

Current best model:
|_
name: None

strict_subtree ->
[
strict_subtree : <nattree * nattree>
{
  
}
]



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




Answer of teacher:

strict_subtree(leaf, node(eb, tb1, tb2)) <= True  :
Yes: {

}

strict_subtree(t1, t3) <= strict_subtree(t1, t2) /\ strict_subtree(t2, t3)  :
No: ()

strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= strict_subtree(ta1, tb1) /\ strict_subtree(ta2, tb2)  :
No: ()

strict_subtree(ta2, tb2) <= strict_subtree(ta1, tb1) /\ strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

False <= strict_subtree(leaf, leaf)  :
No: ()

False <= strict_subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_nat(ea, eb) <= strict_subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

strict_subtree(ta1, tb1) <= strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()


-------------------------------------------
Step 1, which took 0.006589 s (model generation: 0.006514,  model checking: 0.000075):

Clauses:
{
strict_subtree(leaf, node(eb, tb1, tb2)) <= True -> 0
strict_subtree(t1, t3) <= strict_subtree(t1, t2) /\ strict_subtree(t2, t3) -> 0
strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= strict_subtree(ta1, tb1) /\ strict_subtree(ta2, tb2) -> 0
strict_subtree(ta2, tb2) <= strict_subtree(ta1, tb1) /\ strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= strict_subtree(leaf, leaf) -> 0
False <= strict_subtree(node(ea, ta1, ta2), leaf) -> 0
eq_nat(ea, eb) <= strict_subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
strict_subtree(ta1, tb1) <= strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
strict_subtree(leaf, node(z, leaf, leaf)) <= True
}

Current best model:
|_
name: None

strict_subtree ->
[
strict_subtree : <nattree * nattree>
{
  strict_subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
}
]



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




Answer of teacher:

strict_subtree(leaf, node(eb, tb1, tb2)) <= True  :
No: ()

strict_subtree(t1, t3) <= strict_subtree(t1, t2) /\ strict_subtree(t2, t3)  :
No: ()

strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= strict_subtree(ta1, tb1) /\ strict_subtree(ta2, tb2)  :
Yes: {
ta1 -> leaf  ;  ta2 -> leaf  ;  tb1 -> node(_vqmqw_0, _vqmqw_1, _vqmqw_2)  ;  tb2 -> node(_wqmqw_0, _wqmqw_1, _wqmqw_2)
}

strict_subtree(ta2, tb2) <= strict_subtree(ta1, tb1) /\ strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

False <= strict_subtree(leaf, leaf)  :
No: ()

False <= strict_subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_nat(ea, eb) <= strict_subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

strict_subtree(ta1, tb1) <= strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()


-------------------------------------------
Step 2, which took 0.008382 s (model generation: 0.007726,  model checking: 0.000656):

Clauses:
{
strict_subtree(leaf, node(eb, tb1, tb2)) <= True -> 0
strict_subtree(t1, t3) <= strict_subtree(t1, t2) /\ strict_subtree(t2, t3) -> 0
strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= strict_subtree(ta1, tb1) /\ strict_subtree(ta2, tb2) -> 0
strict_subtree(ta2, tb2) <= strict_subtree(ta1, tb1) /\ strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= strict_subtree(leaf, leaf) -> 0
False <= strict_subtree(node(ea, ta1, ta2), leaf) -> 0
eq_nat(ea, eb) <= strict_subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
strict_subtree(ta1, tb1) <= strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
strict_subtree(leaf, node(z, leaf, leaf)) <= True
strict_subtree(node(z, leaf, leaf), node(z, node(z, leaf, leaf), node(z, leaf, leaf))) <= True
}

Current best model:
|_
name: None

strict_subtree ->
[
strict_subtree : <nattree * nattree>
{
  strict_subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
  strict_subtree(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= True
}
]



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




Answer of teacher:

strict_subtree(leaf, node(eb, tb1, tb2)) <= True  :
No: ()

strict_subtree(t1, t3) <= strict_subtree(t1, t2) /\ strict_subtree(t2, t3)  :
No: ()

strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= strict_subtree(ta1, tb1) /\ strict_subtree(ta2, tb2)  :
No: ()

strict_subtree(ta2, tb2) <= strict_subtree(ta1, tb1) /\ strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ta1 -> node(_jrmqw_0, _jrmqw_1, _jrmqw_2)  ;  ta2 -> node(_krmqw_0, _krmqw_1, _krmqw_2)  ;  tb1 -> node(_lrmqw_0, _lrmqw_1, _lrmqw_2)  ;  tb2 -> leaf
}

False <= strict_subtree(leaf, leaf)  :
No: ()

False <= strict_subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_nat(ea, eb) <= strict_subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ea -> z  ;  eb -> s(_srmqw_0)
}

strict_subtree(ta1, tb1) <= strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ta1 -> node(_vrmqw_0, _vrmqw_1, _vrmqw_2)  ;  tb1 -> leaf
}


-------------------------------------------
Step 3, which took 0.011824 s (model generation: 0.011337,  model checking: 0.000487):

Clauses:
{
strict_subtree(leaf, node(eb, tb1, tb2)) <= True -> 0
strict_subtree(t1, t3) <= strict_subtree(t1, t2) /\ strict_subtree(t2, t3) -> 0
strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= strict_subtree(ta1, tb1) /\ strict_subtree(ta2, tb2) -> 0
strict_subtree(ta2, tb2) <= strict_subtree(ta1, tb1) /\ strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= strict_subtree(leaf, leaf) -> 0
False <= strict_subtree(node(ea, ta1, ta2), leaf) -> 0
eq_nat(ea, eb) <= strict_subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
strict_subtree(ta1, tb1) <= strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
strict_subtree(leaf, node(z, leaf, leaf)) <= True
strict_subtree(node(z, leaf, leaf), node(z, node(z, leaf, leaf), node(z, leaf, leaf))) <= True
False <= strict_subtree(node(z, leaf, leaf), node(s(z), leaf, leaf))
strict_subtree(node(z, leaf, leaf), leaf) <= strict_subtree(node(z, leaf, leaf), node(z, leaf, leaf)) /\ strict_subtree(node(z, node(z, leaf, leaf), node(z, leaf, leaf)), node(z, node(z, leaf, leaf), leaf))
strict_subtree(node(z, leaf, leaf), leaf) <= strict_subtree(node(z, node(z, leaf, leaf), leaf), node(z, leaf, leaf))
}

Current best model:
|_
name: None

strict_subtree ->
[
strict_subtree : <nattree * nattree>
{
  strict_subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
  strict_subtree(node(x_0_0, x_0_1, x_0_2), leaf) <= True
  strict_subtree(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= strict_subtree(x_0_1, x_1_2)
}
]



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




Answer of teacher:

strict_subtree(leaf, node(eb, tb1, tb2)) <= True  :
No: ()

strict_subtree(t1, t3) <= strict_subtree(t1, t2) /\ strict_subtree(t2, t3)  :
Yes: {
t1 -> leaf  ;  t2 -> node(_yrmqw_0, _yrmqw_1, _yrmqw_2)  ;  t3 -> leaf
}

strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= strict_subtree(ta1, tb1) /\ strict_subtree(ta2, tb2)  :
Yes: {
ta1 -> leaf  ;  ta2 -> node(_lsmqw_0, _lsmqw_1, _lsmqw_2)  ;  tb1 -> node(_msmqw_0, _msmqw_1, _msmqw_2)  ;  tb2 -> leaf
}

strict_subtree(ta2, tb2) <= strict_subtree(ta1, tb1) /\ strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ta1 -> node(_utmqw_0, _utmqw_1, _utmqw_2)  ;  ta2 -> leaf  ;  tb1 -> leaf  ;  tb2 -> leaf
}

False <= strict_subtree(leaf, leaf)  :
No: ()

False <= strict_subtree(node(ea, ta1, ta2), leaf)  :
Yes: {

}

eq_nat(ea, eb) <= strict_subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ea -> z  ;  eb -> s(_tumqw_0)  ;  ta1 -> node(_hvmqw_0, _hvmqw_1, _hvmqw_2)  ;  tb2 -> leaf
}

strict_subtree(ta1, tb1) <= strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ta1 -> leaf  ;  tb1 -> leaf  ;  tb2 -> node(_evmqw_0, _evmqw_1, _evmqw_2)
}


-------------------------------------------
Step 4, which took 0.012046 s (model generation: 0.011443,  model checking: 0.000603):

Clauses:
{
strict_subtree(leaf, node(eb, tb1, tb2)) <= True -> 0
strict_subtree(t1, t3) <= strict_subtree(t1, t2) /\ strict_subtree(t2, t3) -> 0
strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= strict_subtree(ta1, tb1) /\ strict_subtree(ta2, tb2) -> 0
strict_subtree(ta2, tb2) <= strict_subtree(ta1, tb1) /\ strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= strict_subtree(leaf, leaf) -> 0
False <= strict_subtree(node(ea, ta1, ta2), leaf) -> 0
eq_nat(ea, eb) <= strict_subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
strict_subtree(ta1, tb1) <= strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
strict_subtree(leaf, node(z, leaf, leaf)) <= True
strict_subtree(node(z, leaf, leaf), node(z, node(z, leaf, leaf), node(z, leaf, leaf))) <= True
False <= strict_subtree(node(z, leaf, leaf), leaf)
False <= strict_subtree(node(z, leaf, leaf), node(s(z), leaf, leaf))
False <= strict_subtree(node(z, leaf, leaf), node(z, leaf, leaf)) /\ strict_subtree(node(z, node(z, leaf, leaf), node(z, leaf, leaf)), node(z, node(z, leaf, leaf), leaf))
strict_subtree(leaf, leaf) <= strict_subtree(node(z, leaf, leaf), node(z, leaf, node(z, leaf, leaf)))
False <= strict_subtree(node(z, node(z, leaf, leaf), leaf), node(s(z), leaf, leaf))
False <= strict_subtree(node(z, node(z, leaf, leaf), leaf), node(z, leaf, leaf))
}

Current best model:
|_
name: None

strict_subtree ->
[
strict_subtree : <nattree * nattree>
{
  strict_subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
  strict_subtree(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= strict_subtree(x_0_2, x_1_1)
}
]



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




Answer of teacher:

strict_subtree(leaf, node(eb, tb1, tb2)) <= True  :
No: ()

strict_subtree(t1, t3) <= strict_subtree(t1, t2) /\ strict_subtree(t2, t3)  :
Yes: {
t1 -> node(_lvmqw_0, _lvmqw_1, node(_oxmqw_0, _oxmqw_1, leaf))  ;  t2 -> node(_mvmqw_0, node(_rxmqw_0, node(_eymqw_0, _eymqw_1, _eymqw_2), _rxmqw_2), leaf)  ;  t3 -> node(_nvmqw_0, node(_pxmqw_0, leaf, _pxmqw_2), _nvmqw_2)
}

strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= strict_subtree(ta1, tb1) /\ strict_subtree(ta2, tb2)  :
Yes: {
ta1 -> leaf  ;  ta2 -> node(_tvmqw_0, _tvmqw_1, leaf)  ;  tb1 -> node(_uvmqw_0, leaf, _uvmqw_2)  ;  tb2 -> node(_vvmqw_0, node(_ezmqw_0, _ezmqw_1, _ezmqw_2), _vvmqw_2)
}

strict_subtree(ta2, tb2) <= strict_subtree(ta1, tb1) /\ strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ta1 -> leaf  ;  ta2 -> leaf  ;  tb1 -> node(_gwmqw_0, _gwmqw_1, _gwmqw_2)  ;  tb2 -> leaf
}

False <= strict_subtree(leaf, leaf)  :
No: ()

False <= strict_subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_nat(ea, eb) <= strict_subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ea -> z  ;  eb -> s(_hxmqw_0)  ;  ta2 -> leaf  ;  tb1 -> node(_izmqw_0, _izmqw_1, _izmqw_2)
}

strict_subtree(ta1, tb1) <= strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ta1 -> node(_mxmqw_0, _mxmqw_1, node(_rymqw_0, _rymqw_1, _rymqw_2))  ;  ta2 -> leaf  ;  tb1 -> node(_nxmqw_0, leaf, _nxmqw_2)
}


-------------------------------------------
Step 5, which took 0.018384 s (model generation: 0.017336,  model checking: 0.001048):

Clauses:
{
strict_subtree(leaf, node(eb, tb1, tb2)) <= True -> 0
strict_subtree(t1, t3) <= strict_subtree(t1, t2) /\ strict_subtree(t2, t3) -> 0
strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= strict_subtree(ta1, tb1) /\ strict_subtree(ta2, tb2) -> 0
strict_subtree(ta2, tb2) <= strict_subtree(ta1, tb1) /\ strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= strict_subtree(leaf, leaf) -> 0
False <= strict_subtree(node(ea, ta1, ta2), leaf) -> 0
eq_nat(ea, eb) <= strict_subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
strict_subtree(ta1, tb1) <= strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
strict_subtree(leaf, node(z, leaf, leaf)) <= True
strict_subtree(node(z, leaf, leaf), node(z, node(z, leaf, leaf), node(z, leaf, leaf))) <= True
False <= strict_subtree(node(z, leaf, leaf), leaf)
False <= strict_subtree(node(z, leaf, leaf), node(s(z), leaf, leaf))
False <= strict_subtree(node(z, leaf, leaf), node(s(z), node(z, leaf, leaf), leaf))
False <= strict_subtree(node(z, leaf, leaf), node(z, leaf, leaf)) /\ strict_subtree(node(z, node(z, leaf, leaf), node(z, leaf, leaf)), node(z, node(z, leaf, leaf), leaf))
strict_subtree(leaf, leaf) <= strict_subtree(node(z, leaf, leaf), node(z, leaf, node(z, leaf, leaf)))
strict_subtree(leaf, leaf) <= strict_subtree(node(z, leaf, leaf), node(z, node(z, leaf, leaf), leaf))
strict_subtree(node(z, leaf, node(z, leaf, leaf)), node(z, node(z, leaf, leaf), node(z, node(z, leaf, leaf), leaf))) <= strict_subtree(node(z, leaf, leaf), node(z, node(z, leaf, leaf), leaf))
strict_subtree(node(z, leaf, node(z, leaf, leaf)), node(z, node(z, leaf, leaf), leaf)) <= strict_subtree(node(z, leaf, node(z, leaf, leaf)), node(z, node(z, node(z, leaf, leaf), leaf), leaf)) /\ strict_subtree(node(z, node(z, node(z, leaf, leaf), leaf), leaf), node(z, node(z, leaf, leaf), leaf))
False <= strict_subtree(node(z, node(z, leaf, leaf), leaf), node(s(z), leaf, leaf))
False <= strict_subtree(node(z, node(z, leaf, leaf), leaf), node(z, leaf, leaf))
strict_subtree(node(z, leaf, node(z, leaf, leaf)), node(z, leaf, leaf)) <= strict_subtree(node(z, node(z, leaf, node(z, leaf, leaf)), leaf), node(z, node(z, leaf, leaf), leaf))
}

Current best model:
|_
name: None

strict_subtree ->
[
strict_subtree : <nattree * nattree>
{
  strict_subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
  strict_subtree(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= strict_subtree(x_0_1, x_1_1) /\ strict_subtree(x_0_1, x_1_2)
}
]



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




Answer of teacher:

strict_subtree(leaf, node(eb, tb1, tb2)) <= True  :
No: ()

strict_subtree(t1, t3) <= strict_subtree(t1, t2) /\ strict_subtree(t2, t3)  :
No: ()

strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= strict_subtree(ta1, tb1) /\ strict_subtree(ta2, tb2)  :
Yes: {
ta1 -> node(_qanqw_0, leaf, _qanqw_2)  ;  ta2 -> leaf  ;  tb1 -> node(_sanqw_0, node(_idnqw_0, _idnqw_1, _idnqw_2), node(_idnqw_0, _idnqw_1, _idnqw_2))  ;  tb2 -> node(_tanqw_0, _tanqw_1, leaf)
}

strict_subtree(ta2, tb2) <= strict_subtree(ta1, tb1) /\ strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ta1 -> leaf  ;  ta2 -> node(_xbnqw_0, node(_ndnqw_0, _ndnqw_1, _ndnqw_2), _xbnqw_2)  ;  tb1 -> node(_ybnqw_0, _ybnqw_1, _ybnqw_2)  ;  tb2 -> node(_zbnqw_0, _zbnqw_1, leaf)
}

False <= strict_subtree(leaf, leaf)  :
No: ()

False <= strict_subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_nat(ea, eb) <= strict_subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ea -> z  ;  eb -> s(_jcnqw_0)  ;  ta1 -> leaf  ;  tb1 -> node(_adnqw_0, _adnqw_1, _adnqw_2)  ;  tb2 -> node(_adnqw_0, _adnqw_1, _adnqw_2)
}

strict_subtree(ta1, tb1) <= strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()


-------------------------------------------
Step 6, which took 0.059776 s (model generation: 0.058144,  model checking: 0.001632):

Clauses:
{
strict_subtree(leaf, node(eb, tb1, tb2)) <= True -> 0
strict_subtree(t1, t3) <= strict_subtree(t1, t2) /\ strict_subtree(t2, t3) -> 0
strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= strict_subtree(ta1, tb1) /\ strict_subtree(ta2, tb2) -> 0
strict_subtree(ta2, tb2) <= strict_subtree(ta1, tb1) /\ strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= strict_subtree(leaf, leaf) -> 0
False <= strict_subtree(node(ea, ta1, ta2), leaf) -> 0
eq_nat(ea, eb) <= strict_subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
strict_subtree(ta1, tb1) <= strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
strict_subtree(leaf, node(z, leaf, leaf)) <= True
strict_subtree(node(z, leaf, leaf), node(z, node(z, leaf, leaf), node(z, leaf, leaf))) <= True
strict_subtree(node(z, node(z, leaf, leaf), leaf), node(z, node(z, node(z, leaf, leaf), node(z, leaf, leaf)), node(z, leaf, leaf))) <= True
False <= strict_subtree(node(z, leaf, leaf), leaf)
False <= strict_subtree(node(z, leaf, leaf), node(s(z), leaf, leaf))
False <= strict_subtree(node(z, leaf, leaf), node(s(z), node(z, leaf, leaf), leaf))
False <= strict_subtree(node(z, leaf, leaf), node(s(z), node(z, leaf, leaf), node(z, leaf, leaf)))
False <= strict_subtree(node(z, leaf, leaf), node(z, leaf, leaf)) /\ strict_subtree(node(z, node(z, leaf, leaf), node(z, leaf, leaf)), node(z, node(z, leaf, leaf), leaf))
strict_subtree(leaf, leaf) <= strict_subtree(node(z, leaf, leaf), node(z, leaf, node(z, leaf, leaf)))
strict_subtree(leaf, leaf) <= strict_subtree(node(z, leaf, leaf), node(z, node(z, leaf, leaf), leaf))
strict_subtree(node(z, leaf, node(z, leaf, leaf)), node(z, node(z, leaf, leaf), node(z, node(z, leaf, leaf), leaf))) <= strict_subtree(node(z, leaf, leaf), node(z, node(z, leaf, leaf), leaf))
strict_subtree(node(z, leaf, node(z, leaf, leaf)), node(z, node(z, leaf, leaf), leaf)) <= strict_subtree(node(z, leaf, node(z, leaf, leaf)), node(z, node(z, node(z, leaf, leaf), leaf), leaf)) /\ strict_subtree(node(z, node(z, node(z, leaf, leaf), leaf), leaf), node(z, node(z, leaf, leaf), leaf))
False <= strict_subtree(node(z, leaf, node(z, node(z, leaf, leaf), leaf)), node(z, node(z, leaf, leaf), node(z, leaf, leaf)))
False <= strict_subtree(node(z, node(z, leaf, leaf), leaf), node(s(z), leaf, leaf))
False <= strict_subtree(node(z, node(z, leaf, leaf), leaf), node(z, leaf, leaf))
strict_subtree(node(z, leaf, node(z, leaf, leaf)), node(z, leaf, leaf)) <= strict_subtree(node(z, node(z, leaf, node(z, leaf, leaf)), leaf), node(z, node(z, leaf, leaf), leaf))
}

Current best model:
|_
name: None

strict_subtree ->
[
strict_subtree : <nattree * nattree>
{
  _r_1(z) <= True
  strict_subtree(leaf, leaf) <= True
  strict_subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
  strict_subtree(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_1_0) /\ strict_subtree(x_0_1, x_1_2) /\ strict_subtree(x_0_2, x_1_1)
}
]



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




Answer of teacher:

strict_subtree(leaf, node(eb, tb1, tb2)) <= True  :
No: ()

strict_subtree(t1, t3) <= strict_subtree(t1, t2) /\ strict_subtree(t2, t3)  :
Yes: {
t1 -> node(_yenqw_0, leaf, node(_rmnqw_0, leaf, leaf))  ;  t2 -> node(z, node(z, leaf, leaf), leaf)  ;  t3 -> node(z, node(s(_qlnqw_0), _smnqw_1, _smnqw_2), node(z, node(_wlnqw_0, _wlnqw_1, _wlnqw_2), node(_wlnqw_0, _wlnqw_1, _wlnqw_2)))
}

strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= strict_subtree(ta1, tb1) /\ strict_subtree(ta2, tb2)  :
Yes: {
eb -> s(_qlnqw_0)  ;  ta1 -> leaf  ;  ta2 -> leaf  ;  tb1 -> node(_tfnqw_0, _tfnqw_1, _tfnqw_2)  ;  tb2 -> node(_ufnqw_0, _ufnqw_1, _ufnqw_2)
}

strict_subtree(ta2, tb2) <= strict_subtree(ta1, tb1) /\ strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
eb -> z  ;  ta1 -> leaf  ;  ta2 -> node(_kjnqw_0, leaf, leaf)  ;  tb1 -> node(z, node(_hmnqw_0, _hmnqw_1, _hmnqw_2), node(_hmnqw_0, _hmnqw_1, _hmnqw_2))  ;  tb2 -> leaf
}

False <= strict_subtree(leaf, leaf)  :
Yes: {

}

False <= strict_subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_nat(ea, eb) <= strict_subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ea -> s(_dlnqw_0)  ;  eb -> z  ;  ta1 -> leaf  ;  ta2 -> leaf  ;  tb1 -> node(_hmnqw_0, _hmnqw_1, _hmnqw_2)  ;  tb2 -> node(_hmnqw_0, _hmnqw_1, _hmnqw_2)
}

strict_subtree(ta1, tb1) <= strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
eb -> z  ;  ta1 -> node(_hlnqw_0, leaf, leaf)  ;  ta2 -> leaf  ;  tb1 -> leaf  ;  tb2 -> node(z, node(_hmnqw_0, _hmnqw_1, _hmnqw_2), node(_hmnqw_0, _hmnqw_1, _hmnqw_2))
}


-------------------------------------------
Step 7, which took 0.069786 s (model generation: 0.067689,  model checking: 0.002097):

Clauses:
{
strict_subtree(leaf, node(eb, tb1, tb2)) <= True -> 0
strict_subtree(t1, t3) <= strict_subtree(t1, t2) /\ strict_subtree(t2, t3) -> 0
strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= strict_subtree(ta1, tb1) /\ strict_subtree(ta2, tb2) -> 0
strict_subtree(ta2, tb2) <= strict_subtree(ta1, tb1) /\ strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
False <= strict_subtree(leaf, leaf) -> 0
False <= strict_subtree(node(ea, ta1, ta2), leaf) -> 0
eq_nat(ea, eb) <= strict_subtree(node(ea, ta1, ta2), node(eb, tb1, tb2)) -> 0
strict_subtree(ta1, tb1) <= strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) -> 0
}

Accumulated learning constraints:
{
strict_subtree(leaf, node(z, leaf, leaf)) <= True
strict_subtree(node(s(z), leaf, leaf), node(s(z), node(z, leaf, leaf), node(z, leaf, leaf))) <= True
strict_subtree(node(z, leaf, leaf), node(z, node(z, leaf, leaf), node(z, leaf, leaf))) <= True
strict_subtree(node(z, node(z, leaf, leaf), leaf), node(z, node(z, node(z, leaf, leaf), node(z, leaf, leaf)), node(z, leaf, leaf))) <= True
False <= strict_subtree(leaf, leaf)
False <= strict_subtree(leaf, node(z, node(z, leaf, leaf), node(z, leaf, leaf))) /\ strict_subtree(node(z, leaf, node(z, leaf, leaf)), node(z, node(z, node(z, leaf, leaf), node(z, leaf, leaf)), leaf))
False <= strict_subtree(node(s(z), leaf, leaf), node(z, node(z, leaf, leaf), node(z, leaf, leaf)))
False <= strict_subtree(node(z, leaf, leaf), leaf)
False <= strict_subtree(node(z, leaf, leaf), node(s(z), leaf, leaf))
False <= strict_subtree(node(z, leaf, leaf), node(s(z), node(z, leaf, leaf), leaf))
False <= strict_subtree(node(z, leaf, leaf), node(s(z), node(z, leaf, leaf), node(z, leaf, leaf)))
False <= strict_subtree(node(z, leaf, leaf), node(z, leaf, leaf)) /\ strict_subtree(node(z, node(z, leaf, leaf), node(z, leaf, leaf)), node(z, node(z, leaf, leaf), leaf))
False <= strict_subtree(node(z, leaf, leaf), node(z, leaf, node(z, leaf, leaf)))
False <= strict_subtree(node(z, leaf, leaf), node(z, node(z, leaf, leaf), leaf))
strict_subtree(node(z, leaf, node(z, leaf, leaf)), node(z, node(s(z), leaf, leaf), node(z, node(z, leaf, leaf), node(z, leaf, leaf)))) <= strict_subtree(node(z, leaf, node(z, leaf, leaf)), node(z, node(z, leaf, leaf), leaf)) /\ strict_subtree(node(z, node(z, leaf, leaf), leaf), node(z, node(s(z), leaf, leaf), node(z, node(z, leaf, leaf), node(z, leaf, leaf))))
strict_subtree(node(z, leaf, node(z, leaf, leaf)), node(z, node(z, leaf, leaf), leaf)) <= strict_subtree(node(z, leaf, node(z, leaf, leaf)), node(z, node(z, node(z, leaf, leaf), leaf), leaf)) /\ strict_subtree(node(z, node(z, node(z, leaf, leaf), leaf), leaf), node(z, node(z, leaf, leaf), leaf))
False <= strict_subtree(node(z, leaf, node(z, node(z, leaf, leaf), leaf)), node(z, node(z, leaf, leaf), node(z, leaf, leaf)))
False <= strict_subtree(node(z, node(z, leaf, leaf), leaf), node(s(z), leaf, leaf))
False <= strict_subtree(node(z, node(z, leaf, leaf), leaf), node(z, leaf, leaf))
False <= strict_subtree(node(z, node(z, leaf, leaf), leaf), node(z, leaf, node(z, node(z, leaf, leaf), node(z, leaf, leaf))))
strict_subtree(node(z, leaf, node(z, leaf, leaf)), node(z, leaf, leaf)) <= strict_subtree(node(z, node(z, leaf, node(z, leaf, leaf)), leaf), node(z, node(z, leaf, leaf), leaf))
}

Current best model:
|_
name: None

strict_subtree ->
[
strict_subtree : <nattree * nattree>
{
  _r_1(s(x_0_0), s(x_1_0)) <= True
  _r_1(z, z) <= True
  strict_subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
  strict_subtree(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_0_0, x_1_0) /\ strict_subtree(x_0_1, x_1_1) /\ strict_subtree(x_0_2, x_1_2)
}
]



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




Answer of teacher:

strict_subtree(leaf, node(eb, tb1, tb2)) <= True  :
No: ()

strict_subtree(t1, t3) <= strict_subtree(t1, t2) /\ strict_subtree(t2, t3)  :
No: ()

strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2)) <= strict_subtree(ta1, tb1) /\ strict_subtree(ta2, tb2)  :
No: ()

strict_subtree(ta2, tb2) <= strict_subtree(ta1, tb1) /\ strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()

False <= strict_subtree(leaf, leaf)  :
No: ()

False <= strict_subtree(node(ea, ta1, ta2), leaf)  :
No: ()

eq_nat(ea, eb) <= strict_subtree(node(ea, ta1, ta2), node(eb, tb1, tb2))  :
Yes: {
ea -> s(z)  ;  eb -> s(s(_naoqw_0))  ;  ta1 -> leaf  ;  ta2 -> leaf  ;  tb1 -> node(_vtnqw_0, _vtnqw_1, _vtnqw_2)  ;  tb2 -> node(_vtnqw_0, _vtnqw_1, _vtnqw_2)
}

strict_subtree(ta1, tb1) <= strict_subtree(node(eb, ta1, ta2), node(eb, tb1, tb2))  :
No: ()


Total time: 0.266356
Learner time: 0.186632
Teacher time: 0.006696
Reasons for stopping: Yes: |_
name: None

strict_subtree ->
[
strict_subtree : <nattree * nattree>
{
  _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0)
  _r_1(z, z) <= True
  strict_subtree(leaf, node(x_1_0, x_1_1, x_1_2)) <= True
  strict_subtree(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_0_0, x_1_0) /\ strict_subtree(x_0_1, x_1_1) /\ strict_subtree(x_0_2, x_1_2)
}
]



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