Solving ../../benchmarks/smtlib/true/plus_le.smt2... Inference procedure has parameters: Ice fuel: 200 Timeout: Some(60.) (sec) Teacher_type: Checks all clauses every time Approximation method: remove every clause that can be safely removed Learning problem is: env: { nat -> {s, z} } definition: { (plus, F: { plus(n, z, n) <= True plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) } eq_nat(_lra, _mra) <= plus(_jra, _kra, _lra) /\ plus(_jra, _kra, _mra) ) (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) } ) } properties: { le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) } over-approximation: {plus} under-approximation: {} Clause system for inference is: { le(z, s(nn2)) <= 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 le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) -> 0 False <= le(z, z) -> 0 plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) -> 0 } Solving took 0.200110 seconds. Yes: |_ 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 } ] ; plus -> [ plus : { _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 plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= le(x_0_0, x_2_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: {nat} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.005897 s (model generation: 0.005818, model checking: 0.000079): Clauses: { le(z, s(nn2)) <= 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 le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) -> 0 False <= le(z, z) -> 0 plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) -> 0 } Accumulated learning constraints: { } Current best model: |_ name: None le -> [ le : { } ] ; plus -> [ plus : { } ] -- Equality automata are defined for: {nat} _| Answer of teacher: le(z, s(nn2)) <= 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: () le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) : No: () False <= le(z, z) : No: () plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) : No: () ------------------------------------------- Step 1, which took 0.007756 s (model generation: 0.007655, model checking: 0.000101): Clauses: { le(z, s(nn2)) <= 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 le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) -> 0 False <= le(z, z) -> 0 plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) -> 0 } Accumulated learning constraints: { le(z, s(z)) <= True plus(z, z, z) <= True } Current best model: |_ name: None le -> [ le : { le(z, s(x_1_0)) <= True } ] ; plus -> [ plus : { plus(z, z, z) <= True } ] -- Equality automata are defined for: {nat} _| Answer of teacher: le(z, s(nn2)) <= True : No: () plus(n, z, n) <= True : Yes: { n -> s(_ffrba_0) } le(s(nn1), s(nn2)) <= le(nn1, nn2) : Yes: { nn1 -> z ; nn2 -> s(_hfrba_0) } le(nn1, nn2) <= le(s(nn1), s(nn2)) : No: () False <= le(s(nn1), z) : No: () le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) : No: () False <= le(z, z) : No: () plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) : Yes: { _ira -> z ; mm -> z ; n -> z } ------------------------------------------- Step 2, which took 0.016599 s (model generation: 0.015363, model checking: 0.001236): Clauses: { le(z, s(nn2)) <= 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 le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) -> 0 False <= le(z, z) -> 0 plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, 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(s(x_0_0), s(x_1_0)) <= True le(z, 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: {nat} _| Answer of teacher: le(z, s(nn2)) <= 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: () le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) : No: () False <= le(z, z) : No: () plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) : Yes: { _ira -> s(_pfrba_0) ; mm -> z ; n -> s(_rfrba_0) } ------------------------------------------- Step 3, which took 0.022698 s (model generation: 0.022604, model checking: 0.000094): Clauses: { le(z, s(nn2)) <= 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 le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) -> 0 False <= le(z, z) -> 0 plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, 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)) } 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 } ] ; 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: {nat} _| Answer of teacher: le(z, s(nn2)) <= 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(_sfrba_0) ; nn2 -> z } False <= le(s(nn1), z) : No: () le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) : No: () False <= le(z, z) : Yes: { } plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) : No: () ------------------------------------------- Step 4, which took 0.020994 s (model generation: 0.020177, model checking: 0.000817): Clauses: { le(z, s(nn2)) <= 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 le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) -> 0 False <= le(z, z) -> 0 plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, 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) } 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 } ] ; 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: {nat} _| Answer of teacher: le(z, s(nn2)) <= 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: { } le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) : Yes: { _nra -> s(z) ; m -> s(_fgrba_0) ; n -> s(z) } False <= le(z, z) : No: () plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) : No: () ------------------------------------------- Step 5, which took 0.022424 s (model generation: 0.022020, model checking: 0.000404): Clauses: { le(z, s(nn2)) <= 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 le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) -> 0 False <= le(z, z) -> 0 plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, 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 <= plus(s(z), 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 } ] ; plus -> [ plus : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= le(x_0_0, x_2_0) plus(s(x_0_0), z, s(x_2_0)) <= True plus(z, s(x_1_0), s(x_2_0)) <= True plus(z, z, z) <= True } ] -- Equality automata are defined for: {nat} _| Answer of teacher: le(z, s(nn2)) <= 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: () le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) : No: () False <= le(z, z) : No: () plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) : Yes: { _ira -> s(z) ; mm -> z ; n -> s(s(z)) } ------------------------------------------- Step 6, which took 0.016394 s (model generation: 0.016245, model checking: 0.000149): Clauses: { le(z, s(nn2)) <= 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 le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) -> 0 False <= le(z, z) -> 0 plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, 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) plus(s(s(z)), s(z), s(s(z))) <= plus(s(s(z)), z, s(z)) False <= plus(s(z), 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 } ] ; plus -> [ plus : { le(s(x_0_0), s(x_1_0)) <= le(x_0_0, x_1_0) le(z, s(x_1_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= le(x_1_0, x_2_0) plus(s(x_0_0), z, s(x_2_0)) <= True plus(z, s(x_1_0), s(x_2_0)) <= True plus(z, z, z) <= True } ] -- Equality automata are defined for: {nat} _| Answer of teacher: le(z, s(nn2)) <= 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: () le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) : Yes: { _nra -> s(s(z)) ; m -> s(z) ; n -> s(s(z)) } False <= le(z, z) : No: () plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) : No: () ------------------------------------------- Step 7, which took 0.015061 s (model generation: 0.014691, model checking: 0.000370): Clauses: { le(z, s(nn2)) <= 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 le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) -> 0 False <= le(z, z) -> 0 plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, 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) le(s(s(z)), s(s(z))) <= plus(s(s(z)), s(z), s(s(z))) plus(s(s(z)), s(z), s(s(z))) <= plus(s(s(z)), z, s(z)) False <= plus(s(z), s(z), s(z)) } 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 } ] ; 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: {nat} _| Answer of teacher: le(z, s(nn2)) <= 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(_ajrba_0) ; nn2 -> s(z) } False <= le(s(nn1), z) : No: () le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) : No: () False <= le(z, z) : No: () plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) : No: () ------------------------------------------- Step 8, which took 0.012025 s (model generation: 0.011872, model checking: 0.000153): Clauses: { le(z, s(nn2)) <= 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 le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) -> 0 False <= le(z, z) -> 0 plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, 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 <= plus(s(s(z)), s(z), s(s(z))) False <= plus(s(s(z)), z, s(z)) False <= plus(s(z), 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 } ] ; plus -> [ plus : { _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 plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= le(x_0_0, x_2_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: {nat} _| Answer of teacher: le(z, s(nn2)) <= True : No: () plus(n, z, n) <= True : Yes: { n -> s(s(_kkrba_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: () le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) : No: () False <= le(z, z) : No: () plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) : No: () ------------------------------------------- Step 9, which took 0.022810 s (model generation: 0.022605, model checking: 0.000205): Clauses: { le(z, s(nn2)) <= 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 le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) -> 0 False <= le(z, z) -> 0 plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, 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(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 <= plus(s(s(z)), s(z), s(s(z))) False <= plus(s(s(z)), z, s(z)) False <= plus(s(z), 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 } ] ; plus -> [ plus : { _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 plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ le(x_0_0, x_2_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: {nat} _| Answer of teacher: le(z, s(nn2)) <= 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: () le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) : No: () False <= le(z, z) : No: () plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) : Yes: { _ira -> s(s(_tlrba_0)) ; mm -> z ; n -> s(s(_slrba_0)) } ------------------------------------------- Step 10, which took 0.017482 s (model generation: 0.017304, model checking: 0.000178): Clauses: { le(z, s(nn2)) <= 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 le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) -> 0 False <= le(z, z) -> 0 plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) -> 0 } Accumulated learning constraints: { le(s(z), s(s(z))) <= True le(z, s(z)) <= True plus(s(s(z)), s(z), 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(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 <= plus(s(s(z)), s(z), s(s(z))) False <= plus(s(s(z)), z, s(z)) False <= plus(s(z), 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 } ] ; plus -> [ plus : { _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 plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= le(x_0_0, x_2_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: {nat} _| Answer of teacher: le(z, s(nn2)) <= 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: () le(n, _nra) <= le(z, m) /\ plus(n, m, _nra) : No: () False <= le(z, z) : No: () plus(n, s(mm), s(_ira)) <= plus(n, mm, _ira) : Yes: { _ira -> s(s(z)) ; mm -> z ; n -> s(s(s(z))) } Total time: 0.200110 Learner time: 0.176354 Teacher time: 0.003786 Reasons for stopping: Yes: |_ 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 } ] ; plus -> [ plus : { _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 plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= le(x_0_0, x_2_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: {nat} _|