Solving ../../benchmarks/smtlib/true/tree_flip_preserves_depth.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: { (flip, F: { flip(leaf, leaf) <= True flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) } eq_etree(_zu, _av) <= flip(_yu, _av) /\ flip(_yu, _zu) ) (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) } ) (max_ite, F: { leq_nat(x, y) \/ max_ite(x, y, x) <= True max_ite(x, y, y) <= leq_nat(x, y) } eq_nat(_dv, _ev) <= max_ite(_bv, _cv, _dv) /\ max_ite(_bv, _cv, _ev) ) (height, F: { height(leaf, z) <= True height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) } eq_nat(_jv, _kv) <= height(_iv, _jv) /\ height(_iv, _kv) ) } properties: { eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) } over-approximation: {flip, height, max_ite} under-approximation: {} Clause system for inference is: { flip(leaf, leaf) <= True -> 0 height(leaf, z) <= True -> 0 leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(z, n2) <= True -> 0 eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) -> 0 flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) -> 0 height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 } Solving took 60.066909 seconds. Maybe: timeout during teacher: { height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> out of time }Last solver state: Clauses: { flip(leaf, leaf) <= True -> 0 height(leaf, z) <= True -> 0 leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(z, n2) <= True -> 0 eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) -> 0 flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) -> 0 height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 } Accumulated learning constraints: { flip(leaf, leaf) <= True flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) <= True flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) <= True height(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True height(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(s(z)))) <= True leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(s(z))) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(s(z)), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(s(z)), s(s(z))) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True False <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(z))) False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), node(a, node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) /\ height(node(a, node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)), s(s(z))) False <= flip(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, leaf, leaf))) /\ height(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) False <= flip(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))) /\ height(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) /\ height(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) False <= height(node(a, leaf, leaf), s(s(z))) False <= height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) False <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) False <= height(node(a, node(a, leaf, leaf), leaf), s(z)) False <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) height(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) <= max_ite(s(s(z)), s(z), s(z)) height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max_ite(s(z), s(z), s(s(z))) False <= max_ite(s(z), z, s(s(z))) height(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= max_ite(z, s(s(z)), s(s(s(z)))) False <= max_ite(z, s(z), s(s(z))) } Current best model: |_ name: None flip -> [ flip : { flip(leaf, leaf) <= True flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1) } ] ; height -> [ height : { _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_2(x_0_1, 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)) <= _r_2(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_2, x_1_0) /\ height(x_0_1, x_1_0) } ] ; leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(z, z) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= max_ite(x_0_0, x_1_0, x_2_0) max_ite(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.006734 s (model generation: 0.006629, model checking: 0.000105): Clauses: { flip(leaf, leaf) <= True -> 0 height(leaf, z) <= True -> 0 leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(z, n2) <= True -> 0 eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) -> 0 flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) -> 0 height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 } Accumulated learning constraints: { } Current best model: |_ name: None flip -> [ flip : { } ] ; height -> [ height : { } ] ; leq_nat -> [ leq_nat : { } ] ; max_ite -> [ max_ite : { } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: flip(leaf, leaf) <= True : Yes: { } height(leaf, z) <= True : Yes: { } leq_nat(x, y) \/ max_ite(x, y, x) <= True : Yes: { x -> z ; y -> z } leq_nat(z, n2) <= True : Yes: { n2 -> z } eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) : No: () flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) : No: () height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () ------------------------------------------- Step 1, which took 0.006530 s (model generation: 0.006431, model checking: 0.000099): Clauses: { flip(leaf, leaf) <= True -> 0 height(leaf, z) <= True -> 0 leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(z, n2) <= True -> 0 eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) -> 0 flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) -> 0 height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 } Accumulated learning constraints: { flip(leaf, leaf) <= True height(leaf, z) <= True leq_nat(z, z) <= True } Current best model: |_ name: None flip -> [ flip : { flip(leaf, leaf) <= True } ] ; height -> [ height : { height(leaf, z) <= True } ] ; leq_nat -> [ leq_nat : { leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: flip(leaf, leaf) <= True : No: () height(leaf, z) <= True : No: () leq_nat(x, y) \/ max_ite(x, y, x) <= True : Yes: { x -> z ; y -> s(_fmyve_0) } leq_nat(z, n2) <= True : Yes: { n2 -> s(_gmyve_0) } eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) : No: () flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) : Yes: { _wu -> leaf ; _xu -> leaf ; t1 -> leaf ; t2 -> leaf } height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : Yes: { nn1 -> z ; nn2 -> z } max_ite(x, y, y) <= leq_nat(x, y) : Yes: { x -> z ; y -> z } leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () ------------------------------------------- Step 2, which took 0.008388 s (model generation: 0.008249, model checking: 0.000139): Clauses: { flip(leaf, leaf) <= True -> 0 height(leaf, z) <= True -> 0 leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(z, n2) <= True -> 0 eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) -> 0 flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) -> 0 height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 } Accumulated learning constraints: { flip(leaf, leaf) <= True flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True height(leaf, z) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(z, z, z) <= True } Current best model: |_ name: None flip -> [ flip : { flip(leaf, leaf) <= True flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= True } ] ; height -> [ height : { height(leaf, z) <= True } ] ; leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= True leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { max_ite(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: flip(leaf, leaf) <= True : No: () height(leaf, z) <= True : No: () leq_nat(x, y) \/ max_ite(x, y, x) <= True : Yes: { x -> s(_pmyve_0) ; y -> z } leq_nat(z, n2) <= True : No: () eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) : No: () flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) : No: () height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) : Yes: { _fv -> z ; _gv -> z ; _hv -> z ; t1 -> leaf ; t2 -> leaf } leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : Yes: { x -> z ; y -> s(_zmyve_0) } leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : Yes: { nn1 -> s(_anyve_0) ; nn2 -> z } False <= leq_nat(s(nn1), z) : No: () ------------------------------------------- Step 3, which took 0.009944 s (model generation: 0.009795, model checking: 0.000149): Clauses: { flip(leaf, leaf) <= True -> 0 height(leaf, z) <= True -> 0 leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(z, n2) <= True -> 0 eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) -> 0 flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) -> 0 height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 } Accumulated learning constraints: { flip(leaf, leaf) <= True flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True leq_nat(s(z), s(z)) <= True leq_nat(s(z), z) \/ max_ite(s(z), z, s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True leq_nat(s(z), z) <= leq_nat(s(s(z)), s(z)) } Current best model: |_ name: None flip -> [ flip : { flip(leaf, leaf) <= True flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= True } ] ; height -> [ height : { height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True } ] ; leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= True leq_nat(s(x_0_0), z) <= True leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= True max_ite(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: flip(leaf, leaf) <= True : No: () height(leaf, z) <= True : No: () leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(z, n2) <= True : No: () eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) : Yes: { _lv -> s(z) ; _mv -> node(_dnyve_0, _dnyve_1, _dnyve_2) ; _nv -> s(s(_pnyve_0)) ; t -> node(_fnyve_0, _fnyve_1, _fnyve_2) } flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) : No: () height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : Yes: { x -> s(_inyve_0) ; y -> z } leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : Yes: { } ------------------------------------------- Step 4, which took 0.010481 s (model generation: 0.010194, model checking: 0.000287): Clauses: { flip(leaf, leaf) <= True -> 0 height(leaf, z) <= True -> 0 leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(z, n2) <= True -> 0 eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) -> 0 flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) -> 0 height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 } Accumulated learning constraints: { flip(leaf, leaf) <= True flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True False <= height(node(a, leaf, leaf), s(s(z))) False <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) } Current best model: |_ name: None flip -> [ flip : { flip(leaf, leaf) <= True flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= True } ] ; 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) } ] ; leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= True max_ite(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: flip(leaf, leaf) <= True : No: () height(leaf, z) <= True : No: () leq_nat(x, y) \/ max_ite(x, y, x) <= True : Yes: { x -> s(s(_zoyve_0)) ; y -> s(z) } leq_nat(z, n2) <= True : No: () eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) : Yes: { _lv -> s(s(z)) ; _mv -> node(_tnyve_0, _tnyve_1, leaf) ; _nv -> s(z) ; t -> node(_vnyve_0, _vnyve_1, node(_fpyve_0, _fpyve_1, leaf)) } flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) : No: () height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) : Yes: { _fv -> s(z) ; _gv -> z ; _hv -> s(_ioyve_0) ; t1 -> node(_joyve_0, _joyve_1, leaf) ; t2 -> leaf } leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : Yes: { x -> s(z) ; y -> s(z) } leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () ------------------------------------------- Step 5, which took 0.011987 s (model generation: 0.011761, model checking: 0.000226): Clauses: { flip(leaf, leaf) <= True -> 0 height(leaf, z) <= True -> 0 leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(z, n2) <= True -> 0 eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) -> 0 flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) -> 0 height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 } Accumulated learning constraints: { flip(leaf, leaf) <= True flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) /\ height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) False <= height(node(a, leaf, leaf), s(s(z))) False <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) } Current best model: |_ name: None flip -> [ flip : { flip(leaf, leaf) <= True flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= True } ] ; 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) } ] ; leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= True max_ite(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: flip(leaf, leaf) <= True : No: () height(leaf, z) <= True : No: () leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(z, n2) <= True : No: () eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) : Yes: { _lv -> s(z) ; _mv -> node(_ypyve_0, node(_jryve_0, leaf, _jryve_2), _ypyve_2) ; _nv -> s(s(z)) ; t -> node(_aqyve_0, leaf, _aqyve_2) } flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) : No: () height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) : Yes: { _fv -> z ; _gv -> s(z) ; _hv -> s(_iqyve_0) ; t1 -> leaf ; t2 -> node(_kqyve_0, leaf, _kqyve_2) } leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () ------------------------------------------- Step 6, which took 0.012965 s (model generation: 0.012392, model checking: 0.000573): Clauses: { flip(leaf, leaf) <= True -> 0 height(leaf, z) <= True -> 0 leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(z, n2) <= True -> 0 eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) -> 0 flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) -> 0 height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 } Accumulated learning constraints: { flip(leaf, leaf) <= True flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True height(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True False <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) False <= height(node(a, leaf, leaf), s(s(z))) False <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) } Current best model: |_ name: None flip -> [ flip : { flip(leaf, leaf) <= True flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_2, x_1_1) } ] ; 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) } ] ; leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= True max_ite(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: flip(leaf, leaf) <= True : No: () height(leaf, z) <= True : No: () leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(z, n2) <= True : No: () eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) : Yes: { _lv -> s(s(z)) ; _mv -> node(_esyve_0, leaf, leaf) ; _nv -> s(z) ; t -> node(_gsyve_0, node(_owyve_0, _owyve_1, leaf), leaf) } flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) : No: () height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) : Yes: { _fv -> z ; _gv -> s(z) ; _hv -> s(s(_fxyve_0)) ; t1 -> leaf ; t2 -> node(_ptyve_0, leaf, leaf) } leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () ------------------------------------------- Step 7, which took 0.028797 s (model generation: 0.028162, model checking: 0.000635): Clauses: { flip(leaf, leaf) <= True -> 0 height(leaf, z) <= True -> 0 leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(z, n2) <= True -> 0 eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) -> 0 flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) -> 0 height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 } Accumulated learning constraints: { flip(leaf, leaf) <= True flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True height(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True False <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) False <= height(node(a, leaf, leaf), s(s(z))) False <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max_ite(z, s(z), s(s(z))) } Current best model: |_ name: None flip -> [ flip : { flip(leaf, leaf) <= True flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_1) /\ flip(x_0_2, x_1_2) } ] ; height -> [ height : { _r_1(leaf, z) <= True _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= 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) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) } ] ; leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= True max_ite(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: flip(leaf, leaf) <= True : No: () height(leaf, z) <= True : No: () leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(z, n2) <= True : No: () eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) : Yes: { _lv -> s(s(z)) ; _mv -> node(_pxyve_0, node(_jczve_0, leaf, leaf), leaf) ; _nv -> s(s(s(_qczve_0))) ; t -> node(_rxyve_0, node(_hczve_0, leaf, leaf), leaf) } flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) : Yes: { _wu -> node(_myyve_0, leaf, leaf) ; _xu -> leaf ; t1 -> leaf ; t2 -> node(_pyyve_0, leaf, leaf) } height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () ------------------------------------------- Step 8, which took 0.037191 s (model generation: 0.036524, model checking: 0.000667): Clauses: { flip(leaf, leaf) <= True -> 0 height(leaf, z) <= True -> 0 leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(z, n2) <= True -> 0 eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) -> 0 flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) -> 0 height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 } Accumulated learning constraints: { flip(leaf, leaf) <= True flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) <= True height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True height(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True False <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)) /\ height(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) False <= height(node(a, leaf, leaf), s(s(z))) False <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max_ite(z, s(z), s(s(z))) } Current best model: |_ name: None flip -> [ flip : { flip(leaf, leaf) <= True flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1) } ] ; height -> [ height : { _r_1(leaf, z) <= True _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= 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) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) } ] ; leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= True max_ite(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: flip(leaf, leaf) <= True : No: () height(leaf, z) <= True : No: () leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(z, n2) <= True : No: () eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) : Yes: { _lv -> s(s(z)) ; _mv -> node(_adzve_0, leaf, node(_wgzve_0, leaf, leaf)) ; _nv -> s(s(s(_jizve_0))) ; t -> node(_cdzve_0, node(_ugzve_0, leaf, leaf), leaf) } flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) : No: () height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () ------------------------------------------- Step 9, which took 0.035513 s (model generation: 0.034534, model checking: 0.000979): Clauses: { flip(leaf, leaf) <= True -> 0 height(leaf, z) <= True -> 0 leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(z, n2) <= True -> 0 eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) -> 0 flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) -> 0 height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 } Accumulated learning constraints: { flip(leaf, leaf) <= True flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) <= True height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True height(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True False <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) /\ height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)) /\ height(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) False <= height(node(a, leaf, leaf), s(s(z))) False <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max_ite(z, s(z), s(s(z))) } Current best model: |_ name: None flip -> [ flip : { flip(leaf, leaf) <= True flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1) } ] ; 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) } ] ; leq_nat -> [ leq_nat : { _r_1(z) <= True leq_nat(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_1(z) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= _r_1(x_2_0) max_ite(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: flip(leaf, leaf) <= True : No: () height(leaf, z) <= True : No: () leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(z, n2) <= True : No: () eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) : Yes: { _lv -> s(s(z)) ; _mv -> node(_lizve_0, leaf, node(_qnzve_0, leaf, leaf)) ; _nv -> s(z) ; t -> node(_nizve_0, node(_pnzve_0, leaf, leaf), leaf) } flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) : No: () height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) : Yes: { _fv -> s(z) ; _gv -> z ; _hv -> s(s(_enzve_0)) ; t1 -> node(_ykzve_0, leaf, leaf) ; t2 -> leaf } leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : Yes: { nn1 -> s(z) ; nn2 -> s(_amzve_0) } max_ite(x, y, y) <= leq_nat(x, y) : Yes: { x -> z ; y -> s(s(_pmzve_0)) } leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () ------------------------------------------- Step 10, which took 0.042495 s (model generation: 0.040907, model checking: 0.001588): Clauses: { flip(leaf, leaf) <= True -> 0 height(leaf, z) <= True -> 0 leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(z, n2) <= True -> 0 eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) -> 0 flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) -> 0 height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 } Accumulated learning constraints: { flip(leaf, leaf) <= True flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) <= True height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True height(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True False <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) /\ height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) /\ height(node(a, leaf, node(a, leaf, leaf)), s(z)) False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)) /\ height(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) False <= height(node(a, leaf, leaf), s(s(z))) False <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) max_ite(z, s(s(z)), s(s(z))) <= leq_nat(z, s(s(z))) height(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max_ite(s(z), z, s(s(z))) height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max_ite(z, s(z), s(s(z))) } Current best model: |_ name: None flip -> [ flip : { _r_1(node(x_0_0, x_0_1, x_0_2)) <= True flip(leaf, leaf) <= True flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= _r_1(x_0_2) /\ flip(x_0_2, x_1_1) flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_1) /\ flip(x_0_2, x_1_1) } ] ; height -> [ height : { _r_1(node(x_0_0, x_0_1, x_0_2)) <= 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) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(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) } ] ; leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= True max_ite(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: flip(leaf, leaf) <= True : No: () height(leaf, z) <= True : No: () leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(z, n2) <= True : No: () eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) : Yes: { _lv -> s(z) ; _mv -> node(_rrzve_0, node(_xdawe_0, leaf, _xdawe_2), node(_ldawe_0, _ldawe_1, node(_mcawe_0, _mcawe_1, _mcawe_2))) ; _nv -> s(s(_mdawe_0)) ; t -> node(_trzve_0, node(_mcawe_0, _mcawe_1, _mcawe_2), node(_wdawe_0, leaf, leaf)) } flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) : Yes: { _wu -> leaf ; _xu -> node(_luzve_0, leaf, _luzve_2) ; t1 -> node(_muzve_0, leaf, leaf) ; t2 -> leaf } height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () ------------------------------------------- Step 11, which took 0.102181 s (model generation: 0.101350, model checking: 0.000831): Clauses: { flip(leaf, leaf) <= True -> 0 height(leaf, z) <= True -> 0 leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(z, n2) <= True -> 0 eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) -> 0 flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) -> 0 height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 } Accumulated learning constraints: { flip(leaf, leaf) <= True flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) <= True flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True height(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True False <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)) /\ height(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(z))) False <= height(node(a, leaf, leaf), s(s(z))) False <= height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) False <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) False <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) max_ite(z, s(s(z)), s(s(z))) <= leq_nat(z, s(s(z))) height(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max_ite(s(z), z, s(s(z))) False <= max_ite(z, s(z), s(s(z))) } Current best model: |_ name: None flip -> [ flip : { flip(leaf, leaf) <= True flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1) } ] ; height -> [ height : { _r_2(node(x_0_0, x_0_1, x_0_2)) <= 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) height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_2, x_1_0) } ] ; leq_nat -> [ leq_nat : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True leq_nat(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: flip(leaf, leaf) <= True : No: () height(leaf, z) <= True : No: () leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(z, n2) <= True : No: () eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) : Yes: { _lv -> s(z) ; _mv -> node(_oeawe_0, node(_kkawe_0, leaf, leaf), node(_djawe_0, leaf, leaf)) ; _nv -> s(s(_bjawe_0)) ; t -> node(_qeawe_0, node(_cjawe_0, leaf, leaf), node(_lkawe_0, leaf, leaf)) } flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) : No: () height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) : Yes: { _fv -> z ; _gv -> s(s(z)) ; _hv -> s(s(s(_ukawe_0))) ; t1 -> leaf ; t2 -> node(_xgawe_0, leaf, node(_glawe_0, leaf, leaf)) } leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : Yes: { nn1 -> z ; nn2 -> s(_fiawe_0) } max_ite(x, y, y) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : Yes: { nn1 -> s(z) ; nn2 -> s(s(_viawe_0)) } False <= leq_nat(s(nn1), z) : No: () ------------------------------------------- Step 12, which took 0.137266 s (model generation: 0.136256, model checking: 0.001010): Clauses: { flip(leaf, leaf) <= True -> 0 height(leaf, z) <= True -> 0 leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(z, n2) <= True -> 0 eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) -> 0 flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) -> 0 height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 } Accumulated learning constraints: { flip(leaf, leaf) <= True flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) <= True flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True height(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True False <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)) /\ height(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(z))) False <= height(node(a, leaf, leaf), s(s(z))) False <= height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) False <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) False <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) max_ite(z, s(s(z)), s(s(z))) <= leq_nat(z, s(s(z))) height(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max_ite(s(z), z, s(s(z))) height(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= max_ite(z, s(s(z)), s(s(s(z)))) False <= max_ite(z, s(z), s(s(z))) } Current best model: |_ name: None flip -> [ flip : { flip(leaf, leaf) <= True flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1) } ] ; height -> [ height : { _r_2(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= 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)) <= height(x_0_2, x_1_0) } ] ; leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(z, z) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: flip(leaf, leaf) <= True : No: () height(leaf, z) <= True : No: () leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(z, n2) <= True : No: () eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) : Yes: { _lv -> s(s(s(_asawe_0))) ; _mv -> node(_tlawe_0, leaf, node(_krawe_0, leaf, leaf)) ; _nv -> s(s(z)) ; t -> node(_vlawe_0, node(_irawe_0, leaf, leaf), leaf) } flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) : No: () height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () ------------------------------------------- Step 13, which took 0.127988 s (model generation: 0.126242, model checking: 0.001746): Clauses: { flip(leaf, leaf) <= True -> 0 height(leaf, z) <= True -> 0 leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(z, n2) <= True -> 0 eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) -> 0 flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) -> 0 height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 } Accumulated learning constraints: { flip(leaf, leaf) <= True flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) <= True flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True height(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True False <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(z))) False <= height(node(a, leaf, leaf), s(s(z))) False <= height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) False <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) False <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) max_ite(z, s(s(z)), s(s(z))) <= leq_nat(z, s(s(z))) False <= max_ite(s(z), z, s(s(z))) height(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= max_ite(z, s(s(z)), s(s(s(z)))) False <= max_ite(z, s(z), s(s(z))) } Current best model: |_ name: None flip -> [ flip : { flip(leaf, leaf) <= True flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1) } ] ; height -> [ height : { _r_1(s(x_0_0)) <= True height(leaf, z) <= True height(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(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) } ] ; leq_nat -> [ leq_nat : { _r_2(z) <= True leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= _r_2(x_1_0) leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_2(z) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= _r_2(x_2_0) max_ite(z, s(x_1_0), s(x_2_0)) <= _r_2(x_2_0) max_ite(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: flip(leaf, leaf) <= True : No: () height(leaf, z) <= True : No: () leq_nat(x, y) \/ max_ite(x, y, x) <= True : Yes: { x -> z ; y -> s(s(_lzawe_0)) } leq_nat(z, n2) <= True : Yes: { n2 -> s(s(_lzawe_0)) } eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) : Yes: { _lv -> s(s(z)) ; _mv -> node(_cuawe_0, node(_xbbwe_0, leaf, leaf), leaf) ; _nv -> s(z) ; t -> node(_euawe_0, leaf, node(_wbbwe_0, leaf, leaf)) } flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) : No: () height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) : Yes: { _fv -> s(z) ; _gv -> s(z) ; _hv -> s(s(_cjbwe_0)) ; t1 -> node(_vyawe_0, leaf, leaf) ; t2 -> node(_wyawe_0, leaf, leaf) } leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () ------------------------------------------- Step 14, which took 0.135534 s (model generation: 0.130146, model checking: 0.005388): Clauses: { flip(leaf, leaf) <= True -> 0 height(leaf, z) <= True -> 0 leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(z, n2) <= True -> 0 eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) -> 0 flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) -> 0 height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 } Accumulated learning constraints: { flip(leaf, leaf) <= True flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) <= True flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True height(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(s(z))) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(s(z)), s(s(z))) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True False <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(z))) False <= height(node(a, leaf, leaf), s(s(z))) False <= height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) False <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) False <= height(node(a, node(a, leaf, leaf), leaf), s(z)) False <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max_ite(s(z), s(z), s(s(z))) False <= max_ite(s(z), z, s(s(z))) height(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= max_ite(z, s(s(z)), s(s(s(z)))) False <= max_ite(z, s(z), s(s(z))) } Current best model: |_ name: None flip -> [ flip : { flip(leaf, leaf) <= True flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1) } ] ; height -> [ height : { _r_2(leaf, s(x_1_0)) <= True _r_2(leaf, 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(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_2, x_1_0) /\ height(x_0_1, x_1_0) } ] ; leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(z, z) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: flip(leaf, leaf) <= True : No: () height(leaf, z) <= True : No: () leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(z, n2) <= True : No: () eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) : No: () flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) : No: () height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) : Yes: { _fv -> s(z) ; _gv -> s(z) ; _hv -> s(z) ; t1 -> node(_uqbwe_0, leaf, leaf) ; t2 -> node(_vqbwe_0, leaf, leaf) } leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : Yes: { x -> s(z) ; y -> s(s(_otbwe_0)) } leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () ------------------------------------------- Step 15, which took 0.798611 s (model generation: 0.162974, model checking: 0.635637): Clauses: { flip(leaf, leaf) <= True -> 0 height(leaf, z) <= True -> 0 leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(z, n2) <= True -> 0 eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) -> 0 flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) -> 0 height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 } Accumulated learning constraints: { flip(leaf, leaf) <= True flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) <= True flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True height(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(s(z))) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(s(z)), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(s(z)), s(s(z))) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True False <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(z))) False <= height(node(a, leaf, leaf), s(s(z))) False <= height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) False <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) False <= height(node(a, node(a, leaf, leaf), leaf), s(z)) False <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max_ite(s(z), s(z), s(s(z))) False <= max_ite(s(z), z, s(s(z))) height(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= max_ite(z, s(s(z)), s(s(s(z)))) False <= max_ite(z, s(z), s(s(z))) } Current best model: |_ name: None flip -> [ flip : { flip(leaf, leaf) <= True flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1) } ] ; height -> [ height : { _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)) <= 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(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_2, x_1_0) /\ height(x_0_1, x_1_0) } ] ; leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(z, z) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: flip(leaf, leaf) <= True : No: () height(leaf, z) <= True : No: () leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(z, n2) <= True : No: () eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) : Yes: { _lv -> s(s(z)) ; _mv -> node(_zsdwe_0, node(_vgewe_0, leaf, leaf), node(_ahewe_0, node(_umewe_0, leaf, leaf), leaf)) ; _nv -> s(s(s(z))) ; t -> node(_btdwe_0, node(_xgewe_0, leaf, node(_tmewe_0, leaf, leaf)), node(_zgewe_0, leaf, leaf)) } flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () ------------------------------------------- Step 16, which took 0.194521 s (model generation: 0.173423, model checking: 0.021098): Clauses: { flip(leaf, leaf) <= True -> 0 height(leaf, z) <= True -> 0 leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(z, n2) <= True -> 0 eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) -> 0 flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) -> 0 height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 } Accumulated learning constraints: { flip(leaf, leaf) <= True flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) <= True flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True height(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(s(z))) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(s(z)), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(s(z)), s(s(z))) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True False <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(z))) False <= flip(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))) /\ height(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) /\ height(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) False <= height(node(a, leaf, leaf), s(s(z))) False <= height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) False <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) False <= height(node(a, node(a, leaf, leaf), leaf), s(z)) False <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max_ite(s(z), s(z), s(s(z))) False <= max_ite(s(z), z, s(s(z))) height(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= max_ite(z, s(s(z)), s(s(s(z)))) False <= max_ite(z, s(z), s(s(z))) } Current best model: |_ name: None flip -> [ flip : { flip(leaf, leaf) <= True flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1) } ] ; height -> [ height : { _r_2(leaf, s(x_1_0)) <= True _r_2(leaf, 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(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_2, 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_1, x_1_0) /\ height(x_0_2, x_1_0) } ] ; leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(z, z) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: flip(leaf, leaf) <= True : No: () height(leaf, z) <= True : No: () leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(z, n2) <= True : No: () eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) : No: () flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) : No: () height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) : Yes: { _fv -> s(z) ; _gv -> s(s(z)) ; _hv -> s(s(z)) ; t1 -> node(_bytaf_0, leaf, leaf) ; t2 -> node(_cytaf_0, node(_oyvaf_0, leaf, leaf), node(_oyvaf_0, leaf, leaf)) } leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () ------------------------------------------- Step 17, which took 0.276318 s (model generation: 0.187551, model checking: 0.088767): Clauses: { flip(leaf, leaf) <= True -> 0 height(leaf, z) <= True -> 0 leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(z, n2) <= True -> 0 eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) -> 0 flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) -> 0 height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 } Accumulated learning constraints: { flip(leaf, leaf) <= True flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) <= True flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True height(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True height(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(s(z)))) <= True leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(s(z))) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(s(z)), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(s(z)), s(s(z))) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True False <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(z))) False <= flip(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))) /\ height(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) /\ height(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) False <= height(node(a, leaf, leaf), s(s(z))) False <= height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) False <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) False <= height(node(a, node(a, leaf, leaf), leaf), s(z)) False <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max_ite(s(z), s(z), s(s(z))) False <= max_ite(s(z), z, s(s(z))) height(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= max_ite(z, s(s(z)), s(s(s(z)))) False <= max_ite(z, s(z), s(s(z))) } Current best model: |_ name: None flip -> [ flip : { flip(leaf, leaf) <= True flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1) } ] ; height -> [ height : { _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_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)) <= _r_2(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_2, x_1_0) /\ height(x_0_1, x_1_0) } ] ; leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(z, z) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: flip(leaf, leaf) <= True : No: () height(leaf, z) <= True : No: () leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(z, n2) <= True : No: () eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) : Yes: { _lv -> s(s(s(z))) ; _mv -> node(_bhyaf_0, node(_tuyaf_0, node(_vazaf_0, leaf, leaf), leaf), node(_wuyaf_0, leaf, leaf)) ; _nv -> s(s(z)) ; t -> node(_dhyaf_0, node(_ruyaf_0, leaf, leaf), node(_vuyaf_0, leaf, node(_uazaf_0, leaf, leaf))) } flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) : No: () height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) : Yes: { _fv -> s(s(z)) ; _gv -> s(z) ; _hv -> s(z) ; t1 -> node(_qmyaf_0, leaf, node(_ieacf_0, leaf, leaf)) ; t2 -> node(_rmyaf_0, leaf, leaf) } leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () ------------------------------------------- Step 18, which took 0.318434 s (model generation: 0.258042, model checking: 0.060392): Clauses: { flip(leaf, leaf) <= True -> 0 height(leaf, z) <= True -> 0 leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(z, n2) <= True -> 0 eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) -> 0 flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) -> 0 height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 } Accumulated learning constraints: { flip(leaf, leaf) <= True flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) <= True flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True height(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True height(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(s(z)))) <= True leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(s(z))) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(s(z)), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(s(z)), s(s(z))) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True False <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(z))) False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), node(a, node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) /\ height(node(a, node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)), s(s(z))) False <= flip(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))) /\ height(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) /\ height(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) False <= height(node(a, leaf, leaf), s(s(z))) False <= height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) False <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) False <= height(node(a, node(a, leaf, leaf), leaf), s(z)) False <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) height(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) <= max_ite(s(s(z)), s(z), s(z)) height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max_ite(s(z), s(z), s(s(z))) False <= max_ite(s(z), z, s(s(z))) height(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= max_ite(z, s(s(z)), s(s(s(z)))) False <= max_ite(z, s(z), s(s(z))) } Current best model: |_ name: None flip -> [ flip : { flip(leaf, leaf) <= True flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1) } ] ; height -> [ height : { _r_2(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= height(x_0_1, x_1_0) /\ height(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)) <= _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)) <= height(x_0_1, x_1_0) /\ height(x_0_2, x_1_0) } ] ; leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(z, z) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: flip(leaf, leaf) <= True : No: () height(leaf, z) <= True : No: () leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(z, n2) <= True : No: () eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) : Yes: { _lv -> s(s(s(z))) ; _mv -> node(_siacf_0, node(_uxacf_0, node(_pudcf_0, leaf, leaf), node(_rudcf_0, leaf, leaf)), node(_sxacf_0, leaf, leaf)) ; _nv -> s(s(z)) ; t -> node(_uiacf_0, node(_vxacf_0, leaf, leaf), node(_qxacf_0, node(_qudcf_0, leaf, leaf), node(_oudcf_0, leaf, leaf))) } flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) : No: () height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) : Yes: { _fv -> z ; _gv -> s(s(z)) ; _hv -> s(s(z)) ; t1 -> leaf ; t2 -> node(_alacf_0, node(_byacf_0, leaf, leaf), leaf) } leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () Total time: 60.066909 Learner time: 1.481562 Teacher time: 0.820316 Reasons for stopping: Maybe: timeout during teacher: { height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> out of time }Last solver state: Clauses: { flip(leaf, leaf) <= True -> 0 height(leaf, z) <= True -> 0 leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(z, n2) <= True -> 0 eq_nat(_lv, _nv) <= flip(t, _mv) /\ height(_mv, _nv) /\ height(t, _lv) -> 0 flip(node(e, t1, t2), node(e, _wu, _xu)) <= flip(t1, _xu) /\ flip(t2, _wu) -> 0 height(node(e, t1, t2), s(_hv)) <= height(t1, _fv) /\ height(t2, _gv) /\ max_ite(_fv, _gv, _hv) -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 } Accumulated learning constraints: { flip(leaf, leaf) <= True flip(node(a, leaf, leaf), node(a, leaf, leaf)) <= True flip(node(a, leaf, node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)) <= True flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, node(a, leaf, leaf))) <= True height(leaf, z) <= True height(node(a, leaf, leaf), s(z)) <= True height(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True height(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) <= True height(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True height(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(s(z)))) <= True leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(s(z))) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(s(z)), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(s(z)), s(s(z))) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True False <= flip(node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)) False <= flip(node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)) False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf)))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(z)) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(z))) False <= flip(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), node(a, node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf))) /\ height(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) /\ height(node(a, node(a, node(a, leaf, leaf), leaf), node(a, leaf, leaf)), s(s(z))) False <= flip(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, leaf, leaf))) /\ height(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) False <= flip(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf))) /\ height(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) /\ height(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) False <= height(node(a, leaf, leaf), s(s(z))) False <= height(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) False <= height(node(a, leaf, node(a, leaf, leaf)), s(z)) False <= height(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) False <= height(node(a, node(a, leaf, leaf), leaf), s(z)) False <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) height(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) <= max_ite(s(s(z)), s(z), s(z)) height(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max_ite(s(z), s(z), s(s(z))) False <= max_ite(s(z), z, s(s(z))) height(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= max_ite(z, s(s(z)), s(s(s(z)))) False <= max_ite(z, s(z), s(s(z))) } Current best model: |_ name: None flip -> [ flip : { flip(leaf, leaf) <= True flip(node(x_0_0, x_0_1, x_0_2), node(x_1_0, x_1_1, x_1_2)) <= flip(x_0_1, x_1_2) /\ flip(x_0_2, x_1_1) } ] ; height -> [ height : { _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_2(x_0_1, 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)) <= _r_2(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_2, x_1_0) /\ height(x_0_1, x_1_0) } ] ; leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(z, z) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= max_ite(x_0_0, x_1_0, x_2_0) max_ite(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _|