Solving ../../benchmarks/smtlib/true/tree_height_numnodes_le.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: { (not_empty, P: { not_empty(node(e, t1, t2)) <= True False <= not_empty(leaf) } ) (leq_nat, P: { leq_nat(z, n2) <= True leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) False <= leq_nat(s(nn1), z) } ) (le_nat, P: { le_nat(z, s(nn2)) <= True le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) False <= le_nat(s(nn1), z) False <= le_nat(z, z) } ) (max, F: { max(s(nn), z, s(nn)) <= True max(z, m, m) <= True max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) } eq_nat(_jw, _kw) <= max(_hw, _iw, _jw) /\ max(_hw, _iw, _kw) ) (height, F: { height(leaf, z) <= True height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) } eq_nat(_pw, _qw) <= height(_ow, _pw) /\ height(_ow, _qw) ) (plus, F: { plus(n, z, n) <= True plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) } eq_nat(_uw, _vw) <= plus(_sw, _tw, _uw) /\ plus(_sw, _tw, _vw) ) (numnodes, F: { numnodes(leaf, z) <= True numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) } eq_nat(_ax, _bx) <= numnodes(_zw, _ax) /\ numnodes(_zw, _bx) ) } properties: { le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) } over-approximation: {height, leq_nat, max, not_empty, numnodes, plus} under-approximation: {le_nat, leq_nat} Clause system for inference is: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Solving took 59.697220 seconds. Maybe: timeout during learnerLast solver state: Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le_nat(s(s(z)), s(s(s(z)))) <= True max(s(z), s(z), s(z)) <= True max(s(z), z, s(z)) <= True max(z, s(z), s(z)) <= True max(z, z, z) <= True not_empty(node(a, leaf, leaf)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), 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 height(node(a, leaf, leaf), s(s(z))) <= height(leaf, s(z)) height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= height(node(a, leaf, leaf), s(s(z))) /\ height(node(a, leaf, leaf), z) /\ max(z, s(s(z)), s(s(z))) le_nat(s(s(z)), s(z)) <= height(node(a, leaf, leaf), s(s(z))) /\ not_empty(leaf) height(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) <= height(node(a, leaf, leaf), z) /\ height(node(a, node(a, leaf, leaf), leaf), s(z)) /\ max(z, s(z), s(s(z))) height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) height(node(a, leaf, node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(z))) <= height(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) /\ max(z, s(s(s(z))), s(z)) height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z)) height(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(z)) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), leaf), s(z)) /\ not_empty(leaf) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) le_nat(s(s(s(z))), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) le_nat(s(z), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), z) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), z) le_nat(s(s(s(z))), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(s(z)))) /\ not_empty(node(a, leaf, node(a, leaf, node(a, leaf, leaf)))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(s(z)))) le_nat(s(s(s(z))), s(s(z))) <= height(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))), s(s(s(z)))) /\ not_empty(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))), s(s(z))) le_nat(s(s(s(s(s(z))))), s(s(s(s(s(z)))))) <= height(node(a, node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))), node(b, leaf, leaf)), s(s(s(s(s(z)))))) /\ not_empty(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)))) /\ not_empty(node(b, leaf, leaf)) /\ numnodes(node(a, node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))), node(b, leaf, leaf)), s(s(s(s(s(z)))))) le_nat(s(s(s(s(z)))), s(s(s(s(z))))) <= height(node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), node(a, leaf, leaf)), s(s(s(s(z))))) /\ not_empty(node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) /\ numnodes(node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), node(a, leaf, leaf)), s(s(s(s(z))))) False <= le_nat(s(s(z)), s(s(z))) le_nat(z, s(z)) <= le_nat(s(z), s(s(z))) False <= le_nat(s(z), s(z)) False <= le_nat(s(z), z) le_nat(s(z), s(s(z))) <= le_nat(z, s(z)) False <= le_nat(z, z) height(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z))) numnodes(node(a, leaf, leaf), s(s(z))) <= numnodes(leaf, s(z)) numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(z))) <= numnodes(leaf, s(z)) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z)) numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(z))) <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(z)) numnodes(node(a, node(a, leaf, node(b, node(a, leaf, leaf), node(a, leaf, leaf))), node(a, leaf, node(b, node(a, leaf, leaf), node(a, leaf, leaf)))), s(s(s(z)))) <= numnodes(node(a, leaf, node(b, node(a, leaf, leaf), node(a, leaf, leaf))), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) le_nat(s(s(z)), s(z)) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(s(z)))) <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(z)) numnodes(node(a, node(b, node(a, leaf, leaf), leaf), node(b, leaf, leaf)), s(s(s(z)))) <= numnodes(node(b, leaf, leaf), s(z)) /\ numnodes(node(b, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(s(z))) plus(s(s(z)), s(z), s(s(z))) <= plus(s(s(z)), z, s(z)) False <= plus(s(z), s(z), s(z)) numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= plus(s(z), z, s(s(z))) numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None height -> [ height : { _r_1(leaf, s(x_1_0)) <= True _r_1(leaf, z) <= True _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ _r_2(x_0_1, x_1_0) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ _r_2(x_0_2, x_1_0) /\ not_empty(x_0_1) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ not_empty(x_0_1) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ not_empty(x_0_1) /\ numnodes(x_0_2, x_1_0) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= not_empty(x_0_1) _r_2(leaf, s(x_1_0)) <= True _r_2(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_1, x_1_0) /\ not_empty(x_0_2) _r_2(node(x_0_0, x_0_1, x_0_2), z) <= True height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_2(x_0_2, x_1_0) /\ not_empty(x_0_1) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ height(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ not_empty(x_0_2) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ height(x_0_1, x_1_0) /\ not_empty(x_0_1) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ not_empty(x_0_2) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0) /\ not_empty(x_0_2) not_empty(node(x_0_0, x_0_1, x_0_2)) <= True numnodes(leaf, s(x_1_0)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_1(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_1(x_0_2, x_1_0) /\ not_empty(x_0_1) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_1(x_0_2, x_1_0) /\ not_empty(x_0_2) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_2(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ not_empty(x_0_1) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ not_empty(x_0_1) /\ numnodes(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ not_empty(x_0_2) /\ numnodes(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ numnodes(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0) } ] ; le_nat -> [ le_nat : { le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0) le_nat(z, s(x_1_0)) <= True } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= True max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] ; not_empty -> [ not_empty : { not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; numnodes -> [ numnodes : { _r_1(leaf, s(x_1_0)) <= True _r_1(leaf, z) <= True _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ _r_2(x_0_1, x_1_0) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ _r_2(x_0_2, x_1_0) /\ not_empty(x_0_1) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ not_empty(x_0_1) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ not_empty(x_0_1) /\ numnodes(x_0_2, x_1_0) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= not_empty(x_0_1) _r_2(leaf, s(x_1_0)) <= True _r_2(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_1, x_1_0) /\ not_empty(x_0_2) _r_2(node(x_0_0, x_0_1, x_0_2), z) <= True height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_2(x_0_2, x_1_0) /\ not_empty(x_0_1) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ height(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ not_empty(x_0_2) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ height(x_0_1, x_1_0) /\ not_empty(x_0_1) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ not_empty(x_0_2) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0) /\ not_empty(x_0_2) not_empty(node(x_0_0, x_0_1, x_0_2)) <= True numnodes(leaf, s(x_1_0)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_1(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_1(x_0_2, x_1_0) /\ not_empty(x_0_1) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_1(x_0_2, x_1_0) /\ not_empty(x_0_2) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_2(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ not_empty(x_0_1) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ not_empty(x_0_1) /\ numnodes(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ not_empty(x_0_2) /\ numnodes(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ numnodes(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0) } ] ; plus -> [ plus : { le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0) le_nat(z, s(x_1_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= le_nat(x_1_0, x_2_0) 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.005931 s (model generation: 0.005823, model checking: 0.000108): Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { } Current best model: |_ name: None height -> [ height : { } ] ; le_nat -> [ le_nat : { } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { } ] ; not_empty -> [ not_empty : { } ] ; numnodes -> [ numnodes : { } ] ; plus -> [ plus : { } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: height(leaf, z) <= True : Yes: { } max(s(nn), z, s(nn)) <= True : Yes: { } max(z, m, m) <= True : Yes: { m -> z } not_empty(node(e, t1, t2)) <= True : Yes: { } numnodes(leaf, z) <= True : Yes: { } plus(n, z, n) <= True : Yes: { n -> z } height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) : No: () le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) : No: () le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) : No: () le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) : No: () False <= le_nat(s(nn1), z) : No: () False <= le_nat(z, z) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) : No: () numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) : No: () plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) : No: () ------------------------------------------- Step 1, which took 0.010293 s (model generation: 0.010159, model checking: 0.000134): Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { height(leaf, z) <= True max(s(z), z, s(z)) <= True max(z, z, z) <= True not_empty(node(a, leaf, leaf)) <= True numnodes(leaf, z) <= True plus(z, z, z) <= True } Current best model: |_ name: None height -> [ height : { height(leaf, z) <= True } ] ; le_nat -> [ le_nat : { } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { max(s(x_0_0), z, s(x_2_0)) <= True max(z, z, z) <= True } ] ; not_empty -> [ not_empty : { not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; numnodes -> [ numnodes : { numnodes(leaf, z) <= True } ] ; plus -> [ plus : { plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: height(leaf, z) <= True : No: () max(s(nn), z, s(nn)) <= True : No: () max(z, m, m) <= True : Yes: { m -> s(_myyaw_0) } not_empty(node(e, t1, t2)) <= True : No: () numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : Yes: { n -> s(_nyyaw_0) } height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) : Yes: { _lw -> z ; _mw -> z ; _nw -> z ; t1 -> leaf ; t2 -> leaf } le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) : No: () le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) : No: () le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) : No: () False <= le_nat(s(nn1), z) : No: () False <= le_nat(z, z) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) : Yes: { _gw -> z ; mm -> z ; nn -> z } numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) : Yes: { _ww -> z ; _xw -> z ; _yw -> z ; t1 -> leaf ; t2 -> leaf } plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) : Yes: { _rw -> z ; mm -> z ; n -> z } ------------------------------------------- Step 2, which took 0.009523 s (model generation: 0.009401, model checking: 0.000122): Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True max(s(z), s(z), s(z)) <= True max(s(z), z, s(z)) <= True max(z, s(z), s(z)) <= True max(z, z, z) <= True not_empty(node(a, 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 } Current best model: |_ name: None height -> [ height : { height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True } ] ; le_nat -> [ le_nat : { } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= True max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] ; not_empty -> [ not_empty : { not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; numnodes -> [ numnodes : { numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True } ] ; plus -> [ plus : { 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: height(leaf, z) <= True : No: () max(s(nn), z, s(nn)) <= True : No: () max(z, m, m) <= True : No: () not_empty(node(e, t1, t2)) <= True : No: () numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) : No: () le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) : Yes: { _cx -> s(_hzyaw_0) ; _dx -> s(_izyaw_0) ; t1 -> node(_jzyaw_0, _jzyaw_1, _jzyaw_2) ; t2 -> node(_kzyaw_0, _kzyaw_1, _kzyaw_2) } le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) : No: () le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) : No: () False <= le_nat(s(nn1), z) : No: () False <= le_nat(z, z) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) : No: () numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) : No: () plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) : Yes: { _rw -> s(_lzyaw_0) ; mm -> z ; n -> s(_nzyaw_0) } ------------------------------------------- Step 3, which took 0.010725 s (model generation: 0.010619, model checking: 0.000106): Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True max(s(z), s(z), s(z)) <= True max(s(z), z, s(z)) <= True max(z, s(z), s(z)) <= True max(z, z, z) <= True not_empty(node(a, 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 le_nat(s(z), s(z)) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) } Current best model: |_ name: None height -> [ height : { height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True } ] ; le_nat -> [ le_nat : { le_nat(s(x_0_0), s(x_1_0)) <= True } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= True max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] ; not_empty -> [ not_empty : { not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; numnodes -> [ numnodes : { numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True } ] ; plus -> [ plus : { 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: height(leaf, z) <= True : No: () max(s(nn), z, s(nn)) <= True : No: () max(z, m, m) <= True : No: () not_empty(node(e, t1, t2)) <= True : No: () numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) : No: () le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) : No: () le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) : No: () le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) : Yes: { nn1 -> z ; nn2 -> z } False <= le_nat(s(nn1), z) : No: () False <= le_nat(z, z) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) : No: () numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) : No: () plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) : No: () ------------------------------------------- Step 4, which took 0.010627 s (model generation: 0.010461, model checking: 0.000166): Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True max(s(z), s(z), s(z)) <= True max(s(z), z, s(z)) <= True max(z, s(z), s(z)) <= True max(z, z, z) <= True not_empty(node(a, 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 le_nat(s(z), s(z)) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) le_nat(z, z) <= le_nat(s(z), s(z)) } Current best model: |_ name: None height -> [ height : { height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True } ] ; le_nat -> [ le_nat : { le_nat(s(x_0_0), s(x_1_0)) <= True le_nat(z, z) <= True } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= True max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] ; not_empty -> [ not_empty : { not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; numnodes -> [ numnodes : { numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True } ] ; plus -> [ plus : { 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: height(leaf, z) <= True : No: () max(s(nn), z, s(nn)) <= True : No: () max(z, m, m) <= True : No: () not_empty(node(e, t1, t2)) <= True : No: () numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) : No: () le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) : No: () le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) : No: () le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) : Yes: { nn1 -> z ; nn2 -> s(_xzyaw_0) } False <= le_nat(s(nn1), z) : No: () False <= le_nat(z, z) : Yes: { } leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) : No: () numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) : No: () plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) : No: () ------------------------------------------- Step 5, which took 0.011055 s (model generation: 0.010623, model checking: 0.000432): Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True max(s(z), s(z), s(z)) <= True max(s(z), z, s(z)) <= True max(z, s(z), s(z)) <= True max(z, z, z) <= True not_empty(node(a, 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 <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) le_nat(z, s(z)) <= le_nat(s(z), s(s(z))) False <= le_nat(s(z), s(z)) False <= le_nat(z, z) } Current best model: |_ name: None height -> [ height : { height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0) numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True } ] ; le_nat -> [ le_nat : { le_nat(z, s(x_1_0)) <= True } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= True max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] ; not_empty -> [ not_empty : { not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; numnodes -> [ numnodes : { numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True } ] ; plus -> [ plus : { 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: height(leaf, z) <= True : No: () max(s(nn), z, s(nn)) <= True : No: () max(z, m, m) <= True : No: () not_empty(node(e, t1, t2)) <= True : No: () numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) : Yes: { _lw -> z ; _mw -> s(s(_cbzaw_0)) ; _nw -> s(_fazaw_0) ; t1 -> leaf ; t2 -> node(_hazaw_0, node(_bbzaw_0, _bbzaw_1, _bbzaw_2), _hazaw_2) } le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) : Yes: { _cx -> s(s(_yazaw_0)) ; _dx -> s(_tazaw_0) ; t1 -> node(_uazaw_0, _uazaw_1, _uazaw_2) ; t2 -> node(_vazaw_0, _vazaw_1, _vazaw_2) } le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) : Yes: { nn1 -> z ; nn2 -> s(_xazaw_0) } le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) : No: () False <= le_nat(s(nn1), z) : No: () False <= le_nat(z, z) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) : No: () numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) : No: () plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) : No: () ------------------------------------------- Step 6, which took 0.014354 s (model generation: 0.014150, model checking: 0.000204): Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True max(s(z), s(z), s(z)) <= True max(s(z), z, s(z)) <= True max(z, s(z), s(z)) <= True max(z, z, z) <= True not_empty(node(a, 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 height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z)) le_nat(s(s(z)), s(z)) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) le_nat(z, s(z)) <= le_nat(s(z), s(s(z))) False <= le_nat(s(z), s(z)) le_nat(s(z), s(s(z))) <= le_nat(z, s(z)) False <= le_nat(z, z) } Current best model: |_ name: None height -> [ height : { height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True } ] ; le_nat -> [ le_nat : { } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= True max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] ; not_empty -> [ not_empty : { not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; numnodes -> [ numnodes : { numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_2, x_1_0) } ] ; plus -> [ plus : { 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: height(leaf, z) <= True : No: () max(s(nn), z, s(nn)) <= True : No: () max(z, m, m) <= True : No: () not_empty(node(e, t1, t2)) <= True : No: () numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) : No: () le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) : Yes: { _cx -> s(_dbzaw_0) ; _dx -> s(s(z)) ; t1 -> node(_fbzaw_0, _fbzaw_1, _fbzaw_2) ; t2 -> node(_gbzaw_0, _gbzaw_1, leaf) } le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) : No: () le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) : No: () False <= le_nat(s(nn1), z) : No: () False <= le_nat(z, z) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) : No: () numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) : Yes: { _ww -> s(z) ; _xw -> z ; _yw -> s(_tbzaw_0) ; t1 -> node(_ubzaw_0, _ubzaw_1, leaf) ; t2 -> leaf } plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) : No: () ------------------------------------------- Step 7, which took 0.018260 s (model generation: 0.017819, model checking: 0.000441): Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True max(s(z), s(z), s(z)) <= True max(s(z), z, s(z)) <= True max(z, s(z), s(z)) <= True max(z, z, z) <= True not_empty(node(a, leaf, leaf)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, node(a, leaf, leaf), leaf), 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 height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z)) le_nat(s(s(z)), s(z)) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) le_nat(s(z), s(s(z))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) le_nat(z, s(z)) <= le_nat(s(z), s(s(z))) False <= le_nat(s(z), s(z)) le_nat(s(z), s(s(z))) <= le_nat(z, s(z)) False <= le_nat(z, z) } Current best model: |_ name: None height -> [ height : { height(leaf, s(x_1_0)) <= True height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_2, x_1_0) numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0) } ] ; le_nat -> [ le_nat : { } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= True max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] ; not_empty -> [ not_empty : { not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; numnodes -> [ numnodes : { height(leaf, s(x_1_0)) <= True height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_2, x_1_0) numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0) } ] ; plus -> [ plus : { 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: height(leaf, z) <= True : No: () max(s(nn), z, s(nn)) <= True : No: () max(z, m, m) <= True : No: () not_empty(node(e, t1, t2)) <= True : No: () numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) : Yes: { _lw -> z ; _mw -> s(_wczaw_0) ; _nw -> s(_xczaw_0) ; t1 -> leaf ; t2 -> leaf } le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) : Yes: { _cx -> s(s(z)) ; _dx -> s(s(z)) ; t1 -> node(_bezaw_0, _bezaw_1, _bezaw_2) ; t2 -> node(_cezaw_0, _cezaw_1, leaf) } le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) : No: () le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) : No: () False <= le_nat(s(nn1), z) : No: () False <= le_nat(z, z) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) : No: () numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) : Yes: { _ww -> z ; _xw -> s(z) ; _yw -> s(s(_cgzaw_0)) ; t1 -> leaf ; t2 -> node(_mezaw_0, _mezaw_1, leaf) } plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) : No: () ------------------------------------------- Step 8, which took 0.048398 s (model generation: 0.048139, model checking: 0.000259): Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True max(s(z), s(z), s(z)) <= True max(s(z), z, s(z)) <= True max(z, s(z), s(z)) <= True max(z, z, z) <= True not_empty(node(a, leaf, leaf)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, node(a, leaf, leaf), leaf), 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 height(node(a, leaf, leaf), s(s(z))) <= height(leaf, s(z)) height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z)) le_nat(s(s(z)), s(s(z))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) le_nat(s(s(z)), s(z)) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) le_nat(s(z), s(s(z))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) le_nat(z, s(z)) <= le_nat(s(z), s(s(z))) False <= le_nat(s(z), s(z)) le_nat(s(z), s(s(z))) <= le_nat(z, s(z)) False <= le_nat(z, z) numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None height -> [ height : { _r_1(leaf) <= True height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1) } ] ; le_nat -> [ le_nat : { } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= True max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] ; not_empty -> [ not_empty : { not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; numnodes -> [ numnodes : { numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True } ] ; plus -> [ plus : { 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: height(leaf, z) <= True : No: () max(s(nn), z, s(nn)) <= True : No: () max(z, m, m) <= True : No: () not_empty(node(e, t1, t2)) <= True : No: () numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) : Yes: { _lw -> s(_sgzaw_0) ; _mw -> s(_tgzaw_0) ; _nw -> s(_ugzaw_0) ; t1 -> node(_vgzaw_0, leaf, _vgzaw_2) ; t2 -> node(_wgzaw_0, leaf, _wgzaw_2) } le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) : No: () le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) : No: () le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) : No: () False <= le_nat(s(nn1), z) : No: () False <= le_nat(z, z) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) : No: () numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) : No: () plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) : No: () ------------------------------------------- Step 9, which took 0.051038 s (model generation: 0.050712, model checking: 0.000326): Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True max(s(z), s(z), s(z)) <= True max(s(z), z, s(z)) <= True max(z, s(z), s(z)) <= True max(z, z, z) <= True not_empty(node(a, leaf, leaf)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, node(a, leaf, leaf), leaf), 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 height(node(a, leaf, leaf), s(s(z))) <= height(leaf, s(z)) height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z)) le_nat(s(z), s(s(z))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) le_nat(z, s(z)) <= le_nat(s(z), s(s(z))) False <= le_nat(s(z), s(z)) le_nat(s(z), s(s(z))) <= le_nat(z, s(z)) False <= le_nat(z, z) le_nat(s(s(z)), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) le_nat(s(s(z)), s(z)) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None height -> [ height : { height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True } ] ; le_nat -> [ le_nat : { } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= True max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] ; not_empty -> [ not_empty : { not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; numnodes -> [ numnodes : { _r_1(leaf) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2) } ] ; plus -> [ plus : { 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: height(leaf, z) <= True : No: () max(s(nn), z, s(nn)) <= True : No: () max(z, m, m) <= True : No: () not_empty(node(e, t1, t2)) <= True : No: () numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) : No: () le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) : No: () le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) : No: () le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) : No: () False <= le_nat(s(nn1), z) : No: () False <= le_nat(z, z) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) : No: () numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) : Yes: { _ww -> s(_zizaw_0) ; _xw -> s(_ajzaw_0) ; _yw -> s(_bjzaw_0) ; t1 -> node(_cjzaw_0, _cjzaw_1, leaf) ; t2 -> node(_djzaw_0, _djzaw_1, leaf) } plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) : No: () ------------------------------------------- Step 10, which took 0.052211 s (model generation: 0.051806, model checking: 0.000405): Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True max(s(z), s(z), s(z)) <= True max(s(z), z, s(z)) <= True max(z, s(z), s(z)) <= True max(z, z, z) <= True not_empty(node(a, leaf, leaf)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, node(a, leaf, leaf), leaf), 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 height(node(a, leaf, leaf), s(s(z))) <= height(leaf, s(z)) height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z)) le_nat(s(z), s(s(z))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) le_nat(z, s(z)) <= le_nat(s(z), s(s(z))) False <= le_nat(s(z), s(z)) le_nat(s(z), s(s(z))) <= le_nat(z, s(z)) False <= le_nat(z, z) le_nat(s(s(z)), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) le_nat(s(s(z)), s(z)) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= plus(s(z), s(z), s(z)) numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None height -> [ height : { height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True } ] ; le_nat -> [ le_nat : { _r_1(s(x_0_0)) <= True le_nat(s(x_0_0), s(x_1_0)) <= _r_1(x_1_0) le_nat(z, s(x_1_0)) <= True } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= True max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] ; not_empty -> [ not_empty : { not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; numnodes -> [ numnodes : { numnodes(leaf, s(x_1_0)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0) } ] ; plus -> [ plus : { 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: height(leaf, z) <= True : No: () max(s(nn), z, s(nn)) <= True : No: () max(z, m, m) <= True : No: () not_empty(node(e, t1, t2)) <= True : No: () numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) : No: () le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) : No: () le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) : No: () le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) : Yes: { nn1 -> s(_njzaw_0) ; nn2 -> s(z) } False <= le_nat(s(nn1), z) : No: () False <= le_nat(z, z) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) : No: () numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) : Yes: { _ww -> s(s(s(z))) ; _xw -> s(_ykzaw_0) ; _yw -> s(z) ; t1 -> node(_alzaw_0, node(_xlzaw_0, node(_omzaw_0, leaf, _omzaw_2), _xlzaw_2), _alzaw_2) ; t2 -> leaf } plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) : No: () ------------------------------------------- Step 11, which took 0.067530 s (model generation: 0.067067, model checking: 0.000463): Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True max(s(z), s(z), s(z)) <= True max(s(z), z, s(z)) <= True max(z, s(z), s(z)) <= True max(z, z, z) <= True not_empty(node(a, leaf, leaf)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, node(a, leaf, leaf), leaf), 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 height(node(a, leaf, leaf), s(s(z))) <= height(leaf, s(z)) height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z)) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= le_nat(s(s(z)), s(s(z))) le_nat(z, s(z)) <= le_nat(s(z), s(s(z))) False <= le_nat(s(z), s(z)) le_nat(s(z), s(s(z))) <= le_nat(z, s(z)) False <= le_nat(z, z) numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(z))) <= numnodes(leaf, s(z)) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) le_nat(s(s(z)), s(z)) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= plus(s(z), s(z), s(z)) numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None height -> [ height : { height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True } ] ; le_nat -> [ le_nat : { le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0) le_nat(s(x_0_0), z) <= True le_nat(z, s(x_1_0)) <= True } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= True max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] ; not_empty -> [ not_empty : { not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; numnodes -> [ numnodes : { _r_1(leaf) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2) } ] ; plus -> [ plus : { le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0) le_nat(s(x_0_0), z) <= True le_nat(z, s(x_1_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= le_nat(x_1_0, x_2_0) 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: height(leaf, z) <= True : No: () max(s(nn), z, s(nn)) <= True : No: () max(z, m, m) <= True : No: () not_empty(node(e, t1, t2)) <= True : No: () numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) : No: () le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) : No: () le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) : No: () le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) : No: () False <= le_nat(s(nn1), z) : Yes: { } False <= le_nat(z, z) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) : No: () numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) : Yes: { _ww -> s(_xozaw_0) ; _xw -> s(z) ; _yw -> s(s(_npzaw_0)) ; t1 -> node(_apzaw_0, _apzaw_1, leaf) ; t2 -> node(_bpzaw_0, _bpzaw_1, leaf) } plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) : No: () ------------------------------------------- Step 12, which took 0.199202 s (model generation: 0.198828, model checking: 0.000374): Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True max(s(z), s(z), s(z)) <= True max(s(z), z, s(z)) <= True max(z, s(z), s(z)) <= True max(z, z, z) <= True not_empty(node(a, leaf, leaf)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), 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 height(node(a, leaf, leaf), s(s(z))) <= height(leaf, s(z)) height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z)) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= le_nat(s(s(z)), s(s(z))) le_nat(z, s(z)) <= le_nat(s(z), s(s(z))) False <= le_nat(s(z), s(z)) False <= le_nat(s(z), z) le_nat(s(z), s(s(z))) <= le_nat(z, s(z)) False <= le_nat(z, z) numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(z))) <= numnodes(leaf, s(z)) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) le_nat(s(s(z)), s(z)) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= plus(s(z), s(z), s(z)) numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None height -> [ height : { height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True } ] ; le_nat -> [ le_nat : { } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= True max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] ; not_empty -> [ not_empty : { not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; numnodes -> [ numnodes : { _r_1(leaf, s(x_1_0)) <= True _r_1(leaf, z) <= True _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_1_0) _r_2(s(x_0_0)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) } ] ; plus -> [ plus : { _r_2(s(x_0_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_2_0) plus(s(x_0_0), z, s(x_2_0)) <= 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: height(leaf, z) <= True : No: () max(s(nn), z, s(nn)) <= True : No: () max(z, m, m) <= True : No: () not_empty(node(e, t1, t2)) <= True : No: () numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) : No: () le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) : Yes: { _cx -> s(_vpzaw_0) ; _dx -> s(s(s(_grzaw_0))) ; t1 -> node(_xpzaw_0, _xpzaw_1, _xpzaw_2) ; t2 -> node(_ypzaw_0, _ypzaw_1, _ypzaw_2) } le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) : No: () le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) : No: () False <= le_nat(s(nn1), z) : No: () False <= le_nat(z, z) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) : No: () numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) : Yes: { _ww -> z ; _xw -> s(s(s(_grzaw_0))) ; _yw -> s(z) ; t1 -> leaf ; t2 -> node(_iqzaw_0, _iqzaw_1, node(_lrzaw_0, _lrzaw_1, _lrzaw_2)) } plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) : No: () ------------------------------------------- Step 13, which took 0.368030 s (model generation: 0.367067, model checking: 0.000963): Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True max(s(z), s(z), s(z)) <= True max(s(z), z, s(z)) <= True max(z, s(z), s(z)) <= True max(z, z, z) <= True not_empty(node(a, leaf, leaf)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), 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 height(node(a, leaf, leaf), s(s(z))) <= height(leaf, s(z)) height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z)) le_nat(s(z), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= le_nat(s(s(z)), s(s(z))) le_nat(z, s(z)) <= le_nat(s(z), s(s(z))) False <= le_nat(s(z), s(z)) False <= le_nat(s(z), z) le_nat(s(z), s(s(z))) <= le_nat(z, s(z)) False <= le_nat(z, z) numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(z))) <= numnodes(leaf, s(z)) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z)) numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(z))) <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) le_nat(s(s(z)), s(z)) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= plus(s(z), s(z), s(z)) numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None height -> [ height : { height(leaf, s(x_1_0)) <= True height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0) } ] ; le_nat -> [ le_nat : { } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= True max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] ; not_empty -> [ not_empty : { not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; numnodes -> [ numnodes : { _r_1(leaf, s(x_1_0)) <= True _r_1(leaf, z) <= True _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_1_0) _r_2(s(x_0_0)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) } ] ; plus -> [ plus : { _r_2(s(x_0_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_2_0) plus(s(x_0_0), z, s(x_2_0)) <= 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: height(leaf, z) <= True : No: () max(s(nn), z, s(nn)) <= True : No: () max(z, m, m) <= True : No: () not_empty(node(e, t1, t2)) <= True : No: () numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) : Yes: { _lw -> z ; _mw -> s(s(s(z))) ; _nw -> s(z) ; t1 -> leaf ; t2 -> node(_rszaw_0, _rszaw_1, node(_vxzaw_0, _vxzaw_1, node(_gaabw_0, _gaabw_1, leaf))) } le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) : Yes: { _cx -> s(s(z)) ; _dx -> s(s(s(_xxzaw_0))) ; t1 -> node(_ntzaw_0, _ntzaw_1, _ntzaw_2) ; t2 -> node(_otzaw_0, _otzaw_1, leaf) } le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) : No: () le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) : No: () False <= le_nat(s(nn1), z) : No: () False <= le_nat(z, z) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) : No: () numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) : No: () plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) : No: () ------------------------------------------- Step 14, which took 0.617469 s (model generation: 0.616787, model checking: 0.000682): Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le_nat(s(s(z)), s(s(s(z)))) <= True max(s(z), s(z), s(z)) <= True max(s(z), z, s(z)) <= True max(z, s(z), s(z)) <= True max(z, z, z) <= True not_empty(node(a, leaf, leaf)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), 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 height(node(a, leaf, leaf), s(s(z))) <= height(leaf, s(z)) height(node(a, leaf, node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(z))) <= height(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) /\ max(z, s(s(s(z))), s(z)) height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z)) le_nat(s(z), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= le_nat(s(s(z)), s(s(z))) le_nat(z, s(z)) <= le_nat(s(z), s(s(z))) False <= le_nat(s(z), s(z)) False <= le_nat(s(z), z) le_nat(s(z), s(s(z))) <= le_nat(z, s(z)) False <= le_nat(z, z) numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(z))) <= numnodes(leaf, s(z)) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z)) numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(z))) <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) le_nat(s(s(z)), s(z)) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= plus(s(z), s(z), s(z)) numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None height -> [ height : { height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True } ] ; le_nat -> [ le_nat : { le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0) le_nat(z, s(x_1_0)) <= True } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= True max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] ; not_empty -> [ not_empty : { not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; numnodes -> [ numnodes : { _r_1(leaf, s(x_1_0)) <= True _r_1(leaf, z) <= True _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_0, x_1_0) _r_2(a, s(x_1_0)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) } ] ; plus -> [ plus : { le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0) le_nat(z, s(x_1_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= le_nat(x_1_0, x_2_0) 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: height(leaf, z) <= True : No: () max(s(nn), z, s(nn)) <= True : No: () max(z, m, m) <= True : No: () not_empty(node(e, t1, t2)) <= True : No: () numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) : No: () le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) : Yes: { _cx -> s(s(s(z))) ; _dx -> s(s(s(z))) ; t1 -> node(_beabw_0, _beabw_1, _beabw_2) ; t2 -> node(a, _ceabw_1, _ceabw_2) } le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) : No: () le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) : No: () False <= le_nat(s(nn1), z) : No: () False <= le_nat(z, z) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) : No: () numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) : Yes: { _ww -> s(s(s(_viabw_0))) ; _xw -> s(z) ; _yw -> s(s(_eiabw_0)) ; t1 -> node(b, node(a, _ciabw_1, _ciabw_2), _kfabw_2) ; t2 -> node(b, leaf, _lfabw_2) } plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) : No: () ------------------------------------------- Step 15, which took 1.323132 s (model generation: 1.322078, model checking: 0.001054): Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le_nat(s(s(z)), s(s(s(z)))) <= True max(s(z), s(z), s(z)) <= True max(s(z), z, s(z)) <= True max(z, s(z), s(z)) <= True max(z, z, z) <= True not_empty(node(a, leaf, leaf)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), 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 height(node(a, leaf, leaf), s(s(z))) <= height(leaf, s(z)) height(node(a, leaf, node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(z))) <= height(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) /\ max(z, s(s(s(z))), s(z)) height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z)) le_nat(s(s(s(z))), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) le_nat(s(z), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= le_nat(s(s(z)), s(s(z))) le_nat(z, s(z)) <= le_nat(s(z), s(s(z))) False <= le_nat(s(z), s(z)) False <= le_nat(s(z), z) le_nat(s(z), s(s(z))) <= le_nat(z, s(z)) False <= le_nat(z, z) numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(z))) <= numnodes(leaf, s(z)) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z)) numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(z))) <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) le_nat(s(s(z)), s(z)) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) numnodes(node(a, node(b, node(a, leaf, leaf), leaf), node(b, leaf, leaf)), s(s(s(z)))) <= numnodes(node(b, leaf, leaf), s(z)) /\ numnodes(node(b, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(s(z))) False <= plus(s(z), s(z), s(z)) numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None height -> [ height : { height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0) /\ not_empty(x_0_2) height(node(x_0_0, x_0_1, x_0_2), z) <= True not_empty(leaf) <= True not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; le_nat -> [ le_nat : { le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0) le_nat(z, s(x_1_0)) <= True } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= True max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] ; not_empty -> [ not_empty : { not_empty(leaf) <= True not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; numnodes -> [ numnodes : { _r_1(leaf, s(x_1_0)) <= True _r_1(node(x_0_0, x_0_1, x_0_2), z) <= True _r_2(leaf, s(x_1_0)) <= True _r_2(leaf, z) <= True _r_2(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) } ] ; plus -> [ plus : { le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0) le_nat(z, s(x_1_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= le_nat(x_1_0, x_2_0) 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: height(leaf, z) <= True : No: () max(s(nn), z, s(nn)) <= True : No: () max(z, m, m) <= True : No: () not_empty(node(e, t1, t2)) <= True : No: () numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) : Yes: { _lw -> s(z) ; _mw -> z ; _nw -> s(_tjabw_0) ; t1 -> node(_ujabw_0, _ujabw_1, node(_tsabw_0, _tsabw_1, _tsabw_2)) ; t2 -> leaf } le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) : Yes: { _cx -> s(z) ; _dx -> s(z) ; t1 -> node(_bqabw_0, _bqabw_1, _bqabw_2) ; t2 -> leaf } le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) : No: () le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) : No: () False <= le_nat(s(nn1), z) : No: () False <= le_nat(z, z) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) : No: () numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) : Yes: { _ww -> z ; _xw -> s(z) ; _yw -> s(z) ; t1 -> leaf ; t2 -> node(_arabw_0, _arabw_1, leaf) } plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) : No: () ------------------------------------------- Step 16, which took 2.177477 s (model generation: 2.021679, model checking: 0.155798): Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le_nat(s(s(z)), s(s(s(z)))) <= True max(s(z), s(z), s(z)) <= True max(s(z), z, s(z)) <= True max(z, s(z), s(z)) <= True max(z, z, z) <= True not_empty(node(a, leaf, leaf)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), 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 height(node(a, leaf, leaf), s(s(z))) <= height(leaf, s(z)) height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) height(node(a, leaf, node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(z))) <= height(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) /\ max(z, s(s(s(z))), s(z)) height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z)) False <= height(node(a, node(a, leaf, leaf), leaf), s(z)) /\ not_empty(leaf) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) le_nat(s(s(s(z))), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) le_nat(s(z), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= le_nat(s(s(z)), s(s(z))) le_nat(z, s(z)) <= le_nat(s(z), s(s(z))) False <= le_nat(s(z), s(z)) False <= le_nat(s(z), z) le_nat(s(z), s(s(z))) <= le_nat(z, s(z)) False <= le_nat(z, z) numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(z))) <= numnodes(leaf, s(z)) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z)) numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(z))) <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) le_nat(s(s(z)), s(z)) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) numnodes(node(a, node(b, node(a, leaf, leaf), leaf), node(b, leaf, leaf)), s(s(s(z)))) <= numnodes(node(b, leaf, leaf), s(z)) /\ numnodes(node(b, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(s(z))) False <= plus(s(z), s(z), s(z)) numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None height -> [ height : { height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_1, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0) } ] ; le_nat -> [ le_nat : { le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0) le_nat(z, s(x_1_0)) <= True } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= True max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] ; not_empty -> [ not_empty : { not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; numnodes -> [ numnodes : { _r_1(leaf, s(x_1_0)) <= True _r_1(leaf, z) <= True _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_0, x_1_0) _r_1(node(x_0_0, x_0_1, x_0_2), z) <= True _r_2(a, s(x_1_0)) <= True _r_2(b, s(x_1_0)) <= True numnodes(leaf, s(x_1_0)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ numnodes(x_0_1, x_1_0) } ] ; plus -> [ plus : { le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0) le_nat(z, s(x_1_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= le_nat(x_1_0, x_2_0) 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: height(leaf, z) <= True : No: () max(s(nn), z, s(nn)) <= True : No: () max(z, m, m) <= True : No: () not_empty(node(e, t1, t2)) <= True : No: () numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) : Yes: { _lw -> z ; _mw -> s(z) ; _nw -> s(s(_wlbbw_0)) ; t1 -> leaf ; t2 -> node(_otabw_0, leaf, leaf) } le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) : Yes: { _cx -> s(s(s(s(s(z))))) ; _dx -> s(s(s(s(s(z))))) ; t1 -> node(_zuabw_0, node(a, _wobbw_1, _wobbw_2), node(_zobbw_0, node(_bkbbw_0, leaf, leaf), node(a, node(_wpbbw_0, _wpbbw_1, leaf), _xjbbw_2))) ; t2 -> node(b, _avabw_1, _avabw_2) } le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) : No: () le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) : No: () False <= le_nat(s(nn1), z) : No: () False <= le_nat(z, z) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) : No: () numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) : Yes: { _ww -> s(z) ; _xw -> s(z) ; _yw -> s(s(z)) ; t1 -> node(_zhbbw_0, leaf, node(b, node(_rrkcw_0, _rrkcw_1, _rrkcw_2), node(_rrkcw_0, _rrkcw_1, _rrkcw_2))) ; t2 -> node(_aibbw_0, leaf, node(b, node(_rrkcw_0, _rrkcw_1, _rrkcw_2), node(_rrkcw_0, _rrkcw_1, _rrkcw_2))) } plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) : No: () ------------------------------------------- Step 17, which took 23.461956 s (model generation: 23.453381, model checking: 0.008575): Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le_nat(s(s(z)), s(s(s(z)))) <= True max(s(z), s(z), s(z)) <= True max(s(z), z, s(z)) <= True max(z, s(z), s(z)) <= True max(z, z, z) <= True not_empty(node(a, leaf, leaf)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), 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 height(node(a, leaf, leaf), s(s(z))) <= height(leaf, s(z)) height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) height(node(a, leaf, node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(z))) <= height(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) /\ max(z, s(s(s(z))), s(z)) height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z)) False <= height(node(a, node(a, leaf, leaf), leaf), s(z)) /\ not_empty(leaf) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) le_nat(s(s(s(z))), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) le_nat(s(z), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) le_nat(s(s(s(s(s(z))))), s(s(s(s(s(z)))))) <= height(node(a, node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))), node(b, leaf, leaf)), s(s(s(s(s(z)))))) /\ not_empty(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)))) /\ not_empty(node(b, leaf, leaf)) /\ numnodes(node(a, node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))), node(b, leaf, leaf)), s(s(s(s(s(z)))))) False <= le_nat(s(s(z)), s(s(z))) le_nat(z, s(z)) <= le_nat(s(z), s(s(z))) False <= le_nat(s(z), s(z)) False <= le_nat(s(z), z) le_nat(s(z), s(s(z))) <= le_nat(z, s(z)) False <= le_nat(z, z) height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z))) numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(z))) <= numnodes(leaf, s(z)) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z)) numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(z))) <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(z)) numnodes(node(a, node(a, leaf, node(b, node(a, leaf, leaf), node(a, leaf, leaf))), node(a, leaf, node(b, node(a, leaf, leaf), node(a, leaf, leaf)))), s(s(s(z)))) <= numnodes(node(a, leaf, node(b, node(a, leaf, leaf), node(a, leaf, leaf))), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) le_nat(s(s(z)), s(z)) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) numnodes(node(a, node(b, node(a, leaf, leaf), leaf), node(b, leaf, leaf)), s(s(s(z)))) <= numnodes(node(b, leaf, leaf), s(z)) /\ numnodes(node(b, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(s(z))) False <= plus(s(z), s(z), s(z)) numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None height -> [ height : { _r_1(leaf, s(x_1_0)) <= True _r_1(leaf, z) <= True _r_2(leaf, s(x_1_0)) <= True _r_2(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) _r_2(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), z) <= True numnodes(leaf, s(x_1_0)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ height(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ height(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ height(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), z) <= True } ] ; le_nat -> [ le_nat : { le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0) le_nat(z, s(x_1_0)) <= True } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= True max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] ; not_empty -> [ not_empty : { not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; numnodes -> [ numnodes : { _r_1(leaf, s(x_1_0)) <= True _r_1(leaf, z) <= True _r_2(leaf, s(x_1_0)) <= True _r_2(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) _r_2(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), z) <= True numnodes(leaf, s(x_1_0)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ height(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ height(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ height(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), z) <= True } ] ; plus -> [ plus : { le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0) le_nat(z, s(x_1_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= le_nat(x_0_0, x_2_0) 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: height(leaf, z) <= True : No: () max(s(nn), z, s(nn)) <= True : No: () max(z, m, m) <= True : No: () not_empty(node(e, t1, t2)) <= True : No: () numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) : Yes: { _lw -> z ; _mw -> s(z) ; _nw -> s(s(_shncw_0)) ; t1 -> node(_vwkcw_0, leaf, leaf) ; t2 -> node(_wwkcw_0, node(_qdncw_0, _qdncw_1, _qdncw_2), _wwkcw_2) } le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) : Yes: { _cx -> z ; _dx -> z ; t1 -> node(_ezkcw_0, _ezkcw_1, _ezkcw_2) ; t2 -> node(_fzkcw_0, _fzkcw_1, _fzkcw_2) } le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) : No: () le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) : No: () False <= le_nat(s(nn1), z) : No: () False <= le_nat(z, z) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) : No: () numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) : Yes: { _ww -> z ; _xw -> s(_gklcw_0) ; _yw -> s(_hklcw_0) ; t1 -> leaf ; t2 -> leaf } plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) : Yes: { _rw -> s(z) ; mm -> z ; n -> s(s(z)) } ------------------------------------------- Step 18, which took 2.462219 s (model generation: 2.383737, model checking: 0.078482): Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le_nat(s(s(z)), s(s(s(z)))) <= True max(s(z), s(z), s(z)) <= True max(s(z), z, s(z)) <= True max(z, s(z), s(z)) <= True max(z, z, z) <= True not_empty(node(a, leaf, leaf)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), 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 height(node(a, leaf, leaf), s(s(z))) <= height(leaf, s(z)) height(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) <= height(node(a, leaf, leaf), z) /\ height(node(a, node(a, leaf, leaf), leaf), s(z)) /\ max(z, s(z), s(s(z))) height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) height(node(a, leaf, node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(z))) <= height(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) /\ max(z, s(s(s(z))), s(z)) height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z)) False <= height(node(a, node(a, leaf, leaf), leaf), s(z)) /\ not_empty(leaf) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) le_nat(s(s(s(z))), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) le_nat(s(z), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), z) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), z) le_nat(s(s(s(s(s(z))))), s(s(s(s(s(z)))))) <= height(node(a, node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))), node(b, leaf, leaf)), s(s(s(s(s(z)))))) /\ not_empty(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)))) /\ not_empty(node(b, leaf, leaf)) /\ numnodes(node(a, node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))), node(b, leaf, leaf)), s(s(s(s(s(z)))))) False <= le_nat(s(s(z)), s(s(z))) le_nat(z, s(z)) <= le_nat(s(z), s(s(z))) False <= le_nat(s(z), s(z)) False <= le_nat(s(z), z) le_nat(s(z), s(s(z))) <= le_nat(z, s(z)) False <= le_nat(z, z) height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z))) numnodes(node(a, leaf, leaf), s(s(z))) <= numnodes(leaf, s(z)) numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(z))) <= numnodes(leaf, s(z)) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z)) numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(z))) <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(z)) numnodes(node(a, node(a, leaf, node(b, node(a, leaf, leaf), node(a, leaf, leaf))), node(a, leaf, node(b, node(a, leaf, leaf), node(a, leaf, leaf)))), s(s(s(z)))) <= numnodes(node(a, leaf, node(b, node(a, leaf, leaf), node(a, leaf, leaf))), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) le_nat(s(s(z)), s(z)) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) numnodes(node(a, node(b, node(a, leaf, leaf), leaf), node(b, leaf, leaf)), s(s(s(z)))) <= numnodes(node(b, leaf, leaf), s(z)) /\ numnodes(node(b, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(s(z))) plus(s(s(z)), s(z), s(s(z))) <= plus(s(s(z)), z, s(z)) False <= plus(s(z), s(z), s(z)) numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None height -> [ height : { _r_1(leaf, s(x_1_0)) <= True _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= not_empty(x_0_2) /\ numnodes(x_0_1, x_1_0) _r_1(node(x_0_0, x_0_1, x_0_2), z) <= not_empty(x_0_2) _r_2(leaf, s(x_1_0)) <= True _r_2(leaf, z) <= True _r_2(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ height(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ _r_2(x_0_1, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), z) <= True not_empty(leaf) <= True not_empty(node(x_0_0, x_0_1, x_0_2)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ height(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ numnodes(x_0_1, x_1_0) } ] ; le_nat -> [ le_nat : { le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0) le_nat(z, s(x_1_0)) <= True } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= True max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] ; not_empty -> [ not_empty : { not_empty(leaf) <= True not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; numnodes -> [ numnodes : { _r_1(leaf, s(x_1_0)) <= True _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= not_empty(x_0_2) /\ numnodes(x_0_1, x_1_0) _r_1(node(x_0_0, x_0_1, x_0_2), z) <= not_empty(x_0_2) _r_2(leaf, s(x_1_0)) <= True _r_2(leaf, z) <= True _r_2(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ height(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ _r_2(x_0_1, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), z) <= True not_empty(leaf) <= True not_empty(node(x_0_0, x_0_1, x_0_2)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ height(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ numnodes(x_0_1, x_1_0) } ] ; plus -> [ plus : { le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0) le_nat(z, s(x_1_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= le_nat(x_1_0, x_2_0) 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: height(leaf, z) <= True : No: () max(s(nn), z, s(nn)) <= True : No: () max(z, m, m) <= True : No: () not_empty(node(e, t1, t2)) <= True : No: () numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) : Yes: { _lw -> z ; _mw -> s(s(_powcw_0)) ; _nw -> s(s(_yqxcw_0)) ; t1 -> node(_psscw_0, leaf, _psscw_2) ; t2 -> node(_qsscw_0, leaf, leaf) } le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) : Yes: { _cx -> s(s(_notcw_0)) ; _dx -> s(z) ; t1 -> leaf ; t2 -> leaf } le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) : No: () le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) : No: () False <= le_nat(s(nn1), z) : No: () False <= le_nat(z, z) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) : No: () numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) : Yes: { _ww -> s(z) ; _xw -> z ; _yw -> s(s(_skycw_0)) ; t1 -> node(_rmtcw_0, leaf, leaf) ; t2 -> leaf } plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) : No: () ------------------------------------------- Step 19, which took 9.577970 s (model generation: 9.265070, model checking: 0.312900): Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le_nat(s(s(z)), s(s(s(z)))) <= True max(s(z), s(z), s(z)) <= True max(s(z), z, s(z)) <= True max(z, s(z), s(z)) <= True max(z, z, z) <= True not_empty(node(a, leaf, leaf)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), 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 height(node(a, leaf, leaf), s(s(z))) <= height(leaf, s(z)) height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= height(node(a, leaf, leaf), s(s(z))) /\ height(node(a, leaf, leaf), z) /\ max(z, s(s(z)), s(s(z))) le_nat(s(s(z)), s(z)) <= height(node(a, leaf, leaf), s(s(z))) /\ not_empty(leaf) height(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) <= height(node(a, leaf, leaf), z) /\ height(node(a, node(a, leaf, leaf), leaf), s(z)) /\ max(z, s(z), s(s(z))) height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) height(node(a, leaf, node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(z))) <= height(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) /\ max(z, s(s(s(z))), s(z)) height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z)) False <= height(node(a, node(a, leaf, leaf), leaf), s(z)) /\ not_empty(leaf) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) le_nat(s(s(s(z))), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) le_nat(s(z), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), z) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), z) le_nat(s(s(s(s(s(z))))), s(s(s(s(s(z)))))) <= height(node(a, node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))), node(b, leaf, leaf)), s(s(s(s(s(z)))))) /\ not_empty(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)))) /\ not_empty(node(b, leaf, leaf)) /\ numnodes(node(a, node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))), node(b, leaf, leaf)), s(s(s(s(s(z)))))) False <= le_nat(s(s(z)), s(s(z))) le_nat(z, s(z)) <= le_nat(s(z), s(s(z))) False <= le_nat(s(z), s(z)) False <= le_nat(s(z), z) le_nat(s(z), s(s(z))) <= le_nat(z, s(z)) False <= le_nat(z, z) height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z))) numnodes(node(a, leaf, leaf), s(s(z))) <= numnodes(leaf, s(z)) numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(z))) <= numnodes(leaf, s(z)) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z)) numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(z))) <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(z)) numnodes(node(a, node(a, leaf, node(b, node(a, leaf, leaf), node(a, leaf, leaf))), node(a, leaf, node(b, node(a, leaf, leaf), node(a, leaf, leaf)))), s(s(s(z)))) <= numnodes(node(a, leaf, node(b, node(a, leaf, leaf), node(a, leaf, leaf))), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) le_nat(s(s(z)), s(z)) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) numnodes(node(a, node(b, node(a, leaf, leaf), leaf), node(b, leaf, leaf)), s(s(s(z)))) <= numnodes(node(b, leaf, leaf), s(z)) /\ numnodes(node(b, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(s(z))) plus(s(s(z)), s(z), s(s(z))) <= plus(s(s(z)), z, s(z)) False <= plus(s(z), s(z), s(z)) numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= plus(s(z), z, s(s(z))) numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None height -> [ height : { _r_1(leaf, s(x_1_0)) <= True _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) _r_2(leaf, s(x_1_0)) <= True _r_2(leaf, z) <= True _r_2(node(x_0_0, x_0_1, x_0_2), z) <= True height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_2, x_1_0) numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ height(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ height(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ height(x_0_1, x_1_0) } ] ; le_nat -> [ le_nat : { le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0) le_nat(z, s(x_1_0)) <= True } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= True max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] ; not_empty -> [ not_empty : { not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; numnodes -> [ numnodes : { _r_1(leaf, s(x_1_0)) <= True _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) _r_2(leaf, s(x_1_0)) <= True _r_2(leaf, z) <= True _r_2(node(x_0_0, x_0_1, x_0_2), z) <= True height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_2, x_1_0) numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ height(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ height(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ height(x_0_1, x_1_0) } ] ; plus -> [ plus : { le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0) le_nat(z, s(x_1_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= le_nat(x_1_0, x_2_0) 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: height(leaf, z) <= True : No: () max(s(nn), z, s(nn)) <= True : No: () max(z, m, m) <= True : No: () not_empty(node(e, t1, t2)) <= True : No: () numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) : Yes: { _lw -> s(z) ; _mw -> s(z) ; _nw -> s(z) ; t1 -> node(_amycw_0, node(_ucadw_0, _ucadw_1, _ucadw_2), _amycw_2) ; t2 -> node(_bmycw_0, node(_geadw_0, _geadw_1, _geadw_2), node(_scadw_0, _scadw_1, _scadw_2)) } le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) : Yes: { _cx -> s(s(s(z))) ; _dx -> s(s(s(z))) ; t1 -> node(_zoycw_0, _zoycw_1, leaf) ; t2 -> node(_apycw_0, leaf, node(_xqzcw_0, _xqzcw_1, node(_vdadw_0, _vdadw_1, _vdadw_2))) } le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) : No: () le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) : No: () False <= le_nat(s(nn1), z) : No: () False <= le_nat(z, z) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) : No: () plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) : No: () ------------------------------------------- Step 20, which took 7.249659 s (model generation: 7.246595, model checking: 0.003064): Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le_nat(s(s(z)), s(s(s(z)))) <= True max(s(z), s(z), s(z)) <= True max(s(z), z, s(z)) <= True max(z, s(z), s(z)) <= True max(z, z, z) <= True not_empty(node(a, leaf, leaf)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), 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 height(node(a, leaf, leaf), s(s(z))) <= height(leaf, s(z)) height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= height(node(a, leaf, leaf), s(s(z))) /\ height(node(a, leaf, leaf), z) /\ max(z, s(s(z)), s(s(z))) le_nat(s(s(z)), s(z)) <= height(node(a, leaf, leaf), s(s(z))) /\ not_empty(leaf) height(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) <= height(node(a, leaf, leaf), z) /\ height(node(a, node(a, leaf, leaf), leaf), s(z)) /\ max(z, s(z), s(s(z))) height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) height(node(a, leaf, node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(z))) <= height(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) /\ max(z, s(s(s(z))), s(z)) height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z)) height(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(z)) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), leaf), s(z)) /\ not_empty(leaf) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) le_nat(s(s(s(z))), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) le_nat(s(z), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), z) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), z) le_nat(s(s(s(z))), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(s(z)))) /\ not_empty(node(a, leaf, node(a, leaf, node(a, leaf, leaf)))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(s(z)))) le_nat(s(s(s(s(s(z))))), s(s(s(s(s(z)))))) <= height(node(a, node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))), node(b, leaf, leaf)), s(s(s(s(s(z)))))) /\ not_empty(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)))) /\ not_empty(node(b, leaf, leaf)) /\ numnodes(node(a, node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))), node(b, leaf, leaf)), s(s(s(s(s(z)))))) False <= le_nat(s(s(z)), s(s(z))) le_nat(z, s(z)) <= le_nat(s(z), s(s(z))) False <= le_nat(s(z), s(z)) False <= le_nat(s(z), z) le_nat(s(z), s(s(z))) <= le_nat(z, s(z)) False <= le_nat(z, z) height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z))) numnodes(node(a, leaf, leaf), s(s(z))) <= numnodes(leaf, s(z)) numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(z))) <= numnodes(leaf, s(z)) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z)) numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(z))) <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(z)) numnodes(node(a, node(a, leaf, node(b, node(a, leaf, leaf), node(a, leaf, leaf))), node(a, leaf, node(b, node(a, leaf, leaf), node(a, leaf, leaf)))), s(s(s(z)))) <= numnodes(node(a, leaf, node(b, node(a, leaf, leaf), node(a, leaf, leaf))), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) le_nat(s(s(z)), s(z)) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) numnodes(node(a, node(b, node(a, leaf, leaf), leaf), node(b, leaf, leaf)), s(s(s(z)))) <= numnodes(node(b, leaf, leaf), s(z)) /\ numnodes(node(b, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(s(z))) plus(s(s(z)), s(z), s(s(z))) <= plus(s(s(z)), z, s(z)) False <= plus(s(z), s(z), s(z)) numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= plus(s(z), z, s(s(z))) numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None height -> [ height : { _r_2(leaf) <= True height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1) /\ not_empty(x_0_2) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_1, x_1_0) height(node(x_0_0, x_0_1, x_0_2), z) <= not_empty(x_0_1) not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; le_nat -> [ le_nat : { le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0) le_nat(z, s(x_1_0)) <= True } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= True max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] ; not_empty -> [ not_empty : { not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; numnodes -> [ numnodes : { _r_1(leaf, s(x_1_0)) <= True _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_1, x_1_0) /\ not_empty(x_0_1) _r_2(leaf) <= True height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1) /\ not_empty(x_0_2) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_1, x_1_0) height(node(x_0_0, x_0_1, x_0_2), z) <= not_empty(x_0_1) not_empty(node(x_0_0, x_0_1, x_0_2)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2) } ] ; plus -> [ plus : { le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0) le_nat(z, s(x_1_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= le_nat(x_1_0, x_2_0) 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: height(leaf, z) <= True : No: () max(s(nn), z, s(nn)) <= True : No: () max(z, m, m) <= True : No: () not_empty(node(e, t1, t2)) <= True : No: () numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) : Yes: { _lw -> s(z) ; _mw -> z ; _nw -> s(s(_bcbdw_0)) ; t1 -> node(_jqadw_0, leaf, leaf) ; t2 -> leaf } le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) : Yes: { _cx -> s(s(s(s(z)))) ; _dx -> s(s(s(s(z)))) ; t1 -> node(_rtadw_0, node(_dcbdw_0, leaf, node(_yyadw_0, _yyadw_1, _yyadw_2)), _rtadw_2) ; t2 -> node(_stadw_0, _stadw_1, _stadw_2) } le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) : No: () le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) : No: () False <= le_nat(s(nn1), z) : No: () False <= le_nat(z, z) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) : No: () numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) : Yes: { _ww -> s(_ixadw_0) ; _xw -> s(z) ; _yw -> s(s(z)) ; t1 -> node(_lxadw_0, node(_kgbdw_0, node(_xcbdw_0, leaf, _xcbdw_2), leaf), leaf) ; t2 -> node(_mxadw_0, _mxadw_1, leaf) } plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) : No: () ------------------------------------------- Step 21, which took 5.849232 s (model generation: 5.260897, model checking: 0.588335): Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le_nat(s(s(z)), s(s(s(z)))) <= True max(s(z), s(z), s(z)) <= True max(s(z), z, s(z)) <= True max(z, s(z), s(z)) <= True max(z, z, z) <= True not_empty(node(a, leaf, leaf)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), 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 height(node(a, leaf, leaf), s(s(z))) <= height(leaf, s(z)) height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= height(node(a, leaf, leaf), s(s(z))) /\ height(node(a, leaf, leaf), z) /\ max(z, s(s(z)), s(s(z))) le_nat(s(s(z)), s(z)) <= height(node(a, leaf, leaf), s(s(z))) /\ not_empty(leaf) height(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) <= height(node(a, leaf, leaf), z) /\ height(node(a, node(a, leaf, leaf), leaf), s(z)) /\ max(z, s(z), s(s(z))) height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) height(node(a, leaf, node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(z))) <= height(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) /\ max(z, s(s(s(z))), s(z)) height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z)) height(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(z)) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), leaf), s(z)) /\ not_empty(leaf) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) le_nat(s(s(s(z))), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) le_nat(s(z), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), z) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), z) le_nat(s(s(s(z))), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(s(z)))) /\ not_empty(node(a, leaf, node(a, leaf, node(a, leaf, leaf)))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(s(z)))) le_nat(s(s(s(s(s(z))))), s(s(s(s(s(z)))))) <= height(node(a, node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))), node(b, leaf, leaf)), s(s(s(s(s(z)))))) /\ not_empty(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)))) /\ not_empty(node(b, leaf, leaf)) /\ numnodes(node(a, node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))), node(b, leaf, leaf)), s(s(s(s(s(z)))))) le_nat(s(s(s(s(z)))), s(s(s(s(z))))) <= height(node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), node(a, leaf, leaf)), s(s(s(s(z))))) /\ not_empty(node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) /\ numnodes(node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), node(a, leaf, leaf)), s(s(s(s(z))))) False <= le_nat(s(s(z)), s(s(z))) le_nat(z, s(z)) <= le_nat(s(z), s(s(z))) False <= le_nat(s(z), s(z)) False <= le_nat(s(z), z) le_nat(s(z), s(s(z))) <= le_nat(z, s(z)) False <= le_nat(z, z) height(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z))) numnodes(node(a, leaf, leaf), s(s(z))) <= numnodes(leaf, s(z)) numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(z))) <= numnodes(leaf, s(z)) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z)) numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(z))) <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(z)) numnodes(node(a, node(a, leaf, node(b, node(a, leaf, leaf), node(a, leaf, leaf))), node(a, leaf, node(b, node(a, leaf, leaf), node(a, leaf, leaf)))), s(s(s(z)))) <= numnodes(node(a, leaf, node(b, node(a, leaf, leaf), node(a, leaf, leaf))), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) le_nat(s(s(z)), s(z)) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(s(z)))) <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(z)) numnodes(node(a, node(b, node(a, leaf, leaf), leaf), node(b, leaf, leaf)), s(s(s(z)))) <= numnodes(node(b, leaf, leaf), s(z)) /\ numnodes(node(b, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(s(z))) plus(s(s(z)), s(z), s(s(z))) <= plus(s(s(z)), z, s(z)) False <= plus(s(z), s(z), s(z)) numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= plus(s(z), z, s(s(z))) numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None height -> [ height : { _r_1(leaf, s(x_1_0)) <= True _r_1(leaf, z) <= True _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ _r_2(x_0_1, x_1_0) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ _r_2(x_0_2, x_1_0) /\ not_empty(x_0_1) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ not_empty(x_0_1) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ not_empty(x_0_1) /\ numnodes(x_0_2, x_1_0) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= not_empty(x_0_1) _r_2(leaf, s(x_1_0)) <= True _r_2(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_1, x_1_0) /\ not_empty(x_0_2) _r_2(node(x_0_0, x_0_1, x_0_2), z) <= True height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_2(x_0_2, x_1_0) /\ not_empty(x_0_1) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ height(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ not_empty(x_0_2) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ height(x_0_1, x_1_0) /\ not_empty(x_0_1) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ not_empty(x_0_2) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0) /\ not_empty(x_0_2) not_empty(node(x_0_0, x_0_1, x_0_2)) <= True numnodes(leaf, s(x_1_0)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_1(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_1(x_0_2, x_1_0) /\ not_empty(x_0_1) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_1(x_0_2, x_1_0) /\ not_empty(x_0_2) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_2(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ not_empty(x_0_1) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ not_empty(x_0_1) /\ numnodes(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ not_empty(x_0_2) /\ numnodes(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ numnodes(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0) } ] ; le_nat -> [ le_nat : { le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0) le_nat(z, s(x_1_0)) <= True } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= True max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] ; not_empty -> [ not_empty : { not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; numnodes -> [ numnodes : { _r_1(leaf, s(x_1_0)) <= True _r_1(leaf, z) <= True _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ _r_2(x_0_1, x_1_0) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ _r_2(x_0_2, x_1_0) /\ not_empty(x_0_1) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ not_empty(x_0_1) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ not_empty(x_0_1) /\ numnodes(x_0_2, x_1_0) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= not_empty(x_0_1) _r_2(leaf, s(x_1_0)) <= True _r_2(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_1, x_1_0) /\ not_empty(x_0_2) _r_2(node(x_0_0, x_0_1, x_0_2), z) <= True height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_2(x_0_2, x_1_0) /\ not_empty(x_0_1) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ height(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ not_empty(x_0_2) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ height(x_0_1, x_1_0) /\ not_empty(x_0_1) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ not_empty(x_0_2) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0) /\ not_empty(x_0_2) not_empty(node(x_0_0, x_0_1, x_0_2)) <= True numnodes(leaf, s(x_1_0)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_1(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_1(x_0_2, x_1_0) /\ not_empty(x_0_1) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_1(x_0_2, x_1_0) /\ not_empty(x_0_2) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_2(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ not_empty(x_0_1) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ not_empty(x_0_1) /\ numnodes(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ not_empty(x_0_2) /\ numnodes(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ numnodes(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0) } ] ; plus -> [ plus : { le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0) le_nat(z, s(x_1_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= le_nat(x_1_0, x_2_0) 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: height(leaf, z) <= True : No: () max(s(nn), z, s(nn)) <= True : No: () max(z, m, m) <= True : No: () not_empty(node(e, t1, t2)) <= True : No: () numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) : Yes: { _cx -> s(s(s(z))) ; _dx -> s(s(z)) ; t1 -> node(_nrrdw_0, _nrrdw_1, _nrrdw_2) ; t2 -> node(_orrdw_0, node(_wbrfw_0, _wbrfw_1, _wbrfw_2), node(_pcrfw_0, node(_hyqfw_0, _hyqfw_1, _hyqfw_2), node(_fbrfw_0, _fbrfw_1, _fbrfw_2))) } le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) : No: () le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) : No: () False <= le_nat(s(nn1), z) : No: () False <= le_nat(z, z) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) : No: () plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) : No: () Total time: 59.697220 Learner time: 52.442898 Teacher time: 1.153393 Reasons for stopping: Maybe: timeout during learnerLast solver state: Clauses: { height(leaf, z) <= True -> 0 max(s(nn), z, s(nn)) <= True -> 0 max(z, m, m) <= True -> 0 not_empty(node(e, t1, t2)) <= True -> 0 numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 0 height(node(e, t1, t2), s(_nw)) <= height(t1, _lw) /\ height(t2, _mw) /\ max(_lw, _mw, _nw) -> 0 le_nat(_cx, _dx) <= height(node(e, t1, t2), _cx) /\ not_empty(t1) /\ not_empty(t2) /\ numnodes(node(e, t1, t2), _dx) -> 0 le_nat(s(nn1), s(nn2)) <= le_nat(nn1, nn2) -> 0 le_nat(nn1, nn2) <= le_nat(s(nn1), s(nn2)) -> 0 False <= le_nat(s(nn1), z) -> 0 False <= le_nat(z, z) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 max(s(nn), s(mm), s(_gw)) <= max(nn, mm, _gw) -> 0 numnodes(node(e, t1, t2), s(_yw)) <= numnodes(t1, _ww) /\ numnodes(t2, _xw) /\ plus(_ww, _xw, _yw) -> 0 plus(n, s(mm), s(_rw)) <= plus(n, mm, _rw) -> 0 } Accumulated learning constraints: { height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le_nat(s(s(z)), s(s(s(z)))) <= True max(s(z), s(z), s(z)) <= True max(s(z), z, s(z)) <= True max(z, s(z), s(z)) <= True max(z, z, z) <= True not_empty(node(a, leaf, leaf)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), 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 height(node(a, leaf, leaf), s(s(z))) <= height(leaf, s(z)) height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= height(node(a, leaf, leaf), s(s(z))) /\ height(node(a, leaf, leaf), z) /\ max(z, s(s(z)), s(s(z))) le_nat(s(s(z)), s(z)) <= height(node(a, leaf, leaf), s(s(z))) /\ not_empty(leaf) height(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) <= height(node(a, leaf, leaf), z) /\ height(node(a, node(a, leaf, leaf), leaf), s(z)) /\ max(z, s(z), s(s(z))) height(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) height(node(a, leaf, node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(z))) <= height(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) /\ max(z, s(s(s(z))), s(z)) height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z)) height(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(z))) <= height(node(a, node(a, leaf, leaf), leaf), s(z)) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), leaf), s(z)) /\ not_empty(leaf) /\ numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) le_nat(s(s(s(z))), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) le_nat(s(z), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), z) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), z) le_nat(s(s(s(z))), s(s(s(z)))) <= height(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(s(z)))) /\ not_empty(node(a, leaf, node(a, leaf, node(a, leaf, leaf)))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, node(a, leaf, leaf)))), s(s(s(z)))) le_nat(s(s(s(z))), s(s(z))) <= height(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))), s(s(s(z)))) /\ not_empty(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))) /\ numnodes(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))), s(s(z))) le_nat(s(s(s(s(s(z))))), s(s(s(s(s(z)))))) <= height(node(a, node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))), node(b, leaf, leaf)), s(s(s(s(s(z)))))) /\ not_empty(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)))) /\ not_empty(node(b, leaf, leaf)) /\ numnodes(node(a, node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))), node(b, leaf, leaf)), s(s(s(s(s(z)))))) le_nat(s(s(s(s(z)))), s(s(s(s(z))))) <= height(node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), node(a, leaf, leaf)), s(s(s(s(z))))) /\ not_empty(node(a, node(a, leaf, node(a, leaf, leaf)), leaf)) /\ numnodes(node(a, node(a, node(a, leaf, node(a, leaf, leaf)), leaf), node(a, leaf, leaf)), s(s(s(s(z))))) False <= le_nat(s(s(z)), s(s(z))) le_nat(z, s(z)) <= le_nat(s(z), s(s(z))) False <= le_nat(s(z), s(z)) False <= le_nat(s(z), z) le_nat(s(z), s(s(z))) <= le_nat(z, s(z)) False <= le_nat(z, z) height(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z))) numnodes(node(a, leaf, leaf), s(s(z))) <= numnodes(leaf, s(z)) numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(z))) <= numnodes(leaf, s(z)) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(z)) numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(z))) <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(z)) numnodes(node(a, node(a, leaf, node(b, node(a, leaf, leaf), node(a, leaf, leaf))), node(a, leaf, node(b, node(a, leaf, leaf), node(a, leaf, leaf)))), s(s(s(z)))) <= numnodes(node(a, leaf, node(b, node(a, leaf, leaf), node(a, leaf, leaf))), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) le_nat(s(s(z)), s(z)) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(s(z)))) <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(z)) numnodes(node(a, node(b, node(a, leaf, leaf), leaf), node(b, leaf, leaf)), s(s(s(z)))) <= numnodes(node(b, leaf, leaf), s(z)) /\ numnodes(node(b, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ plus(s(s(s(z))), s(z), s(s(z))) plus(s(s(z)), s(z), s(s(z))) <= plus(s(s(z)), z, s(z)) False <= plus(s(z), s(z), s(z)) numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= plus(s(z), z, s(s(z))) numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None height -> [ height : { _r_1(leaf, s(x_1_0)) <= True _r_1(leaf, z) <= True _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ _r_2(x_0_1, x_1_0) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ _r_2(x_0_2, x_1_0) /\ not_empty(x_0_1) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ not_empty(x_0_1) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ not_empty(x_0_1) /\ numnodes(x_0_2, x_1_0) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= not_empty(x_0_1) _r_2(leaf, s(x_1_0)) <= True _r_2(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_1, x_1_0) /\ not_empty(x_0_2) _r_2(node(x_0_0, x_0_1, x_0_2), z) <= True height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_2(x_0_2, x_1_0) /\ not_empty(x_0_1) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ height(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ not_empty(x_0_2) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ height(x_0_1, x_1_0) /\ not_empty(x_0_1) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ not_empty(x_0_2) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0) /\ not_empty(x_0_2) not_empty(node(x_0_0, x_0_1, x_0_2)) <= True numnodes(leaf, s(x_1_0)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_1(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_1(x_0_2, x_1_0) /\ not_empty(x_0_1) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_1(x_0_2, x_1_0) /\ not_empty(x_0_2) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_2(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ not_empty(x_0_1) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ not_empty(x_0_1) /\ numnodes(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ not_empty(x_0_2) /\ numnodes(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ numnodes(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0) } ] ; le_nat -> [ le_nat : { le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0) le_nat(z, s(x_1_0)) <= True } ] ; leq_nat -> [ leq_nat : { } ] ; max -> [ max : { max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= True max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] ; not_empty -> [ not_empty : { not_empty(node(x_0_0, x_0_1, x_0_2)) <= True } ] ; numnodes -> [ numnodes : { _r_1(leaf, s(x_1_0)) <= True _r_1(leaf, z) <= True _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ _r_2(x_0_1, x_1_0) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ _r_2(x_0_2, x_1_0) /\ not_empty(x_0_1) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ not_empty(x_0_1) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ not_empty(x_0_1) /\ numnodes(x_0_2, x_1_0) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= not_empty(x_0_1) _r_2(leaf, s(x_1_0)) <= True _r_2(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_1, x_1_0) /\ not_empty(x_0_2) _r_2(node(x_0_0, x_0_1, x_0_2), z) <= True height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_2(x_0_2, x_1_0) /\ not_empty(x_0_1) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ height(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ not_empty(x_0_2) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ height(x_0_1, x_1_0) /\ not_empty(x_0_1) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ not_empty(x_0_2) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0) /\ not_empty(x_0_2) not_empty(node(x_0_0, x_0_1, x_0_2)) <= True numnodes(leaf, s(x_1_0)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_1(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_1(x_0_2, x_1_0) /\ not_empty(x_0_1) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_1(x_0_2, x_1_0) /\ not_empty(x_0_2) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_2(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ not_empty(x_0_1) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ not_empty(x_0_1) /\ numnodes(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ not_empty(x_0_2) /\ numnodes(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ numnodes(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0) } ] ; plus -> [ plus : { le_nat(s(x_0_0), s(x_1_0)) <= le_nat(x_0_0, x_1_0) le_nat(z, s(x_1_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= le_nat(x_1_0, x_2_0) 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} _|