Solving ../../benchmarks/smtlib/true/tree_depth_le_node.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: { (le, P: { le(z, s(nn2)) <= True le(s(nn1), s(nn2)) <= le(nn1, nn2) le(nn1, nn2) <= le(s(nn1), s(nn2)) False <= le(s(nn1), z) False <= le(z, z) } ) (leq, P: { leq(z, n2) <= True leq(s(nn1), s(nn2)) <= leq(nn1, nn2) leq(nn1, nn2) <= leq(s(nn1), s(nn2)) False <= leq(s(nn1), z) } ) (max, F: { leq(n, m) \/ max(n, m, n) <= True max(n, m, m) <= leq(n, m) } eq_nat(_ola, _pla) <= max(_mla, _nla, _ola) /\ max(_mla, _nla, _pla) ) (depth, F: { depth(leaf, z) <= True depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) } eq_nat(_ula, _vla) <= depth(_tla, _ula) /\ depth(_tla, _vla) ) } properties: { le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) } over-approximation: {depth, max} under-approximation: {le} Clause system for inference is: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Solving took 60.466296 seconds. Maybe: timeout during teacher: { depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> out of time le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> out of time }Last solver state: Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(s(z)))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True leq(s(z), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), s(s(z))) <= True max(s(z), s(s(z)), 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 le(s(s(z)), s(z)) <= depth(leaf, s(s(z))) False <= depth(leaf, s(s(z))) /\ max(z, s(s(z)), s(z)) False <= depth(leaf, s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) False <= depth(node(a, leaf, leaf), s(s(z))) False <= depth(node(a, leaf, node(a, leaf, leaf)), s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) /\ depth(node(a, node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ depth(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) depth(node(a, leaf, node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))), s(s(s(z)))) <= depth(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(z))) /\ max(z, s(s(z)), s(s(z))) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) le(s(s(s(s(z)))), s(s(s(s(z))))) <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) /\ depth(node(a, node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), leaf), s(s(s(s(z))))) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) False <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) depth(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), leaf), s(s(z))) <= depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ max(s(s(s(s(s(z))))), z, s(z)) False <= le(s(s(z)), s(s(z))) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) depth(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)), s(s(s(s(z))))) <= max(s(s(z)), s(s(z)), s(s(s(z)))) False <= max(s(s(z)), s(z), s(z)) depth(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), leaf), s(s(s(z)))) <= max(s(s(z)), z, s(s(z))) False <= max(s(s(z)), z, s(z)) depth(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= max(s(z), s(s(z)), s(s(s(z)))) depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max(s(z), s(z), s(s(z))) depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) depth(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= max(z, s(s(z)), s(s(s(z)))) depth(node(a, leaf, node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(s(z)))) <= max(z, s(s(z)), s(s(z))) depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= max(z, s(s(z)), s(z)) depth(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z))) } Current best model: |_ name: None depth -> [ depth : { _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) depth(leaf, z) <= True depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ depth(x_0_2, x_1_0) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ depth(x_0_1, x_1_0) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; max -> [ max : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(z, z) <= True max(s(x_0_0), s(x_1_0), s(x_2_0)) <= max(x_0_0, x_1_0, x_2_0) max(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) max(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.007993 s (model generation: 0.007837, model checking: 0.000156): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { } Current best model: |_ name: None depth -> [ depth : { } ] ; le -> [ le : { } ] ; leq -> [ leq : { } ] ; max -> [ max : { } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : Yes: { } leq(n, m) \/ max(n, m, n) <= True : Yes: { m -> z ; n -> z } leq(z, n2) <= True : Yes: { n2 -> z } depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : No: () le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : No: () le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 1, which took 0.013865 s (model generation: 0.013713, model checking: 0.000152): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True leq(z, z) <= True } Current best model: |_ name: None depth -> [ depth : { depth(leaf, z) <= True } ] ; le -> [ le : { } ] ; leq -> [ leq : { leq(z, z) <= True } ] ; max -> [ max : { } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : Yes: { m -> z ; n -> s(_jgmcd_0) } leq(z, n2) <= True : Yes: { n2 -> s(_mgmcd_0) } depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : No: () le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : No: () le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : Yes: { m -> z ; n -> z } leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : Yes: { nn1 -> z ; nn2 -> z } leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 2, which took 0.015312 s (model generation: 0.015140, model checking: 0.000172): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True leq(s(z), s(z)) <= True leq(s(z), z) \/ max(s(z), z, s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(z, z, z) <= True } Current best model: |_ name: None depth -> [ depth : { depth(leaf, z) <= True } ] ; le -> [ le : { } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= True leq(s(x_0_0), z) <= True leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; max -> [ max : { max(s(x_0_0), z, s(x_2_0)) <= True max(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : Yes: { _qla -> z ; _rla -> z ; _sla -> z ; t1 -> leaf ; t2 -> leaf } le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : No: () le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : Yes: { m -> z ; n -> s(_zgmcd_0) } leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : Yes: { } ------------------------------------------- Step 3, which took 0.018607 s (model generation: 0.018462, model checking: 0.000145): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(z), z, s(z)) <= True max(z, z, z) <= True False <= leq(s(z), z) } Current best model: |_ name: None depth -> [ depth : { depth(leaf, z) <= True depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True } ] ; le -> [ le : { } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= True leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; max -> [ max : { max(s(x_0_0), z, s(x_2_0)) <= True max(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : No: () le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : Yes: { _wla -> z ; _xla -> s(_dhmcd_0) ; t1 -> leaf } le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : Yes: { m -> s(_khmcd_0) ; n -> z } leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : Yes: { nn1 -> s(_mhmcd_0) ; nn2 -> z } False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 4, which took 0.013500 s (model generation: 0.013337, model checking: 0.000163): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True le(z, s(z)) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(z), z, s(z)) <= True max(z, s(z), s(z)) <= True max(z, z, z) <= True False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) } Current best model: |_ name: None depth -> [ depth : { depth(leaf, z) <= True depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True } ] ; le -> [ le : { le(z, s(x_1_0)) <= True le(z, z) <= True } ] ; leq -> [ leq : { le(z, s(x_1_0)) <= True le(z, z) <= True leq(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; max -> [ max : { 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 } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : Yes: { m -> s(z) ; n -> s(s(_limcd_0)) } leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : No: () le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : Yes: { _wla -> s(_qhmcd_0) ; _xla -> s(_rhmcd_0) ; t1 -> node(_shmcd_0, _shmcd_1, _shmcd_2) } le(s(nn1), s(nn2)) <= le(nn1, nn2) : Yes: { nn1 -> z ; nn2 -> z } le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : Yes: { } max(n, m, m) <= leq(n, m) : Yes: { m -> s(z) ; n -> s(z) } leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : Yes: { nn1 -> s(z) ; nn2 -> s(z) } leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 5, which took 0.010624 s (model generation: 0.010500, model checking: 0.000124): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), 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 le(s(z), s(z)) <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) } Current best model: |_ name: None depth -> [ depth : { depth(leaf, z) <= True depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= True le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; 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 } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : No: () le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : No: () le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : Yes: { nn1 -> z ; nn2 -> z } False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 6, which took 0.010547 s (model generation: 0.010323, model checking: 0.000224): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), 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 False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) False <= le(s(z), s(z)) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) } Current best model: |_ name: None depth -> [ depth : { depth(leaf, z) <= True depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= depth(x_0_1, x_1_0) } ] ; le -> [ le : { le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; 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 } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : Yes: { _qla -> z ; _rla -> s(z) ; _sla -> s(_qjmcd_0) ; t1 -> leaf ; t2 -> node(_sjmcd_0, leaf, _sjmcd_2) } le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : Yes: { _wla -> s(z) ; _xla -> s(s(z)) ; t1 -> node(_fkmcd_0, leaf, _fkmcd_2) } le(s(nn1), s(nn2)) <= le(nn1, nn2) : Yes: { nn1 -> z ; nn2 -> s(_hkmcd_0) } le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 7, which took 0.011879 s (model generation: 0.011108, model checking: 0.000771): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), 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 False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) False <= le(s(z), s(z)) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) } Current best model: |_ name: None depth -> [ depth : { depth(leaf, s(x_1_0)) <= True depth(leaf, z) <= True depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= depth(x_0_1, x_1_0) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; 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 } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : Yes: { _qla -> s(s(s(z))) ; _rla -> s(z) ; _sla -> s(z) ; t1 -> node(_ummcd_0, node(_momcd_0, node(_dpmcd_0, leaf, _dpmcd_2), _momcd_2), _ummcd_2) ; t2 -> node(_vmmcd_0, leaf, _vmmcd_2) } le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : Yes: { _wla -> s(z) ; _xla -> s(z) ; t1 -> leaf } le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 8, which took 0.041540 s (model generation: 0.041258, model checking: 0.000282): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), 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 False <= depth(leaf, s(z)) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) False <= le(s(z), s(z)) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) } Current best model: |_ name: None depth -> [ depth : { _r_1(leaf) <= True depth(leaf, z) <= True depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; 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 } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : Yes: { _qla -> s(_vpmcd_0) ; _rla -> s(_wpmcd_0) ; _sla -> s(_xpmcd_0) ; t1 -> node(_ypmcd_0, leaf, _ypmcd_2) ; t2 -> node(_zpmcd_0, leaf, _zpmcd_2) } le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : No: () le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 9, which took 0.033281 s (model generation: 0.032588, model checking: 0.000693): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), 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 False <= depth(leaf, s(z)) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) False <= le(s(z), s(z)) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) } Current best model: |_ name: None depth -> [ depth : { _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)) <= True depth(leaf, z) <= True depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; 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 } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : No: () le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : Yes: { _wla -> s(s(z)) ; _xla -> s(s(z)) ; t1 -> node(_bsmcd_0, node(_ftmcd_0, _ftmcd_1, _ftmcd_2), _bsmcd_2) } le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 10, which took 0.032437 s (model generation: 0.031986, model checking: 0.000451): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), 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 False <= depth(leaf, s(z)) le(s(s(z)), s(s(z))) <= depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) False <= le(s(z), s(z)) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) } Current best model: |_ name: None depth -> [ depth : { _r_1(s(x_0_0)) <= True depth(leaf, z) <= True depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_1_0) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= depth(x_0_1, x_1_0) } ] ; le -> [ le : { _r_1(s(x_0_0)) <= True le(s(x_0_0), s(x_1_0)) <= _r_1(x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; 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 } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : No: () le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : No: () le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : Yes: { nn1 -> s(_xvmcd_0) ; nn2 -> s(z) } False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 11, which took 0.031688 s (model generation: 0.031227, model checking: 0.000461): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), 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 False <= depth(leaf, s(z)) False <= depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) False <= le(s(s(z)), s(s(z))) False <= le(s(z), s(z)) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) } Current best model: |_ name: None depth -> [ depth : { _r_1(node(x_0_0, x_0_1, x_0_2)) <= True depth(leaf, z) <= True depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= depth(x_0_1, x_1_0) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; 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 } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : Yes: { _qla -> s(z) ; _rla -> z ; _sla -> s(s(_jancd_0)) ; t1 -> node(_cymcd_0, leaf, leaf) ; t2 -> leaf } le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : Yes: { _wla -> s(z) ; _xla -> s(z) ; t1 -> node(_qymcd_0, _qymcd_1, node(_uzmcd_0, _uzmcd_1, _uzmcd_2)) ; t2 -> node(_uzmcd_0, _uzmcd_1, _uzmcd_2) } le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 12, which took 0.049262 s (model generation: 0.048242, model checking: 0.001020): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), 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 False <= depth(leaf, s(z)) False <= depth(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z)) False <= depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) False <= le(s(s(z)), s(s(z))) False <= le(s(z), s(z)) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) } Current best model: |_ name: None depth -> [ depth : { _r_1(s(x_0_0)) <= True depth(leaf, s(x_1_0)) <= _r_1(x_1_0) depth(leaf, z) <= True depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_1_0) /\ depth(x_0_2, x_1_0) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= depth(x_0_1, x_1_0) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; 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 } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : Yes: { _qla -> z ; _rla -> s(s(_aincd_0)) ; _sla -> s(z) ; t1 -> leaf ; t2 -> leaf } le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : Yes: { _wla -> s(s(_dincd_0)) ; _xla -> s(z) ; t1 -> leaf } le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 13, which took 0.051723 s (model generation: 0.050366, model checking: 0.001357): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), 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 le(s(s(z)), s(z)) <= depth(leaf, s(s(z))) depth(node(a, leaf, leaf), s(s(z))) <= depth(leaf, s(s(z))) /\ max(z, s(s(z)), s(z)) False <= depth(leaf, s(z)) False <= depth(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z)) False <= depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) False <= le(s(s(z)), s(s(z))) False <= le(s(z), s(z)) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) } Current best model: |_ name: None depth -> [ depth : { _r_1(leaf, s(x_1_0)) <= True depth(leaf, z) <= True depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= depth(x_0_1, x_1_0) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(s(x_0_0), z) <= True le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; max -> [ max : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True max(s(x_0_0), s(x_1_0), s(x_2_0)) <= leq(x_0_0, x_2_0) 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 } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : Yes: { _qla -> s(s(s(s(s(_cmncd_0))))) ; _rla -> z ; _sla -> s(z) ; t1 -> node(_dkncd_0, node(_cnncd_0, node(_ioncd_0, node(_omncd_0, leaf, _omncd_2), _ioncd_2), _cnncd_2), _dkncd_2) ; t2 -> leaf } le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : Yes: { _wla -> s(s(z)) ; _xla -> s(s(z)) ; t1 -> node(_ukncd_0, leaf, _ukncd_2) } le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : Yes: { } False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 14, which took 0.058451 s (model generation: 0.056994, model checking: 0.001457): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), 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 le(s(s(z)), s(z)) <= depth(leaf, s(s(z))) depth(node(a, leaf, leaf), s(s(z))) <= depth(leaf, s(s(z))) /\ max(z, s(s(z)), s(z)) False <= depth(leaf, s(z)) False <= depth(node(a, leaf, leaf), s(s(z))) /\ depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) False <= depth(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z)) False <= depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) depth(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), leaf), s(s(z))) <= depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ max(s(s(s(s(s(z))))), z, s(z)) False <= le(s(s(z)), s(s(z))) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) } Current best model: |_ name: None depth -> [ depth : { _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) depth(leaf, z) <= True depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= depth(x_0_1, x_1_0) /\ depth(x_0_2, x_1_0) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; max -> [ max : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= leq(x_0_0, x_2_0) max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : Yes: { _qla -> s(s(_huncd_0)) ; _rla -> s(s(_htncd_0)) ; _sla -> s(z) ; t1 -> node(_eqncd_0, leaf, node(_nuncd_0, _nuncd_1, _nuncd_2)) ; t2 -> node(_fqncd_0, leaf, _fqncd_2) } le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : Yes: { _wla -> s(s(s(z))) ; _xla -> s(s(s(z))) ; t1 -> node(_bsncd_0, leaf, _bsncd_2) } le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 15, which took 0.377859 s (model generation: 0.376359, model checking: 0.001500): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), 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 le(s(s(z)), s(z)) <= depth(leaf, s(s(z))) depth(node(a, leaf, leaf), s(s(z))) <= depth(leaf, s(s(z))) /\ max(z, s(s(z)), s(z)) False <= depth(leaf, s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) False <= depth(node(a, leaf, leaf), s(s(z))) /\ depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, leaf, leaf), s(s(z))) /\ max(s(s(z)), s(s(z)), s(z)) False <= depth(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z)) False <= depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) depth(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), leaf), s(s(z))) <= depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ max(s(s(s(s(s(z))))), z, s(z)) False <= le(s(s(z)), s(s(z))) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) } Current best model: |_ name: None depth -> [ depth : { _r_1(leaf, s(x_1_0)) <= True _r_1(leaf, z) <= 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) depth(leaf, z) <= True depth(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) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; 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 } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : Yes: { _qla -> z ; _rla -> s(s(z)) ; _sla -> s(z) ; t1 -> leaf ; t2 -> node(_rvncd_0, node(_maocd_0, leaf, _maocd_2), _rvncd_2) } le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : Yes: { _wla -> s(s(z)) ; _xla -> s(s(z)) ; t1 -> node(_fyncd_0, leaf, node(_pzncd_0, leaf, _pzncd_2)) } le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 16, which took 0.482350 s (model generation: 0.480981, model checking: 0.001369): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), 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 le(s(s(z)), s(z)) <= depth(leaf, s(s(z))) depth(node(a, leaf, leaf), s(s(z))) <= depth(leaf, s(s(z))) /\ max(z, s(s(z)), s(z)) False <= depth(leaf, s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) False <= depth(node(a, leaf, leaf), s(s(z))) /\ depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, leaf, leaf), s(s(z))) /\ max(s(s(z)), s(s(z)), s(z)) False <= depth(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z)) False <= depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z)) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) depth(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), leaf), s(s(z))) <= depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ max(s(s(s(s(s(z))))), z, s(z)) False <= le(s(s(z)), s(s(z))) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) } Current best model: |_ name: None depth -> [ depth : { _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True depth(leaf, z) <= True depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= depth(x_0_1, x_1_0) /\ depth(x_0_2, x_1_0) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; max -> [ max : { _r_2(z) <= True max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= _r_2(x_2_0) max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : Yes: { m -> z ; n -> s(s(_yfocd_0)) } leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : Yes: { _qla -> s(s(_kgocd_0)) ; _rla -> z ; _sla -> s(z) ; t1 -> node(_rdocd_0, _rdocd_1, node(_jgocd_0, _jgocd_1, _jgocd_2)) ; t2 -> leaf } le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : Yes: { _wla -> s(s(z)) ; _xla -> s(s(z)) ; t1 -> node(_ueocd_0, _ueocd_1, node(_bgocd_0, _bgocd_1, _bgocd_2)) ; t2 -> node(_zfocd_0, _zfocd_1, _zfocd_2) } le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 17, which took 0.245289 s (model generation: 0.243585, model checking: 0.001704): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), 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 le(s(s(z)), s(z)) <= depth(leaf, s(s(z))) depth(node(a, leaf, leaf), s(s(z))) <= depth(leaf, s(s(z))) /\ max(z, s(s(z)), s(z)) False <= depth(leaf, s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) False <= depth(node(a, leaf, leaf), s(s(z))) /\ depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) False <= depth(node(a, leaf, leaf), s(s(z))) /\ max(s(s(z)), s(s(z)), s(z)) False <= depth(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z)) False <= depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z)) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) depth(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), leaf), s(s(z))) <= depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ max(s(s(s(s(s(z))))), z, s(z)) False <= le(s(s(z)), s(s(z))) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= max(s(s(z)), z, s(z)) depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) } Current best model: |_ name: None depth -> [ depth : { _r_2(leaf, s(x_1_0)) <= True depth(leaf, z) <= True depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= depth(x_0_1, x_1_0) /\ depth(x_0_2, x_1_0) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True leq(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; max -> [ max : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True max(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) max(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : Yes: { _qla -> s(s(_hnocd_0)) ; _rla -> z ; _sla -> s(s(_inocd_0)) ; t1 -> node(_iiocd_0, leaf, _iiocd_2) ; t2 -> leaf } le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : Yes: { _wla -> s(s(s(z))) ; _xla -> s(s(s(z))) ; t1 -> node(_nkocd_0, leaf, _nkocd_2) ; t2 -> node(_ulocd_0, leaf, _ulocd_2) } le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : Yes: { nn1 -> z ; nn2 -> s(_jlocd_0) } leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : Yes: { nn1 -> s(z) ; nn2 -> s(s(_lmocd_0)) } False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 18, which took 0.276520 s (model generation: 0.273847, model checking: 0.002673): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True leq(s(z), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), 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 le(s(s(z)), s(z)) <= depth(leaf, s(s(z))) depth(node(a, leaf, leaf), s(s(z))) <= depth(leaf, s(s(z))) /\ max(z, s(s(z)), s(z)) False <= depth(leaf, s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) False <= depth(node(a, leaf, leaf), s(s(z))) /\ depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) False <= depth(node(a, leaf, leaf), s(s(z))) /\ max(s(s(z)), s(s(z)), s(z)) depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(z))) /\ max(s(s(z)), z, s(s(z))) False <= depth(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z)) False <= depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z)) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) depth(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), leaf), s(s(z))) <= depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ max(s(s(s(s(s(z))))), z, s(z)) False <= le(s(s(z)), s(s(z))) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= max(s(s(z)), z, s(z)) depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) } Current best model: |_ name: None depth -> [ depth : { _r_2(leaf, s(x_1_0)) <= True depth(leaf, z) <= True depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ depth(x_0_2, x_1_0) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= depth(x_0_1, x_1_0) /\ depth(x_0_2, x_1_0) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; max -> [ max : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True max(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) max(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) max(z, s(x_1_0), s(x_2_0)) <= True max(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : Yes: { _qla -> z ; _rla -> s(z) ; _sla -> s(s(_cbpcd_0)) ; t1 -> leaf ; t2 -> node(_vpocd_0, leaf, leaf) } le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : No: () le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : Yes: { m -> s(s(_vvocd_0)) ; n -> s(z) } leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 19, which took 0.293636 s (model generation: 0.291297, model checking: 0.002339): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True leq(s(z), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), s(s(z))) <= True max(s(z), s(s(z)), 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 le(s(s(z)), s(z)) <= depth(leaf, s(s(z))) depth(node(a, leaf, leaf), s(s(z))) <= depth(leaf, s(s(z))) /\ max(z, s(s(z)), s(z)) False <= depth(leaf, s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) False <= depth(node(a, leaf, leaf), s(s(z))) /\ depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) False <= depth(node(a, leaf, leaf), s(s(z))) /\ max(s(s(z)), s(s(z)), s(z)) depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(z))) /\ max(s(s(z)), z, s(s(z))) False <= depth(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z)) False <= depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) /\ max(z, s(s(z)), s(z)) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) depth(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), leaf), s(s(z))) <= depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ max(s(s(s(s(s(z))))), z, s(z)) False <= le(s(s(z)), s(s(z))) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= max(s(s(z)), z, s(z)) depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) depth(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z))) } Current best model: |_ name: None depth -> [ depth : { _r_2(leaf, s(x_1_0)) <= True depth(leaf, z) <= True depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ depth(x_0_2, x_1_0) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= depth(x_0_1, x_1_0) /\ depth(x_0_2, x_1_0) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; max -> [ max : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) max(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : Yes: { _qla -> s(z) ; _rla -> z ; _sla -> s(z) ; t1 -> node(_ngpcd_0, leaf, leaf) ; t2 -> leaf } le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : No: () le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 20, which took 0.277747 s (model generation: 0.276359, model checking: 0.001388): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True leq(s(z), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), s(s(z))) <= True max(s(z), s(s(z)), 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 le(s(s(z)), s(z)) <= depth(leaf, s(s(z))) False <= depth(leaf, s(s(z))) /\ max(z, s(s(z)), s(z)) False <= depth(leaf, s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) False <= depth(node(a, leaf, leaf), s(s(z))) False <= depth(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z)) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) False <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) depth(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), leaf), s(s(z))) <= depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ max(s(s(s(s(s(z))))), z, s(z)) False <= le(s(s(z)), s(s(z))) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= max(s(s(z)), z, s(z)) depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= max(z, s(s(z)), s(z)) depth(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z))) } Current best model: |_ name: None depth -> [ depth : { _r_1(leaf, s(x_1_0)) <= True _r_1(leaf, z) <= 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) /\ _r_1(x_0_2, x_1_0) depth(leaf, z) <= True depth(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) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; max -> [ max : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= leq(x_0_0, x_2_0) max(z, s(x_1_0), s(x_2_0)) <= leq(x_1_0, x_2_0) max(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : Yes: { _qla -> s(z) ; _rla -> s(z) ; _sla -> s(z) ; t1 -> node(_zppcd_0, leaf, node(_uspcd_0, _uspcd_1, _uspcd_2)) ; t2 -> node(_aqpcd_0, leaf, _aqpcd_2) } le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : No: () le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 21, which took 0.296181 s (model generation: 0.272320, model checking: 0.023861): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True leq(s(z), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), s(s(z))) <= True max(s(z), s(s(z)), 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 le(s(s(z)), s(z)) <= depth(leaf, s(s(z))) False <= depth(leaf, s(s(z))) /\ max(z, s(s(z)), s(z)) False <= depth(leaf, s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) False <= depth(node(a, leaf, leaf), s(s(z))) False <= depth(node(a, leaf, node(a, leaf, leaf)), s(z)) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) False <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) depth(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), leaf), s(s(z))) <= depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ max(s(s(s(s(s(z))))), z, s(z)) False <= le(s(s(z)), s(s(z))) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= max(s(s(z)), z, s(z)) depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= max(z, s(s(z)), s(z)) depth(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z))) } Current best model: |_ name: None depth -> [ depth : { _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) depth(leaf, z) <= True depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ depth(x_0_2, x_1_0) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ depth(x_0_1, x_1_0) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; max -> [ max : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) max(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : Yes: { _qla -> s(z) ; _rla -> s(z) ; _sla -> s(s(_zzucd_0)) ; t1 -> node(_uzpcd_0, leaf, leaf) ; t2 -> node(_vzpcd_0, leaf, leaf) } le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : Yes: { _wla -> s(s(s(z))) ; _xla -> s(s(s(z))) ; t1 -> node(_yzpcd_0, leaf, node(_mfqcd_0, node(_buqcd_0, leaf, leaf), leaf)) ; t2 -> node(_ofqcd_0, node(_cuqcd_0, leaf, leaf), leaf) } le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 22, which took 0.422698 s (model generation: 0.417229, model checking: 0.005469): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True leq(s(z), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), s(s(z))) <= True max(s(z), s(s(z)), 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 le(s(s(z)), s(z)) <= depth(leaf, s(s(z))) False <= depth(leaf, s(s(z))) /\ max(z, s(s(z)), s(z)) False <= depth(leaf, s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) False <= depth(node(a, leaf, leaf), s(s(z))) False <= depth(node(a, leaf, node(a, leaf, leaf)), s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) /\ depth(node(a, node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) False <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) depth(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), leaf), s(s(z))) <= depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ max(s(s(s(s(s(z))))), z, s(z)) False <= le(s(s(z)), s(s(z))) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= max(s(s(z)), z, s(z)) depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max(s(z), s(z), s(s(z))) depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= max(z, s(s(z)), s(z)) depth(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z))) } Current best model: |_ name: None depth -> [ depth : { _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_1, x_1_0) /\ _r_2(x_0_2, x_1_0) _r_2(leaf, s(x_1_0)) <= True _r_2(leaf, z) <= True depth(leaf, z) <= True depth(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) depth(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) depth(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) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; max -> [ max : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True max(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max(s(x_0_0), z, s(x_2_0)) <= leq(x_0_0, x_2_0) max(z, s(x_1_0), s(x_2_0)) <= leq(x_1_0, x_2_0) max(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : Yes: { _qla -> s(s(z)) ; _rla -> s(z) ; _sla -> s(z) ; t1 -> node(_ylvcd_0, leaf, node(_cawcd_0, leaf, leaf)) ; t2 -> node(_zlvcd_0, leaf, leaf) } le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : No: () le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 23, which took 0.376082 s (model generation: 0.346949, model checking: 0.029133): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True leq(s(z), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), s(s(z))) <= True max(s(z), s(s(z)), 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 le(s(s(z)), s(z)) <= depth(leaf, s(s(z))) False <= depth(leaf, s(s(z))) /\ max(z, s(s(z)), s(z)) False <= depth(leaf, s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) False <= depth(node(a, leaf, leaf), s(s(z))) False <= depth(node(a, leaf, node(a, leaf, leaf)), s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) /\ depth(node(a, node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) False <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) depth(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), leaf), s(s(z))) <= depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ max(s(s(s(s(s(z))))), z, s(z)) False <= le(s(s(z)), s(s(z))) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= max(s(s(z)), s(z), s(z)) False <= max(s(s(z)), z, s(z)) depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max(s(z), s(z), s(s(z))) depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= max(z, s(s(z)), s(z)) depth(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z))) } Current best model: |_ name: None depth -> [ depth : { _r_2(leaf, s(x_1_0)) <= True _r_2(leaf, z) <= True depth(leaf, z) <= True depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ depth(x_0_2, x_1_0) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ depth(x_0_1, x_1_0) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= depth(x_0_1, x_1_0) /\ depth(x_0_2, x_1_0) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; max -> [ max : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True max(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) max(s(x_0_0), s(x_1_0), s(x_2_0)) <= le(x_0_0, x_1_0) max(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) max(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : Yes: { _qla -> s(z) ; _rla -> s(s(z)) ; _sla -> s(s(_gvbdd_0)) ; t1 -> node(_dlxcd_0, leaf, leaf) ; t2 -> node(_elxcd_0, node(_ljadd_0, leaf, leaf), node(_ljadd_0, leaf, leaf)) } le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : No: () le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 24, which took 0.621028 s (model generation: 0.617451, model checking: 0.003577): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(s(z)))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True leq(s(z), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), s(s(z))) <= True max(s(z), s(s(z)), 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 le(s(s(z)), s(z)) <= depth(leaf, s(s(z))) False <= depth(leaf, s(s(z))) /\ max(z, s(s(z)), s(z)) False <= depth(leaf, s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) False <= depth(node(a, leaf, leaf), s(s(z))) False <= depth(node(a, leaf, node(a, leaf, leaf)), s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) /\ depth(node(a, node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) False <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) depth(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), leaf), s(s(z))) <= depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ max(s(s(s(s(s(z))))), z, s(z)) False <= le(s(s(z)), s(s(z))) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= max(s(s(z)), s(z), s(z)) False <= max(s(s(z)), z, s(z)) depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max(s(z), s(z), s(s(z))) depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= max(z, s(s(z)), s(z)) depth(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z))) } Current best model: |_ name: None depth -> [ depth : { _r_1(leaf, s(x_1_0)) <= True _r_1(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) /\ _r_1(x_0_2, x_1_0) depth(leaf, z) <= True depth(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) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ depth(x_0_2, x_1_0) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; max -> [ max : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True max(s(x_0_0), s(x_1_0), s(x_2_0)) <= leq(x_0_0, x_2_0) max(s(x_0_0), z, s(x_2_0)) <= leq(x_0_0, x_2_0) max(z, s(x_1_0), s(x_2_0)) <= leq(x_1_0, x_2_0) max(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : Yes: { _qla -> s(s(z)) ; _rla -> s(s(z)) ; _sla -> s(s(s(_amcdd_0))) ; t1 -> node(_chcdd_0, node(_qlcdd_0, leaf, leaf), node(_zlcdd_0, _zlcdd_1, _zlcdd_2)) ; t2 -> node(_dhcdd_0, node(_wjcdd_0, leaf, leaf), _dhcdd_2) } le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : No: () le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 25, which took 0.975235 s (model generation: 0.970190, model checking: 0.005045): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(s(z)))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True leq(s(z), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), s(s(z))) <= True max(s(z), s(s(z)), 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 le(s(s(z)), s(z)) <= depth(leaf, s(s(z))) False <= depth(leaf, s(s(z))) /\ max(z, s(s(z)), s(z)) False <= depth(leaf, s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) False <= depth(node(a, leaf, leaf), s(s(z))) False <= depth(node(a, leaf, node(a, leaf, leaf)), s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) /\ depth(node(a, node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) False <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) depth(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), leaf), s(s(z))) <= depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ max(s(s(s(s(s(z))))), z, s(z)) False <= le(s(s(z)), s(s(z))) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) depth(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)), s(s(s(s(z))))) <= max(s(s(z)), s(s(z)), s(s(s(z)))) False <= max(s(s(z)), s(z), s(z)) False <= max(s(s(z)), z, s(z)) depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max(s(z), s(z), s(s(z))) depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= max(z, s(s(z)), s(z)) depth(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z))) } Current best model: |_ name: None depth -> [ depth : { _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) _r_2(leaf, s(x_1_0)) <= True _r_2(leaf, z) <= True depth(leaf, z) <= True depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) depth(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) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= depth(x_0_1, x_1_0) /\ depth(x_0_2, x_1_0) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; max -> [ max : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True max(s(x_0_0), s(x_1_0), s(x_2_0)) <= leq(x_0_0, x_2_0) max(s(x_0_0), z, s(x_2_0)) <= leq(x_0_0, x_2_0) max(z, s(x_1_0), s(x_2_0)) <= leq(x_1_0, x_2_0) max(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : Yes: { _qla -> z ; _rla -> s(s(z)) ; _sla -> s(s(z)) ; t1 -> leaf ; t2 -> node(_smcdd_0, node(_cjddd_0, leaf, leaf), node(_ulddd_0, _ulddd_1, _ulddd_2)) } le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : Yes: { _wla -> s(s(s(z))) ; _xla -> s(s(s(z))) ; t1 -> node(_zycdd_0, node(_ebddd_0, leaf, leaf), _zycdd_2) ; t2 -> node(_gbddd_0, node(_igddd_0, leaf, leaf), _gbddd_2) } le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 26, which took 1.091347 s (model generation: 0.542864, model checking: 0.548483): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(s(z)))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True leq(s(z), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), s(s(z))) <= True max(s(z), s(s(z)), 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 le(s(s(z)), s(z)) <= depth(leaf, s(s(z))) False <= depth(leaf, s(s(z))) /\ max(z, s(s(z)), s(z)) False <= depth(leaf, s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) False <= depth(node(a, leaf, leaf), s(s(z))) False <= depth(node(a, leaf, node(a, leaf, leaf)), s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) /\ depth(node(a, node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ depth(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) False <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) depth(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), leaf), s(s(z))) <= depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ max(s(s(s(s(s(z))))), z, s(z)) False <= le(s(s(z)), s(s(z))) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) depth(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)), s(s(s(s(z))))) <= max(s(s(z)), s(s(z)), s(s(s(z)))) False <= max(s(s(z)), s(z), s(z)) False <= max(s(s(z)), z, s(z)) depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max(s(z), s(z), s(s(z))) depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) depth(node(a, leaf, node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(s(z)))) <= max(z, s(s(z)), s(s(z))) depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= max(z, s(s(z)), s(z)) depth(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z))) } Current best model: |_ name: None depth -> [ depth : { _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) depth(leaf, z) <= True depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ depth(x_0_2, x_1_0) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ depth(x_0_1, x_1_0) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; max -> [ max : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True max(s(x_0_0), s(x_1_0), s(x_2_0)) <= max(x_0_0, x_1_0, x_2_0) max(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) max(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : Yes: { _qla -> z ; _rla -> s(s(z)) ; _sla -> s(s(s(_djhdd_0))) ; t1 -> leaf ; t2 -> node(_pnddd_0, leaf, node(_agedd_0, leaf, leaf)) } le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 27, which took 1.500480 s (model generation: 1.488077, model checking: 0.012403): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(s(z)))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True leq(s(z), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), s(s(z))) <= True max(s(z), s(s(z)), 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 le(s(s(z)), s(z)) <= depth(leaf, s(s(z))) False <= depth(leaf, s(s(z))) /\ max(z, s(s(z)), s(z)) False <= depth(leaf, s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) False <= depth(node(a, leaf, leaf), s(s(z))) False <= depth(node(a, leaf, node(a, leaf, leaf)), s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) /\ depth(node(a, node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ depth(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) False <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) depth(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), leaf), s(s(z))) <= depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ max(s(s(s(s(s(z))))), z, s(z)) False <= le(s(s(z)), s(s(z))) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) depth(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)), s(s(s(s(z))))) <= max(s(s(z)), s(s(z)), s(s(s(z)))) False <= max(s(s(z)), s(z), s(z)) False <= max(s(s(z)), z, s(z)) depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max(s(z), s(z), s(s(z))) depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) depth(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= max(z, s(s(z)), s(s(s(z)))) depth(node(a, leaf, node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(s(z)))) <= max(z, s(s(z)), s(s(z))) depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= max(z, s(s(z)), s(z)) depth(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z))) } Current best model: |_ name: None depth -> [ depth : { _r_1(leaf, s(x_1_0)) <= True _r_1(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) /\ _r_1(x_0_2, 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) depth(leaf, z) <= True depth(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) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ depth(x_0_1, x_1_0) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; max -> [ max : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True max(s(x_0_0), s(x_1_0), s(x_2_0)) <= leq(x_0_0, x_2_0) max(s(x_0_0), z, s(x_2_0)) <= leq(x_0_0, x_2_0) max(z, s(x_1_0), s(x_2_0)) <= leq(x_1_0, x_2_0) max(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : Yes: { _qla -> z ; _rla -> s(s(z)) ; _sla -> s(s(z)) ; t1 -> leaf ; t2 -> node(_zadgd_0, node(_oxdgd_0, leaf, leaf), node(_xkfgd_0, node(_hlfgd_0, _hlfgd_1, _hlfgd_2), node(_jlfgd_0, _jlfgd_1, _jlfgd_2))) } le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : Yes: { _wla -> s(s(s(s(z)))) ; _xla -> s(s(s(s(z)))) ; t1 -> node(_gldgd_0, node(_pmdgd_0, _pmdgd_1, node(_kqdgd_0, leaf, leaf)), node(_iqdgd_0, _iqdgd_1, node(_updgd_0, leaf, leaf))) } le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 28, which took 2.616176 s (model generation: 2.080324, model checking: 0.535852): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(s(z)))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True leq(s(z), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), s(s(z))) <= True max(s(z), s(s(z)), 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 le(s(s(z)), s(z)) <= depth(leaf, s(s(z))) False <= depth(leaf, s(s(z))) /\ max(z, s(s(z)), s(z)) False <= depth(leaf, s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) False <= depth(node(a, leaf, leaf), s(s(z))) False <= depth(node(a, leaf, node(a, leaf, leaf)), s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) /\ depth(node(a, node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ depth(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) depth(node(a, leaf, node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))), s(s(s(z)))) <= depth(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(z))) /\ max(z, s(s(z)), s(s(z))) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) le(s(s(s(s(z)))), s(s(s(s(z))))) <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) /\ depth(node(a, node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), leaf), s(s(s(s(z))))) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) False <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) depth(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), leaf), s(s(z))) <= depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ max(s(s(s(s(s(z))))), z, s(z)) False <= le(s(s(z)), s(s(z))) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) depth(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)), s(s(s(s(z))))) <= max(s(s(z)), s(s(z)), s(s(s(z)))) False <= max(s(s(z)), s(z), s(z)) False <= max(s(s(z)), z, s(z)) depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max(s(z), s(z), s(s(z))) depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) depth(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= max(z, s(s(z)), s(s(s(z)))) depth(node(a, leaf, node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(s(z)))) <= max(z, s(s(z)), s(s(z))) depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= max(z, s(s(z)), s(z)) depth(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z))) } Current best model: |_ name: None depth -> [ depth : { _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) depth(leaf, z) <= True depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ depth(x_0_2, x_1_0) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ depth(x_0_1, x_1_0) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; max -> [ max : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(z, z) <= True le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True max(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) max(s(x_0_0), s(x_1_0), s(x_2_0)) <= le(x_0_0, x_1_0) max(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) max(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : Yes: { _qla -> s(z) ; _rla -> s(s(z)) ; _sla -> s(s(s(_irlgd_0))) ; t1 -> node(_ytfgd_0, leaf, leaf) ; t2 -> node(_ztfgd_0, leaf, node(_otigd_0, leaf, leaf)) } le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () ------------------------------------------- Step 29, which took 3.206677 s (model generation: 3.202966, model checking: 0.003711): Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(s(z)))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True leq(s(z), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), s(s(z))) <= True max(s(z), s(s(z)), 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 le(s(s(z)), s(z)) <= depth(leaf, s(s(z))) False <= depth(leaf, s(s(z))) /\ max(z, s(s(z)), s(z)) False <= depth(leaf, s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) False <= depth(node(a, leaf, leaf), s(s(z))) False <= depth(node(a, leaf, node(a, leaf, leaf)), s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) /\ depth(node(a, node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ depth(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) depth(node(a, leaf, node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))), s(s(s(z)))) <= depth(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(z))) /\ max(z, s(s(z)), s(s(z))) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) le(s(s(s(s(z)))), s(s(s(s(z))))) <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) /\ depth(node(a, node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), leaf), s(s(s(s(z))))) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) False <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) depth(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), leaf), s(s(z))) <= depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ max(s(s(s(s(s(z))))), z, s(z)) False <= le(s(s(z)), s(s(z))) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) depth(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)), s(s(s(s(z))))) <= max(s(s(z)), s(s(z)), s(s(s(z)))) False <= max(s(s(z)), s(z), s(z)) False <= max(s(s(z)), z, s(z)) depth(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= max(s(z), s(s(z)), s(s(s(z)))) depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max(s(z), s(z), s(s(z))) depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) depth(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= max(z, s(s(z)), s(s(s(z)))) depth(node(a, leaf, node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(s(z)))) <= max(z, s(s(z)), s(s(z))) depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= max(z, s(s(z)), s(z)) depth(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z))) } Current best model: |_ name: None depth -> [ depth : { _r_1(leaf, s(x_1_0)) <= True _r_1(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) /\ _r_1(x_0_2, x_1_0) depth(leaf, z) <= True depth(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) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ depth(x_0_2, x_1_0) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; max -> [ max : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True max(s(x_0_0), s(x_1_0), s(x_2_0)) <= max(x_0_0, x_1_0, x_2_0) max(s(x_0_0), z, s(x_2_0)) <= leq(x_0_0, x_2_0) max(z, s(x_1_0), s(x_2_0)) <= leq(x_1_0, x_2_0) max(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: depth(leaf, z) <= True : No: () leq(n, m) \/ max(n, m, n) <= True : No: () leq(z, n2) <= True : No: () depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) : Yes: { _qla -> s(s(z)) ; _rla -> z ; _sla -> s(s(z)) ; t1 -> node(_cwejd_0, node(_lbfjd_0, leaf, leaf), node(_kefjd_0, _kefjd_1, _kefjd_2)) ; t2 -> leaf } le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) : No: () le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () max(n, m, m) <= leq(n, m) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () Total time: 60.466296 Learner time: 12.273878 Teacher time: 1.186136 Reasons for stopping: Maybe: timeout during teacher: { depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> out of time le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> out of time }Last solver state: Clauses: { depth(leaf, z) <= True -> 0 leq(n, m) \/ max(n, m, n) <= True -> 0 leq(z, n2) <= True -> 0 depth(node(e, t1, t2), s(_sla)) <= depth(t1, _qla) /\ depth(t2, _rla) /\ max(_qla, _rla, _sla) -> 0 le(_wla, _xla) <= depth(t1, _wla) /\ depth(node(e, t1, t2), _xla) -> 0 le(s(nn1), s(nn2)) <= le(nn1, nn2) -> 0 le(nn1, nn2) <= le(s(nn1), s(nn2)) -> 0 False <= le(s(nn1), z) -> 0 False <= le(z, z) -> 0 max(n, m, m) <= leq(n, m) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 } Accumulated learning constraints: { depth(leaf, z) <= True depth(node(a, leaf, leaf), s(z)) <= True depth(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) <= True depth(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(s(z)))) <= True le(s(z), s(s(z))) <= True le(z, s(z)) <= True leq(s(s(z)), s(s(z))) <= True leq(s(s(z)), z) \/ max(s(s(z)), z, s(s(z))) <= True leq(s(z), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, s(z)) <= True leq(z, z) <= True max(s(s(z)), s(z), s(s(z))) <= True max(s(z), s(s(z)), 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 le(s(s(z)), s(z)) <= depth(leaf, s(s(z))) False <= depth(leaf, s(s(z))) /\ max(z, s(s(z)), s(z)) False <= depth(leaf, s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, leaf), s(s(s(z)))) /\ depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) False <= depth(node(a, leaf, leaf), s(s(z))) False <= depth(node(a, leaf, node(a, leaf, leaf)), s(z)) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) /\ depth(node(a, node(a, leaf, node(a, node(a, leaf, leaf), leaf)), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) le(s(s(s(z))), s(s(s(z)))) <= depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ depth(node(a, node(a, node(a, leaf, leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(s(s(z)))) False <= depth(node(a, node(a, leaf, leaf), leaf), s(z)) depth(node(a, leaf, node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf)))), s(s(s(z)))) <= depth(node(a, node(a, leaf, leaf), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(z))) /\ max(z, s(s(z)), s(s(z))) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) False <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) le(s(s(s(s(z)))), s(s(s(s(z))))) <= depth(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) /\ depth(node(a, node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), leaf), s(s(s(s(z))))) depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), node(a, leaf, leaf)), s(s(z))) <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(s(z)))) /\ max(s(s(s(z))), s(z), s(z)) False <= depth(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) depth(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), leaf), s(s(z))) <= depth(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ max(s(s(s(s(s(z))))), z, s(z)) False <= le(s(s(z)), s(s(z))) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) depth(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)), s(s(s(s(z))))) <= max(s(s(z)), s(s(z)), s(s(s(z)))) False <= max(s(s(z)), s(z), s(z)) depth(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), leaf), s(s(s(z)))) <= max(s(s(z)), z, s(s(z))) False <= max(s(s(z)), z, s(z)) depth(node(a, node(a, leaf, leaf), node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= max(s(z), s(s(z)), s(s(s(z)))) depth(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= max(s(z), s(z), s(s(z))) depth(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= max(s(z), z, s(s(z))) depth(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= max(z, s(s(z)), s(s(s(z)))) depth(node(a, leaf, node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(s(z)))) <= max(z, s(s(z)), s(s(z))) depth(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= max(z, s(s(z)), s(z)) depth(node(a, leaf, node(a, leaf, leaf)), s(s(s(z)))) <= max(z, s(z), s(s(z))) } Current best model: |_ name: None depth -> [ depth : { _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) depth(leaf, z) <= True depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ depth(x_0_2, x_1_0) depth(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) /\ depth(x_0_1, x_1_0) } ] ; le -> [ le : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; max -> [ max : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(z, z) <= True max(s(x_0_0), s(x_1_0), s(x_2_0)) <= max(x_0_0, x_1_0, x_2_0) max(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) max(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _|