Solving ../../benchmarks/smtlib/true/tree_size_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) } ) (plus, F: { plus(n, z, n) <= True plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) } eq_nat(_in, _jn) <= plus(_gn, _hn, _in) /\ plus(_gn, _hn, _jn) ) (numnodes, F: { numnodes(leaf, z) <= True numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) } eq_nat(_on, _pn) <= numnodes(_nn, _on) /\ numnodes(_nn, _pn) ) } properties: { le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) } over-approximation: {numnodes, plus} under-approximation: {le} Clause system for inference is: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Solving took 60.924616 seconds. Maybe: timeout during learnerLast solver state: Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, s(z)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= True plus(s(s(z)), z, s(s(z))) <= True plus(s(z), s(z), s(s(z))) <= True plus(s(z), z, s(z)) <= True plus(z, s(s(z)), s(s(z))) <= True plus(z, s(z), s(z)) <= True plus(z, z, z) <= True False <= le(s(s(z)), s(s(z))) False <= le(s(s(z)), s(z)) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= numnodes(leaf, s(s(z))) False <= numnodes(leaf, s(z)) False <= numnodes(node(a, leaf, leaf), s(s(z))) False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z)) numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ plus(s(z), s(z), s(z)) numnodes(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ plus(s(s(s(s(s(z))))), s(s(s(z))), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), leaf), z) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), z) False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(z))) numnodes(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ plus(s(s(z)), s(s(z)), s(z)) numnodes(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), z) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(z)) False <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) numnodes(node(a, node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), leaf), s(s(z))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(s(z)))) /\ plus(s(s(s(z))), z, s(z)) le(s(s(s(z))), s(s(z))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) /\ numnodes(node(a, node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), node(a, leaf, leaf)), s(s(z))) False <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) plus(s(z), s(s(z)), s(s(z))) <= plus(s(z), s(z), s(z)) numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= plus(s(z), z, s(s(z))) numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z)))) numnodes(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= plus(z, s(s(z)), s(z)) } Current best model: |_ name: None 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 } ] ; numnodes -> [ numnodes : { _r_2(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_2, x_1_0) _r_3(leaf, s(x_1_0)) <= True _r_3(leaf, z) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_2, x_1_0) /\ numnodes(x_0_1, x_1_0) } ] ; plus -> [ plus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) plus(z, s(x_1_0), s(x_2_0)) <= True plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.006595 s (model generation: 0.006525, model checking: 0.000070): Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { } Current best model: |_ name: None le -> [ le : { } ] ; numnodes -> [ numnodes : { } ] ; plus -> [ plus : { } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: numnodes(leaf, z) <= True : Yes: { } plus(n, z, n) <= True : Yes: { n -> z } 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: () numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) : No: () le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) : No: () plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) : No: () ------------------------------------------- Step 1, which took 0.006333 s (model generation: 0.006205, model checking: 0.000128): Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { numnodes(leaf, z) <= True plus(z, z, z) <= True } Current best model: |_ name: None le -> [ le : { } ] ; numnodes -> [ numnodes : { numnodes(leaf, z) <= True } ] ; plus -> [ plus : { plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : Yes: { n -> s(_xdbqw_0) } 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: () numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) : Yes: { _kn -> z ; _ln -> z ; _mn -> z ; t1 -> leaf ; t2 -> leaf } le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) : No: () plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) : Yes: { _fn -> z ; mm -> z ; n -> z } ------------------------------------------- Step 2, which took 0.008624 s (model generation: 0.008337, model checking: 0.000287): Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True plus(s(z), z, s(z)) <= True plus(z, s(z), s(z)) <= True plus(z, z, z) <= True } Current best model: |_ name: None le -> [ le : { } ] ; numnodes -> [ numnodes : { numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True } ] ; plus -> [ plus : { plus(s(x_0_0), z, s(x_2_0)) <= True plus(z, s(x_1_0), s(x_2_0)) <= True plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : 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: () numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) : No: () le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) : Yes: { _qn -> z ; _rn -> s(_kebqw_0) ; t1 -> leaf } plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) : Yes: { _fn -> s(_mebqw_0) ; mm -> z ; n -> s(_oebqw_0) } ------------------------------------------- Step 3, which took 0.015309 s (model generation: 0.015123, model checking: 0.000186): Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { le(z, s(z)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True plus(s(z), s(z), s(s(z))) <= True plus(s(z), z, s(z)) <= True plus(z, s(z), s(z)) <= True plus(z, z, z) <= True } Current best model: |_ name: None le -> [ le : { le(z, s(x_1_0)) <= True } ] ; numnodes -> [ numnodes : { numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True } ] ; plus -> [ plus : { plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True plus(s(x_0_0), z, s(x_2_0)) <= True plus(z, s(x_1_0), s(x_2_0)) <= True plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () le(s(nn1), s(nn2)) <= le(nn1, nn2) : Yes: { nn1 -> z ; nn2 -> s(_qebqw_0) } le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) : No: () le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) : Yes: { _qn -> s(_rebqw_0) ; _rn -> s(_sebqw_0) ; t1 -> node(_tebqw_0, _tebqw_1, _tebqw_2) } plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) : No: () ------------------------------------------- Step 4, which took 0.012023 s (model generation: 0.011950, model checking: 0.000073): Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, s(z)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True plus(s(z), s(z), s(s(z))) <= True plus(s(z), z, s(z)) <= True plus(z, s(z), s(z)) <= True plus(z, z, z) <= True le(s(z), s(z)) <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) } Current best model: |_ name: None le -> [ le : { le(s(x_0_0), s(x_1_0)) <= True le(z, s(x_1_0)) <= True } ] ; numnodes -> [ numnodes : { numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True } ] ; plus -> [ plus : { plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True plus(s(x_0_0), z, s(x_2_0)) <= True plus(z, s(x_1_0), s(x_2_0)) <= True plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : 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: () numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) : No: () le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) : No: () plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) : No: () ------------------------------------------- Step 5, which took 0.009493 s (model generation: 0.009427, model checking: 0.000066): Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, s(z)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True plus(s(z), s(z), s(s(z))) <= True plus(s(z), z, s(z)) <= True plus(z, s(z), s(z)) <= True plus(z, z, z) <= True le(z, z) <= le(s(z), s(z)) le(s(z), s(z)) <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) } Current best model: |_ name: None le -> [ le : { le(s(x_0_0), s(x_1_0)) <= True le(z, s(x_1_0)) <= True le(z, z) <= True } ] ; numnodes -> [ numnodes : { numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True } ] ; plus -> [ plus : { plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True plus(s(x_0_0), z, s(x_2_0)) <= True plus(z, s(x_1_0), s(x_2_0)) <= True plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : Yes: { nn1 -> s(_yebqw_0) ; nn2 -> z } False <= le(s(nn1), z) : No: () False <= le(z, z) : Yes: { } numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) : No: () le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) : No: () plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) : No: () ------------------------------------------- Step 6, which took 0.009778 s (model generation: 0.009505, model checking: 0.000273): Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, s(z)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True plus(s(z), s(z), s(s(z))) <= True plus(s(z), z, s(z)) <= True plus(z, s(z), s(z)) <= True plus(z, z, z) <= True le(s(z), z) <= le(s(s(z)), s(z)) False <= le(s(z), s(z)) False <= le(z, z) False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) } Current best model: |_ name: None 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 } ] ; numnodes -> [ numnodes : { numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0) } ] ; plus -> [ plus : { plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True plus(s(x_0_0), z, s(x_2_0)) <= True plus(z, s(x_1_0), s(x_2_0)) <= True plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () 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: () numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) : Yes: { _kn -> z ; _ln -> s(z) ; _mn -> s(_rfbqw_0) ; t1 -> leaf ; t2 -> node(_tfbqw_0, leaf, _tfbqw_2) } le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) : No: () plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) : No: () ------------------------------------------- Step 7, which took 0.010617 s (model generation: 0.010282, model checking: 0.000335): Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, s(z)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True plus(s(z), s(z), s(s(z))) <= True plus(s(z), z, s(z)) <= True plus(z, s(z), s(z)) <= True plus(z, z, z) <= True False <= le(s(s(z)), s(z)) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) } Current best model: |_ name: None 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 } ] ; numnodes -> [ numnodes : { numnodes(leaf, s(x_1_0)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0) } ] ; plus -> [ plus : { plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True plus(s(x_0_0), z, s(x_2_0)) <= True plus(z, s(x_1_0), s(x_2_0)) <= True plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : 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: () numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) : Yes: { _kn -> s(s(s(z))) ; _ln -> s(_aibqw_0) ; _mn -> s(z) ; t1 -> node(_cibqw_0, node(_kjbqw_0, node(_bkbqw_0, leaf, _bkbqw_2), _kjbqw_2), _cibqw_2) ; t2 -> leaf } le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) : Yes: { _qn -> s(z) ; _rn -> s(z) ; t1 -> leaf } plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) : No: () ------------------------------------------- Step 8, which took 0.015719 s (model generation: 0.015521, model checking: 0.000198): Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, s(z)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True plus(s(z), s(z), s(s(z))) <= True plus(s(z), z, s(z)) <= True plus(z, s(z), s(z)) <= True plus(z, z, z) <= True False <= le(s(s(z)), s(z)) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= numnodes(leaf, s(z)) False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) } Current best model: |_ name: None 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 } ] ; numnodes -> [ numnodes : { _r_1(leaf) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1) } ] ; plus -> [ plus : { plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True plus(s(x_0_0), z, s(x_2_0)) <= True plus(z, s(x_1_0), s(x_2_0)) <= True plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : 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: () numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) : Yes: { _kn -> s(_ykbqw_0) ; _ln -> z ; _mn -> s(_albqw_0) ; t1 -> node(_blbqw_0, leaf, _blbqw_2) ; t2 -> leaf } le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) : No: () plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) : No: () ------------------------------------------- Step 9, which took 0.017300 s (model generation: 0.017050, model checking: 0.000250): Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, s(z)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True plus(s(z), s(z), s(s(z))) <= True plus(s(z), z, s(z)) <= True plus(z, s(z), s(z)) <= True plus(z, z, z) <= True False <= le(s(s(z)), s(z)) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= numnodes(leaf, s(z)) False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) } Current best model: |_ name: None 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 } ] ; numnodes -> [ numnodes : { _r_1(leaf, s(x_1_0)) <= True _r_1(leaf, z) <= True _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) } ] ; plus -> [ plus : { plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True plus(s(x_0_0), z, s(x_2_0)) <= True plus(z, s(x_1_0), s(x_2_0)) <= True plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : 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: () numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) : No: () le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) : Yes: { _qn -> s(s(z)) ; _rn -> s(s(z)) ; t1 -> node(_zmbqw_0, node(_jnbqw_0, _jnbqw_1, _jnbqw_2), _zmbqw_2) } plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) : No: () ------------------------------------------- Step 10, which took 0.020794 s (model generation: 0.020349, model checking: 0.000445): Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, s(z)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True plus(s(z), s(z), s(s(z))) <= True plus(s(z), z, s(z)) <= True plus(z, s(z), s(z)) <= True plus(z, z, z) <= True False <= le(s(s(z)), s(z)) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= numnodes(leaf, s(z)) False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) le(s(s(z)), s(s(z))) <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) } Current best model: |_ name: None 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 } ] ; numnodes -> [ numnodes : { _r_1(s(x_0_0)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0) } ] ; plus -> [ plus : { plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True plus(s(x_0_0), z, s(x_2_0)) <= True plus(z, s(x_1_0), s(x_2_0)) <= True plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () le(nn1, nn2) <= le(s(nn1), s(nn2)) : Yes: { nn1 -> s(_wnbqw_0) ; nn2 -> s(z) } False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) : No: () le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) : No: () plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) : No: () ------------------------------------------- Step 11, which took 0.019441 s (model generation: 0.018881, model checking: 0.000560): Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, s(z)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True plus(s(z), s(z), s(s(z))) <= True plus(s(z), z, s(z)) <= True plus(z, s(z), s(z)) <= True plus(z, z, z) <= True False <= le(s(s(z)), s(s(z))) False <= le(s(s(z)), s(z)) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= numnodes(leaf, s(z)) False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) False <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) } Current best model: |_ name: None 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 } ] ; numnodes -> [ numnodes : { _r_1(leaf, s(x_1_0)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0) } ] ; plus -> [ plus : { plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True plus(s(x_0_0), z, s(x_2_0)) <= True plus(z, s(x_1_0), s(x_2_0)) <= True plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : 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: () numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) : Yes: { _kn -> s(s(s(s(s(_ftbqw_0))))) ; _ln -> s(s(s(_ftbqw_0))) ; _mn -> s(z) ; t1 -> node(_qsbqw_0, node(_cubqw_0, node(_vubqw_0, node(_otbqw_0, leaf, _otbqw_2), _vubqw_2), _cubqw_2), _qsbqw_2) ; t2 -> node(_rsbqw_0, node(_otbqw_0, leaf, _otbqw_2), _rsbqw_2) } le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) : Yes: { _qn -> s(s(z)) ; _rn -> s(s(z)) ; t1 -> node(_xsbqw_0, leaf, _xsbqw_2) } plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) : No: () ------------------------------------------- Step 12, which took 0.032940 s (model generation: 0.032514, model checking: 0.000426): Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, s(z)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True plus(s(z), s(z), s(s(z))) <= True plus(s(z), z, s(z)) <= True plus(z, s(z), s(z)) <= True plus(z, z, z) <= True False <= le(s(s(z)), s(s(z))) False <= le(s(s(z)), s(z)) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= numnodes(leaf, s(z)) False <= numnodes(node(a, leaf, leaf), s(s(z))) numnodes(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ plus(s(s(s(s(s(z))))), s(s(s(z))), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) False <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) } Current best model: |_ name: None 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 } ] ; numnodes -> [ numnodes : { _r_1(node(x_0_0, x_0_1, x_0_2)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0) } ] ; plus -> [ plus : { plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True plus(s(x_0_0), z, s(x_2_0)) <= True plus(z, s(x_1_0), s(x_2_0)) <= True plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : 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: () numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) : Yes: { _kn -> s(z) ; _ln -> z ; _mn -> s(s(_cybqw_0)) ; t1 -> node(_pwbqw_0, leaf, leaf) ; t2 -> leaf } le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) : Yes: { _qn -> s(z) ; _rn -> s(z) ; t1 -> node(_dxbqw_0, _dxbqw_1, node(_nxbqw_0, _nxbqw_1, _nxbqw_2)) ; t2 -> node(_nxbqw_0, _nxbqw_1, _nxbqw_2) } plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) : No: () ------------------------------------------- Step 13, which took 0.040265 s (model generation: 0.039264, model checking: 0.001001): Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, s(z)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True plus(s(z), s(z), s(s(z))) <= True plus(s(z), z, s(z)) <= True plus(z, s(z), s(z)) <= True plus(z, z, z) <= True False <= le(s(s(z)), s(s(z))) False <= le(s(s(z)), s(z)) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= numnodes(leaf, s(z)) False <= numnodes(node(a, leaf, leaf), s(s(z))) False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z)) numnodes(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ plus(s(s(s(s(s(z))))), s(s(s(z))), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) False <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= plus(s(z), z, s(s(z))) } Current best model: |_ name: None 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 } ] ; numnodes -> [ numnodes : { _r_1(s(x_0_0)) <= True numnodes(leaf, s(x_1_0)) <= _r_1(x_1_0) numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_1_0) /\ numnodes(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0) } ] ; plus -> [ plus : { _r_1(s(x_0_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_2_0) plus(s(x_0_0), z, s(x_2_0)) <= True plus(z, s(x_1_0), s(x_2_0)) <= True plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : 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: () numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) : Yes: { _kn -> z ; _ln -> s(s(_pfcqw_0)) ; _mn -> s(z) ; t1 -> leaf ; t2 -> leaf } le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) : Yes: { _qn -> s(s(_sfcqw_0)) ; _rn -> s(z) ; t1 -> leaf } plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) : No: () ------------------------------------------- Step 14, which took 0.126502 s (model generation: 0.125761, model checking: 0.000741): Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, s(z)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True plus(s(z), s(z), s(s(z))) <= True plus(s(z), z, s(z)) <= True plus(z, s(z), s(z)) <= True plus(z, z, z) <= True False <= le(s(s(z)), s(s(z))) False <= le(s(s(z)), s(z)) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= numnodes(leaf, s(s(z))) False <= numnodes(leaf, s(z)) False <= numnodes(node(a, leaf, leaf), s(s(z))) False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z)) numnodes(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ plus(s(s(s(s(s(z))))), s(s(s(z))), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) False <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= plus(s(z), z, s(s(z))) } Current best model: |_ name: None 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 } ] ; numnodes -> [ numnodes : { _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(leaf, s(x_1_0)) <= True _r_2(leaf, z) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ _r_2(x_0_1, x_1_0) } ] ; plus -> [ plus : { plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True plus(s(x_0_0), z, s(x_2_0)) <= True plus(z, s(x_1_0), s(x_2_0)) <= True plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : 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: () numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) : Yes: { _kn -> z ; _ln -> s(s(z)) ; _mn -> s(z) ; t1 -> leaf ; t2 -> node(_dhcqw_0, node(_cmcqw_0, leaf, _cmcqw_2), _dhcqw_2) } le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) : Yes: { _qn -> s(s(z)) ; _rn -> s(s(z)) ; t1 -> node(_okcqw_0, leaf, node(_zkcqw_0, leaf, _zkcqw_2)) } plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) : No: () ------------------------------------------- Step 15, which took 0.127256 s (model generation: 0.125848, model checking: 0.001408): Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, s(z)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True plus(s(z), s(z), s(s(z))) <= True plus(s(z), z, s(z)) <= True plus(z, s(z), s(z)) <= True plus(z, z, z) <= True False <= le(s(s(z)), s(s(z))) False <= le(s(s(z)), s(z)) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= numnodes(leaf, s(s(z))) False <= numnodes(leaf, s(z)) False <= numnodes(node(a, leaf, leaf), s(s(z))) False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z)) numnodes(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ plus(s(s(s(s(s(z))))), s(s(s(z))), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) False <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) False <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= plus(s(z), z, s(s(z))) numnodes(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= plus(z, s(s(z)), s(z)) } Current best model: |_ name: None 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 } ] ; numnodes -> [ numnodes : { _r_1(leaf, s(x_1_0)) <= True _r_1(leaf, z) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ numnodes(x_0_1, x_1_0) } ] ; plus -> [ plus : { _r_2(z) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True plus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_2_0) plus(z, s(x_1_0), s(x_2_0)) <= _r_2(x_1_0) plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : Yes: { n -> s(s(_rucqw_0)) } 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: () numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) : Yes: { _kn -> s(z) ; _ln -> s(z) ; _mn -> s(s(_zxcqw_0)) ; t1 -> node(_tscqw_0, leaf, leaf) ; t2 -> node(_uscqw_0, leaf, leaf) } le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) : No: () plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) : Yes: { _fn -> s(_lucqw_0) ; mm -> s(z) ; n -> z } ------------------------------------------- Step 16, which took 0.188637 s (model generation: 0.178844, model checking: 0.009793): Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, s(z)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= True plus(s(s(z)), z, s(s(z))) <= True plus(s(z), s(z), s(s(z))) <= True plus(s(z), z, s(z)) <= True plus(z, s(s(z)), s(s(z))) <= True plus(z, s(z), s(z)) <= True plus(z, z, z) <= True False <= le(s(s(z)), s(s(z))) False <= le(s(s(z)), s(z)) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= numnodes(leaf, s(s(z))) False <= numnodes(leaf, s(z)) False <= numnodes(node(a, leaf, leaf), s(s(z))) False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z)) numnodes(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ plus(s(s(s(s(s(z))))), s(s(s(z))), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) False <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) False <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= plus(s(z), z, s(s(z))) numnodes(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= plus(z, s(s(z)), s(z)) } Current best model: |_ name: None 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 } ] ; numnodes -> [ numnodes : { _r_2(node(x_0_0, x_0_1, x_0_2)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1) /\ _r_2(x_0_2) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1) /\ numnodes(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2) /\ numnodes(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0) } ] ; plus -> [ plus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : 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: () numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) : Yes: { _kn -> z ; _ln -> s(s(z)) ; _mn -> s(s(s(_uweqw_0))) ; t1 -> leaf ; t2 -> node(_ksdqw_0, leaf, node(_bffqw_0, leaf, leaf)) } le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) : Yes: { _qn -> s(s(z)) ; _rn -> s(s(z)) ; t1 -> node(_kgeqw_0, node(_eieqw_0, _eieqw_1, _eieqw_2), node(_eieqw_0, _eieqw_1, _eieqw_2)) ; t2 -> node(_iweqw_0, node(_eieqw_0, _eieqw_1, _eieqw_2), node(_eieqw_0, _eieqw_1, _eieqw_2)) } plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) : No: () ------------------------------------------- Step 17, which took 0.277282 s (model generation: 0.248463, model checking: 0.028819): Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, s(z)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= True plus(s(s(z)), z, s(s(z))) <= True plus(s(z), s(z), s(s(z))) <= True plus(s(z), z, s(z)) <= True plus(z, s(s(z)), s(s(z))) <= True plus(z, s(z), s(z)) <= True plus(z, z, z) <= True False <= le(s(s(z)), s(s(z))) False <= le(s(s(z)), s(z)) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= numnodes(leaf, s(s(z))) False <= numnodes(leaf, s(z)) False <= numnodes(node(a, leaf, leaf), s(s(z))) False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z)) numnodes(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ plus(s(s(s(s(s(z))))), s(s(s(z))), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(z))) False <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) False <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= plus(s(z), z, s(s(z))) numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z)))) numnodes(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= plus(z, s(s(z)), s(z)) } Current best model: |_ name: None 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 } ] ; numnodes -> [ numnodes : { _r_1(leaf, s(x_1_0)) <= True _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) _r_2(node(x_0_0, x_0_1, x_0_2)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_2(x_0_1) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_2(x_0_2) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1) /\ numnodes(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= numnodes(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), z) <= _r_2(x_0_1) } ] ; plus -> [ plus : { plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True plus(s(x_0_0), z, s(x_2_0)) <= True plus(z, s(x_1_0), s(x_2_0)) <= True plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : 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: () numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) : Yes: { _kn -> z ; _ln -> s(s(s(_boiqw_0))) ; _mn -> s(z) ; t1 -> node(_agiqw_0, node(_npiqw_0, leaf, _npiqw_2), node(_sakqw_0, _sakqw_1, _sakqw_2)) ; t2 -> node(_bgiqw_0, node(_voiqw_0, leaf, node(_eoiqw_0, _eoiqw_1, _eoiqw_2)), _bgiqw_2) } le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) : Yes: { _qn -> z ; _rn -> z ; t1 -> node(_zniqw_0, node(_foiqw_0, _foiqw_1, _foiqw_2), _zniqw_2) } plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) : No: () ------------------------------------------- Step 18, which took 0.454580 s (model generation: 0.449811, model checking: 0.004769): Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, s(z)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= True plus(s(s(z)), z, s(s(z))) <= True plus(s(z), s(z), s(s(z))) <= True plus(s(z), z, s(z)) <= True plus(z, s(s(z)), s(s(z))) <= True plus(z, s(z), s(z)) <= True plus(z, z, z) <= True False <= le(s(s(z)), s(s(z))) False <= le(s(s(z)), s(z)) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= numnodes(leaf, s(s(z))) False <= numnodes(leaf, s(z)) False <= numnodes(node(a, leaf, leaf), s(s(z))) False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z)) numnodes(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ plus(s(s(s(s(s(z))))), s(s(s(z))), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), leaf), z) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), z) False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(z))) numnodes(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), z) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(z)) False <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) False <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= plus(s(z), z, s(s(z))) numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z)))) numnodes(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= plus(z, s(s(z)), s(z)) } Current best model: |_ name: None 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 } ] ; numnodes -> [ numnodes : { _r_1(leaf, s(x_1_0)) <= _r_2(x_1_0) _r_1(leaf, z) <= True _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_1_0) _r_2(s(x_0_0)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_1(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ _r_2(x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_1_0) /\ numnodes(x_0_1, x_1_0) } ] ; plus -> [ plus : { plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True plus(s(x_0_0), z, s(x_2_0)) <= True plus(z, s(x_1_0), s(x_2_0)) <= True plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : 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: () numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) : Yes: { _kn -> s(s(s(z))) ; _ln -> z ; _mn -> s(z) ; t1 -> node(_whkqw_0, node(_zilqw_0, _zilqw_1, node(_oblqw_0, _oblqw_1, leaf)), node(_xilqw_0, _xilqw_1, _xilqw_2)) ; t2 -> leaf } le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) : Yes: { _qn -> s(s(s(z))) ; _rn -> s(s(z)) ; t1 -> node(_ywkqw_0, node(_uykqw_0, _uykqw_1, node(_kalqw_0, _kalqw_1, leaf)), node(_uykqw_0, _uykqw_1, node(_kalqw_0, _kalqw_1, leaf))) ; t2 -> node(_sykqw_0, _sykqw_1, leaf) } plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) : No: () ------------------------------------------- Step 19, which took 6.499278 s (model generation: 6.498165, model checking: 0.001113): Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, s(z)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= True plus(s(s(z)), z, s(s(z))) <= True plus(s(z), s(z), s(s(z))) <= True plus(s(z), z, s(z)) <= True plus(z, s(s(z)), s(s(z))) <= True plus(z, s(z), s(z)) <= True plus(z, z, z) <= True False <= le(s(s(z)), s(s(z))) False <= le(s(s(z)), s(z)) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= numnodes(leaf, s(s(z))) False <= numnodes(leaf, s(z)) False <= numnodes(node(a, leaf, leaf), s(s(z))) False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z)) numnodes(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ plus(s(s(s(s(s(z))))), s(s(s(z))), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), leaf), z) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), z) False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(z))) numnodes(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), z) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(z)) False <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) numnodes(node(a, node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), leaf), s(s(z))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(s(z)))) /\ plus(s(s(s(z))), z, s(z)) le(s(s(s(z))), s(s(z))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) /\ numnodes(node(a, node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), node(a, leaf, leaf)), s(s(z))) False <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= plus(s(z), z, s(s(z))) numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z)))) numnodes(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= plus(z, s(s(z)), s(z)) } Current best model: |_ name: None 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 } ] ; numnodes -> [ numnodes : { _r_1(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True _r_2(leaf, s(x_1_0)) <= True _r_2(leaf, z) <= True _r_3(leaf, z) <= True _r_3(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) numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_2, x_1_0) /\ _r_2(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1, x_1_0) } ] ; plus -> [ plus : { plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True plus(s(x_0_0), z, s(x_2_0)) <= True plus(z, s(x_1_0), s(x_2_0)) <= True plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : 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: () numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) : Yes: { _kn -> s(z) ; _ln -> s(z) ; _mn -> s(z) ; t1 -> node(_wnlqw_0, leaf, node(_mplqw_0, _mplqw_1, _mplqw_2)) ; t2 -> node(_xnlqw_0, leaf, _xnlqw_2) } le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) : No: () plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) : No: () ------------------------------------------- Step 20, which took 10.929090 s (model generation: 10.926345, model checking: 0.002745): Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, s(z)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= True plus(s(s(z)), z, s(s(z))) <= True plus(s(z), s(z), s(s(z))) <= True plus(s(z), z, s(z)) <= True plus(z, s(s(z)), s(s(z))) <= True plus(z, s(z), s(z)) <= True plus(z, z, z) <= True False <= le(s(s(z)), s(s(z))) False <= le(s(s(z)), s(z)) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= numnodes(leaf, s(s(z))) False <= numnodes(leaf, s(z)) False <= numnodes(node(a, leaf, leaf), s(s(z))) False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z)) numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ plus(s(z), s(z), s(z)) numnodes(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ plus(s(s(s(s(s(z))))), s(s(s(z))), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), leaf), z) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), z) False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(z))) numnodes(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), z) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(z)) False <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) numnodes(node(a, node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), leaf), s(s(z))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(s(z)))) /\ plus(s(s(s(z))), z, s(z)) le(s(s(s(z))), s(s(z))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) /\ numnodes(node(a, node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), node(a, leaf, leaf)), s(s(z))) False <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= plus(s(z), z, s(s(z))) numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z)))) numnodes(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= plus(z, s(s(z)), s(z)) } Current best model: |_ name: None 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 } ] ; numnodes -> [ numnodes : { _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_3(leaf, z) <= True _r_3(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_3(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ _r_3(x_0_2, x_1_0) } ] ; plus -> [ plus : { plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True plus(s(x_0_0), z, s(x_2_0)) <= True plus(z, s(x_1_0), s(x_2_0)) <= True plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : 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: () numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) : Yes: { _kn -> s(s(z)) ; _ln -> s(s(z)) ; _mn -> s(z) ; t1 -> node(_vvlqw_0, node(_vbmqw_0, leaf, leaf), node(_zbmqw_0, _zbmqw_1, _zbmqw_2)) ; t2 -> node(_wvlqw_0, node(_iamqw_0, leaf, leaf), _wvlqw_2) } le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) : No: () plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) : No: () ------------------------------------------- Step 21, which took 41.084125 s (model generation: 41.082149, model checking: 0.001976): Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, s(z)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= True plus(s(s(z)), z, s(s(z))) <= True plus(s(z), s(z), s(s(z))) <= True plus(s(z), z, s(z)) <= True plus(z, s(s(z)), s(s(z))) <= True plus(z, s(z), s(z)) <= True plus(z, z, z) <= True False <= le(s(s(z)), s(s(z))) False <= le(s(s(z)), s(z)) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= numnodes(leaf, s(s(z))) False <= numnodes(leaf, s(z)) False <= numnodes(node(a, leaf, leaf), s(s(z))) False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z)) numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ plus(s(z), s(z), s(z)) numnodes(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ plus(s(s(s(s(s(z))))), s(s(s(z))), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), leaf), z) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), z) False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(z))) numnodes(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ plus(s(s(z)), s(s(z)), s(z)) numnodes(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), z) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(z)) False <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) numnodes(node(a, node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), leaf), s(s(z))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(s(z)))) /\ plus(s(s(s(z))), z, s(z)) le(s(s(s(z))), s(s(z))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) /\ numnodes(node(a, node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), node(a, leaf, leaf)), s(s(z))) False <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= plus(s(z), z, s(s(z))) numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z)))) numnodes(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= plus(z, s(s(z)), s(z)) } Current best model: |_ name: None 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 } ] ; numnodes -> [ numnodes : { _r_2(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_2, x_1_0) _r_3(leaf, s(x_1_0)) <= True _r_3(leaf, z) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_2, x_1_0) /\ numnodes(x_0_1, x_1_0) } ] ; plus -> [ plus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) plus(z, s(x_1_0), s(x_2_0)) <= True plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _| Answer of teacher: numnodes(leaf, z) <= True : No: () plus(n, z, n) <= True : No: () le(s(nn1), s(nn2)) <= le(nn1, nn2) : No: () False <= le(s(nn1), z) : No: () False <= le(z, z) : No: () plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) : Yes: { _fn -> s(_vpmqw_0) ; mm -> s(z) ; n -> s(z) } Total time: 60.924616 Learner time: 59.856319 Teacher time: 0.055662 Reasons for stopping: Maybe: timeout during learnerLast solver state: Clauses: { numnodes(leaf, z) <= True -> 0 plus(n, z, n) <= True -> 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 numnodes(node(e, t1, t2), s(_mn)) <= numnodes(t1, _kn) /\ numnodes(t2, _ln) /\ plus(_kn, _ln, _mn) -> 0 le(_qn, _rn) <= numnodes(t1, _qn) /\ numnodes(node(e, t1, t2), _rn) -> 0 plus(n, s(mm), s(_fn)) <= plus(n, mm, _fn) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, s(z)) <= True numnodes(leaf, z) <= True numnodes(node(a, leaf, leaf), s(z)) <= True numnodes(node(a, leaf, node(a, leaf, leaf)), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), leaf), s(s(z))) <= True numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(s(z)))) <= True plus(s(s(z)), z, s(s(z))) <= True plus(s(z), s(z), s(s(z))) <= True plus(s(z), z, s(z)) <= True plus(z, s(s(z)), s(s(z))) <= True plus(z, s(z), s(z)) <= True plus(z, z, z) <= True False <= le(s(s(z)), s(s(z))) False <= le(s(s(z)), s(z)) False <= le(s(z), s(z)) False <= le(s(z), z) False <= le(z, z) False <= numnodes(leaf, s(s(z))) False <= numnodes(leaf, s(z)) False <= numnodes(node(a, leaf, leaf), s(s(z))) False <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(z)) numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(z))) <= numnodes(node(a, leaf, node(a, leaf, leaf)), s(z)) /\ plus(s(z), s(z), s(z)) numnodes(node(a, node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) /\ numnodes(node(a, node(a, node(a, node(a, leaf, leaf), leaf), leaf), leaf), s(s(s(s(s(z)))))) /\ plus(s(s(s(s(s(z))))), s(s(s(z))), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), leaf), s(z)) False <= numnodes(node(a, node(a, leaf, leaf), leaf), z) /\ numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), z) False <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ numnodes(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), node(a, leaf, leaf))), s(s(z))) numnodes(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), s(s(z))) /\ plus(s(s(z)), s(s(z)), s(z)) numnodes(node(a, node(a, node(a, leaf, leaf), node(a, leaf, leaf)), node(a, node(a, leaf, node(a, leaf, leaf)), leaf)), s(s(z))) <= numnodes(node(a, node(a, leaf, leaf), node(a, leaf, leaf)), z) /\ numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(s(z)))) /\ plus(z, s(s(s(z))), s(z)) False <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), leaf), s(s(z))) numnodes(node(a, node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), leaf), s(s(z))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, leaf)), s(s(s(z)))) /\ plus(s(s(s(z))), z, s(z)) le(s(s(s(z))), s(s(z))) <= numnodes(node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), s(s(s(z)))) /\ numnodes(node(a, node(a, node(a, leaf, node(a, leaf, leaf)), node(a, leaf, node(a, leaf, leaf))), node(a, leaf, leaf)), s(s(z))) False <= numnodes(node(a, node(a, node(a, leaf, leaf), leaf), leaf), s(s(z))) plus(s(z), s(s(z)), s(s(z))) <= plus(s(z), s(z), s(z)) numnodes(node(a, node(a, leaf, leaf), leaf), s(s(s(z)))) <= plus(s(z), z, s(s(z))) numnodes(node(a, leaf, node(a, leaf, node(a, leaf, leaf))), s(s(s(s(z))))) <= plus(z, s(s(z)), s(s(s(z)))) numnodes(node(a, leaf, node(a, node(a, leaf, leaf), leaf)), s(s(z))) <= plus(z, s(s(z)), s(z)) } Current best model: |_ name: None 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 } ] ; numnodes -> [ numnodes : { _r_2(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_2, x_1_0) _r_3(leaf, s(x_1_0)) <= True _r_3(leaf, z) <= True numnodes(leaf, z) <= True numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_2(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_1, x_1_0) /\ numnodes(x_0_2, x_1_0) numnodes(node(x_0_0, x_0_1, x_0_2), s(x_1_0)) <= _r_3(x_0_2, x_1_0) /\ numnodes(x_0_1, x_1_0) } ] ; plus -> [ plus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) plus(z, s(x_1_0), s(x_2_0)) <= True plus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, etree, nat} _|