Solving ../../benchmarks/smtlib/true/min_of_plus_and_max.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(_fga)) <= plus(n, mm, _fga) } eq_nat(_iga, _jga) <= plus(_gga, _hga, _iga) /\ plus(_gga, _hga, _jga) ) (mult, F: { mult(n, z, z) <= True mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) } eq_nat(_oga, _pga) <= mult(_mga, _nga, _oga) /\ mult(_mga, _nga, _pga) ) (leq_nat, P: { leq_nat(z, s(nn2)) <= True leq_nat(z, z) <= True leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) False <= leq_nat(s(nn1), z) } ) (max_ite, F: { leq_nat(x, y) \/ max_ite(x, y, x) <= True max_ite(x, y, y) <= leq_nat(x, y) } eq_nat(_sga, _tga) <= max_ite(_qga, _rga, _sga) /\ max_ite(_qga, _rga, _tga) ) (minus, F: { minus(s(u), z, s(u)) <= True minus(z, y, z) <= True minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) } eq_nat(_xga, _yga) <= minus(_vga, _wga, _xga) /\ minus(_vga, _wga, _yga) ) (min_ite, F: { leq_nat(x, y) \/ min_ite(x, y, y) <= True min_ite(x, y, x) <= leq_nat(x, y) } eq_nat(_bha, _cha) <= min_ite(_zga, _aha, _bha) /\ min_ite(_zga, _aha, _cha) ) } properties: { eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) } over-approximation: {max_ite, min_ite, minus, mult, plus} under-approximation: {mult} Clause system for inference is: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Solving took 60.575028 seconds. Maybe: timeout during teacher: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> out of time leq_nat(x, y) \/ min_ite(x, y, y) <= True -> out of time leq_nat(z, s(nn2)) <= True -> out of time leq_nat(z, z) <= True -> out of time minus(s(u), z, s(u)) <= True -> out of time minus(z, y, z) <= True -> out of time plus(n, z, n) <= True -> out of time leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> out of time max_ite(x, y, y) <= leq_nat(x, y) -> out of time min_ite(x, y, x) <= leq_nat(x, y) -> out of time leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> out of time False <= leq_nat(s(nn1), z) -> out of time eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> out of time minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> out of time mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> out of time plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> out of time }Last solver state: Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(s(s(z))), s(s(z))) \/ max_ite(s(s(s(z))), s(s(z)), s(s(s(z)))) <= True leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(s(z))) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(s(z)), s(s(z))) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(s(z)), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(s(z)), s(s(z))) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(s(z)), s(z), s(z)) <= True min_ite(s(s(z)), z, z) <= True min_ite(s(z), s(z), s(z)) <= True min_ite(s(z), z, z) <= True min_ite(z, s(s(z)), z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, 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(s(z)), s(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 <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(s(z)), z) False <= leq_nat(s(z), z) False <= max_ite(s(s(z)), s(s(z)), s(z)) /\ min_ite(s(s(z)), s(s(z)), s(z)) /\ plus(s(s(z)), s(s(z)), s(z)) False <= max_ite(s(s(z)), s(z), s(z)) /\ plus(s(s(z)), s(z), s(z)) False <= max_ite(s(s(z)), z, s(z)) False <= max_ite(s(z), s(s(z)), s(z)) /\ min_ite(s(z), s(s(z)), s(z)) /\ plus(s(z), s(s(z)), s(z)) False <= max_ite(s(z), s(z), s(s(z))) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(z)) False <= max_ite(z, s(s(z)), s(s(s(z)))) /\ minus(s(s(z)), s(s(s(z))), s(z)) False <= max_ite(z, s(s(z)), s(z)) False <= max_ite(z, s(z), s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= min_ite(s(s(z)), s(s(z)), s(z)) /\ plus(s(s(z)), s(s(z)), s(s(z))) False <= min_ite(s(z), s(s(z)), s(z)) /\ plus(s(z), s(s(z)), s(s(z))) False <= minus(s(s(s(z))), s(s(z)), s(s(z))) /\ plus(z, s(s(z)), s(s(s(z)))) False <= minus(s(s(s(z))), s(z), s(z)) /\ plus(s(z), z, s(s(s(z)))) False <= minus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), z) minus(s(s(z)), s(s(s(z))), s(s(z))) <= minus(s(z), s(s(z)), s(s(z))) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) plus(s(s(z)), s(s(s(z))), s(s(z))) <= plus(s(s(z)), s(s(z)), s(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)) False <= plus(s(z), z, s(s(z))) False <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(z, z) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { min_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True min_ite(s(x_0_0), z, z) <= True min_ite(z, s(x_1_0), z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(z, z) <= True _r_2(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0, x_1_0) _r_2(s(x_0_0), z) <= True _r_2(z, s(x_1_0)) <= True leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_1_0, x_2_0) /\ leq_nat(x_0_0, x_1_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0, x_1_0) /\ _r_2(x_0_0, x_2_0) minus(s(x_0_0), s(x_1_0), z) <= leq_nat(x_0_0, x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; 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 _r_2(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0, x_1_0) _r_2(s(x_0_0), z) <= True _r_2(z, s(x_1_0)) <= True leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_0_0, x_2_0) /\ leq_nat(x_1_0, x_2_0) plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0, x_1_0) /\ _r_2(x_0_0, x_2_0) /\ _r_2(x_1_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)) <= _r_1(x_1_0, x_2_0) plus(z, z, z) <= True } ] -- Equality automata are defined for: {nat} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.005967 s (model generation: 0.005819, model checking: 0.000148): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { } Current best model: |_ name: None leq_nat -> [ leq_nat : { } ] ; max_ite -> [ max_ite : { } ] ; min_ite -> [ min_ite : { } ] ; minus -> [ minus : { } ] ; mult -> [ mult : { } ] ; plus -> [ plus : { } ] -- Equality automata are defined for: {nat} _| Answer of teacher: leq_nat(x, y) \/ max_ite(x, y, x) <= True : Yes: { x -> z ; y -> z } leq_nat(x, y) \/ min_ite(x, y, y) <= True : Yes: { x -> z ; y -> z } leq_nat(z, s(nn2)) <= True : Yes: { } leq_nat(z, z) <= True : Yes: { } minus(s(u), z, s(u)) <= True : Yes: { } minus(z, y, z) <= True : Yes: { y -> z } plus(n, z, n) <= True : Yes: { n -> z } leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () min_ite(x, y, x) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : No: () minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : No: () mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : No: () ------------------------------------------- Step 1, which took 0.007228 s (model generation: 0.006685, model checking: 0.000543): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(z, s(z)) <= True leq_nat(z, z) <= True minus(s(z), z, s(z)) <= True minus(z, z, z) <= True plus(z, z, z) <= True } Current best model: |_ name: None leq_nat -> [ leq_nat : { leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { } ] ; min_ite -> [ min_ite : { } ] ; minus -> [ minus : { minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; plus -> [ plus : { plus(z, z, z) <= True } ] -- Equality automata are defined for: {nat} _| Answer of teacher: leq_nat(x, y) \/ max_ite(x, y, x) <= True : Yes: { x -> s(_zblaa_0) ; y -> z } leq_nat(x, y) \/ min_ite(x, y, y) <= True : Yes: { x -> s(_dclaa_0) ; y -> z } leq_nat(z, s(nn2)) <= True : No: () leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : Yes: { y -> s(_fclaa_0) } plus(n, z, n) <= True : Yes: { n -> s(_gclaa_0) } leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : Yes: { nn1 -> z ; nn2 -> z } max_ite(x, y, y) <= leq_nat(x, y) : Yes: { x -> z ; y -> z } min_ite(x, y, x) <= leq_nat(x, y) : Yes: { x -> z ; y -> z } leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : No: () minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : Yes: { _uga -> z ; u -> z ; x2 -> z } mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : Yes: { _fga -> z ; mm -> z ; n -> z } ------------------------------------------- Step 2, which took 0.015853 s (model generation: 0.015520, model checking: 0.000333): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(z), s(z)) <= True leq_nat(s(z), z) \/ max_ite(s(z), z, s(z)) <= True leq_nat(s(z), z) \/ min_ite(s(z), z, z) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(z, z, z) <= True min_ite(z, z, z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, 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 leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= True leq_nat(s(x_0_0), z) <= True leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { min_ite(s(x_0_0), z, z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; 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: leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(x, y) \/ min_ite(x, y, y) <= True : No: () leq_nat(z, s(nn2)) <= True : No: () leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () plus(n, z, n) <= True : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : Yes: { x -> z ; y -> s(_hdlaa_0) } min_ite(x, y, x) <= leq_nat(x, y) : Yes: { x -> z ; y -> s(_ndlaa_0) } leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : Yes: { } eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : No: () minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : Yes: { _uga -> s(_odlaa_0) ; u -> s(_pdlaa_0) ; x2 -> z } mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : Yes: { _fga -> s(_rdlaa_0) ; mm -> z ; n -> s(_tdlaa_0) } ------------------------------------------- Step 3, which took 0.016648 s (model generation: 0.016508, model checking: 0.000140): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(z), z, z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, 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 <= leq_nat(s(z), z) } Current best model: |_ name: None leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= True leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= True max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { min_ite(s(x_0_0), z, z) <= True min_ite(z, s(x_1_0), z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; 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: leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(x, y) \/ min_ite(x, y, y) <= True : No: () leq_nat(z, s(nn2)) <= True : No: () leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () plus(n, z, n) <= True : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : Yes: { x -> s(_udlaa_0) ; y -> s(_vdlaa_0) } min_ite(x, y, x) <= leq_nat(x, y) : Yes: { x -> s(_wdlaa_0) ; y -> s(_xdlaa_0) } leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : Yes: { nn1 -> s(_ydlaa_0) ; nn2 -> z } False <= leq_nat(s(nn1), z) : No: () eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : Yes: { _dha -> z ; _eha -> s(_helaa_0) ; _fha -> s(_ielaa_0) ; _gha -> s(_jelaa_0) ; n1 -> z ; n2 -> s(_lelaa_0) } minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : No: () mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : No: () ------------------------------------------- Step 4, which took 0.026421 s (model generation: 0.026204, model checking: 0.000217): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(z), s(z), s(z)) <= True min_ite(s(z), z, z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, 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 <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) False <= minus(s(z), s(z), s(z)) } Current best model: |_ name: None leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= True max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { min_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True min_ite(s(x_0_0), z, z) <= True min_ite(z, s(x_1_0), z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; 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: leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(x, y) \/ min_ite(x, y, y) <= True : No: () leq_nat(z, s(nn2)) <= True : No: () leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () plus(n, z, n) <= True : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () min_ite(x, y, x) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : Yes: { _dha -> s(_cflaa_0) ; _eha -> s(_dflaa_0) ; _fha -> s(_eflaa_0) ; _gha -> z ; n1 -> s(_gflaa_0) ; n2 -> s(_hflaa_0) } minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : Yes: { _uga -> s(_uflaa_0) ; u -> s(s(_aglaa_0)) ; x2 -> s(z) } mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : No: () ------------------------------------------- Step 5, which took 0.026501 s (model generation: 0.026120, model checking: 0.000381): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(z), s(z), s(z)) <= True min_ite(s(z), z, z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, 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 <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) False <= minus(s(z), s(z), s(z)) False <= plus(s(z), s(z), s(z)) } Current best model: |_ name: None leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= True max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { min_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True min_ite(s(x_0_0), z, z) <= True min_ite(z, s(x_1_0), z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), z) <= True _r_1(z, s(x_1_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; plus -> [ plus : { _r_1(s(x_0_0), z) <= True _r_1(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_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: leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(x, y) \/ min_ite(x, y, y) <= True : No: () leq_nat(z, s(nn2)) <= True : No: () leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () plus(n, z, n) <= True : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () min_ite(x, y, x) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : Yes: { _dha -> z ; _eha -> s(z) ; _fha -> s(_ahlaa_0) ; _gha -> s(s(_zhlaa_0)) ; n1 -> s(_chlaa_0) ; n2 -> z } minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : Yes: { _uga -> s(s(_ailaa_0)) ; u -> s(_ohlaa_0) ; x2 -> z } mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : Yes: { _fga -> s(_thlaa_0) ; mm -> z ; n -> s(s(_bilaa_0)) } ------------------------------------------- Step 6, which took 0.039554 s (model generation: 0.039226, model checking: 0.000328): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(z), s(z), s(z)) <= True min_ite(s(z), z, z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, 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 <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), 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 leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= True max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { min_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True min_ite(s(x_0_0), z, z) <= True min_ite(z, s(x_1_0), z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(s(x_0_0), z) <= True _r_1(z, s(x_1_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_1(x_0_0, x_2_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; plus -> [ plus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(s(x_0_0), z) <= True _r_1(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_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: leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(x, y) \/ min_ite(x, y, y) <= True : No: () leq_nat(z, s(nn2)) <= True : No: () leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () plus(n, z, n) <= True : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () min_ite(x, y, x) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : Yes: { _dha -> z ; _eha -> s(z) ; _fha -> s(s(_hklaa_0)) ; _gha -> s(s(_hklaa_0)) ; n1 -> z ; n2 -> s(_jjlaa_0) } minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : No: () mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : No: () ------------------------------------------- Step 7, which took 0.036267 s (model generation: 0.035900, model checking: 0.000367): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(z), s(z), s(z)) <= True min_ite(s(z), z, z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, 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 <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) False <= max_ite(z, s(z), s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), 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 leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= True max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { min_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True min_ite(s(x_0_0), z, z) <= True min_ite(z, s(x_1_0), z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; 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: leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(x, y) \/ min_ite(x, y, y) <= True : No: () leq_nat(z, s(nn2)) <= True : No: () leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () plus(n, z, n) <= True : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () min_ite(x, y, x) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : Yes: { _dha -> z ; _eha -> s(s(_cmlaa_0)) ; _fha -> s(_mllaa_0) ; _gha -> s(_nllaa_0) ; n1 -> z ; n2 -> s(_pllaa_0) } minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : No: () mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : No: () ------------------------------------------- Step 8, which took 0.061803 s (model generation: 0.061377, model checking: 0.000426): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(z), s(z), s(z)) <= True min_ite(s(z), z, z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, 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 <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) False <= max_ite(z, s(z), s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), 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)) False <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None leq_nat -> [ leq_nat : { _r_2(z) <= True leq_nat(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= True max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { min_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True min_ite(s(x_0_0), z, z) <= True min_ite(z, s(x_1_0), z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; plus -> [ plus : { _r_1(s(x_0_0)) <= True _r_2(z) <= 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)) <= _r_2(x_2_0) plus(z, z, z) <= True } ] -- Equality automata are defined for: {nat} _| Answer of teacher: leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(x, y) \/ min_ite(x, y, y) <= True : No: () leq_nat(z, s(nn2)) <= True : No: () leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () plus(n, z, n) <= True : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : Yes: { nn1 -> s(z) ; nn2 -> s(_emlaa_0) } max_ite(x, y, y) <= leq_nat(x, y) : No: () min_ite(x, y, x) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : Yes: { _dha -> s(_tmlaa_0) ; _eha -> s(s(_dolaa_0)) ; _fha -> s(_vmlaa_0) ; _gha -> z ; n1 -> s(_xmlaa_0) ; n2 -> s(_ymlaa_0) } minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : No: () mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : Yes: { _fga -> s(z) ; mm -> s(_ynlaa_0) ; n -> z } ------------------------------------------- Step 9, which took 0.062898 s (model generation: 0.062356, model checking: 0.000542): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(z), s(z), s(z)) <= True min_ite(s(z), z, z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, 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 <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) False <= max_ite(z, s(z), s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), 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)) False <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None leq_nat -> [ leq_nat : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True leq_nat(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= True max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { min_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True min_ite(s(x_0_0), z, z) <= True min_ite(z, s(x_1_0), z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True _r_2(s(x_0_0)) <= True leq_nat(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= leq_nat(x_0_0, x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; plus -> [ plus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True _r_2(s(x_0_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_2_0) plus(s(x_0_0), z, s(x_2_0)) <= True plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) plus(z, z, z) <= True } ] -- Equality automata are defined for: {nat} _| Answer of teacher: leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(x, y) \/ min_ite(x, y, y) <= True : No: () leq_nat(z, s(nn2)) <= True : No: () leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () plus(n, z, n) <= True : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : Yes: { nn1 -> z ; nn2 -> s(_jolaa_0) } max_ite(x, y, y) <= leq_nat(x, y) : No: () min_ite(x, y, x) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : Yes: { nn1 -> s(z) ; nn2 -> s(s(_tqlaa_0)) } False <= leq_nat(s(nn1), z) : No: () eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : Yes: { _dha -> z ; _eha -> s(s(_pqlaa_0)) ; _fha -> s(_eplaa_0) ; _gha -> s(_fplaa_0) ; n1 -> s(_gplaa_0) ; n2 -> z } minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : Yes: { _uga -> z ; u -> s(z) ; x2 -> s(s(_xqlaa_0)) } mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : No: () ------------------------------------------- Step 10, which took 0.069313 s (model generation: 0.068826, model checking: 0.000487): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(z), s(z), s(z)) <= True min_ite(s(z), z, z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, 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 <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) False <= max_ite(z, s(z), s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= minus(s(s(z)), s(z), z) minus(s(s(z)), s(s(s(z))), z) <= minus(s(z), s(s(z)), z) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), 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)) False <= plus(s(z), z, s(s(z))) False <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= True max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { min_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True min_ite(s(x_0_0), z, z) <= True min_ite(z, s(x_1_0), z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= leq_nat(x_0_0, x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; plus -> [ plus : { _r_1(s(x_0_0)) <= True _r_2(z) <= 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)) <= _r_2(x_2_0) plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0) plus(z, s(x_1_0), s(x_2_0)) <= _r_2(x_2_0) plus(z, z, z) <= True } ] -- Equality automata are defined for: {nat} _| Answer of teacher: leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(x, y) \/ min_ite(x, y, y) <= True : No: () leq_nat(z, s(nn2)) <= True : No: () leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () plus(n, z, n) <= True : Yes: { n -> s(s(_ttlaa_0)) } leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () min_ite(x, y, x) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : Yes: { _dha -> z ; _eha -> s(s(_vtlaa_0)) ; _fha -> s(_fslaa_0) ; _gha -> s(_gslaa_0) ; n1 -> z ; n2 -> s(s(_utlaa_0)) } minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : No: () mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : No: () ------------------------------------------- Step 11, which took 0.144994 s (model generation: 0.144522, model checking: 0.000472): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(z), s(z), s(z)) <= True min_ite(s(z), z, z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, 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 <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) False <= max_ite(z, s(s(z)), s(z)) /\ min_ite(z, s(s(z)), z) False <= max_ite(z, s(z), s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= minus(s(s(z)), s(z), z) minus(s(s(z)), s(s(s(z))), z) <= minus(s(z), s(s(z)), z) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), 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)) False <= plus(s(z), z, s(s(z))) False <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { min_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True min_ite(s(x_0_0), z, z) <= True min_ite(z, s(x_1_0), z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True _r_2(s(x_0_0), s(x_1_0)) <= True _r_2(s(x_0_0), z) <= True _r_2(z, s(x_1_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0, x_1_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0, x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; plus -> [ plus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True _r_2(s(x_0_0), s(x_1_0)) <= True _r_2(s(x_0_0), z) <= True _r_2(z, s(x_1_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0, x_2_0) /\ _r_2(x_1_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)) <= _r_1(x_1_0, x_2_0) plus(z, z, z) <= True } ] -- Equality automata are defined for: {nat} _| Answer of teacher: leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(x, y) \/ min_ite(x, y, y) <= True : No: () leq_nat(z, s(nn2)) <= True : No: () leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () plus(n, z, n) <= True : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () min_ite(x, y, x) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : Yes: { _dha -> z ; _eha -> s(z) ; _fha -> s(s(_jxlaa_0)) ; _gha -> s(_fvlaa_0) ; n1 -> s(z) ; n2 -> z } minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : Yes: { _uga -> z ; u -> z ; x2 -> s(_zvlaa_0) } mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : No: () ------------------------------------------- Step 12, which took 0.118861 s (model generation: 0.118330, model checking: 0.000531): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(z), s(z), s(z)) <= True min_ite(s(z), z, z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, 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 <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(z)) False <= max_ite(z, s(s(z)), s(z)) /\ min_ite(z, s(s(z)), z) False <= max_ite(z, s(z), s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), 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)) False <= plus(s(z), z, s(s(z))) False <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_2(s(x_0_0), s(x_1_0)) <= True _r_2(z, z) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= _r_2(x_1_0, x_2_0) max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { min_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True min_ite(s(x_0_0), z, z) <= True min_ite(z, s(x_1_0), z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(s(x_0_0), z) <= True _r_1(z, s(x_1_0)) <= True leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_1(x_0_0, x_2_0) minus(s(x_0_0), s(x_1_0), z) <= leq_nat(x_0_0, x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; plus -> [ plus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(s(x_0_0), z) <= True _r_1(z, s(x_1_0)) <= True _r_2(s(x_0_0), s(x_1_0)) <= True _r_2(z, z) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) plus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0, x_2_0) plus(z, s(x_1_0), s(x_2_0)) <= _r_2(x_1_0, x_2_0) plus(z, z, z) <= True } ] -- Equality automata are defined for: {nat} _| Answer of teacher: leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(x, y) \/ min_ite(x, y, y) <= True : No: () leq_nat(z, s(nn2)) <= True : No: () leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () plus(n, z, n) <= True : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () min_ite(x, y, x) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : Yes: { _dha -> s(_dylaa_0) ; _eha -> s(z) ; _fha -> s(z) ; _gha -> z ; n1 -> s(_hylaa_0) ; n2 -> s(s(_iamaa_0)) } minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : No: () mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : No: () ------------------------------------------- Step 13, which took 0.110490 s (model generation: 0.109969, model checking: 0.000521): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(z), s(z), s(z)) <= True min_ite(s(z), z, z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, 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 <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) False <= max_ite(s(z), s(s(z)), s(z)) /\ min_ite(s(z), s(s(z)), s(z)) /\ plus(s(z), s(s(z)), s(z)) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(z)) False <= max_ite(z, s(s(z)), s(z)) /\ min_ite(z, s(s(z)), z) False <= max_ite(z, s(z), s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), 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)) False <= plus(s(z), z, s(s(z))) False <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_2(s(x_0_0), s(x_1_0)) <= True _r_2(z, z) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= _r_2(x_1_0, x_2_0) max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { min_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True min_ite(s(x_0_0), z, z) <= True min_ite(z, s(x_1_0), z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(s(x_0_0), z) <= True _r_1(z, s(x_1_0)) <= True leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_1(x_0_0, x_2_0) minus(s(x_0_0), s(x_1_0), z) <= leq_nat(x_0_0, x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; plus -> [ plus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(s(x_0_0), z) <= True _r_1(z, s(x_1_0)) <= True _r_2(s(x_0_0), s(x_1_0)) <= True _r_2(z, z) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) plus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0, x_2_0) plus(z, s(x_1_0), s(x_2_0)) <= _r_2(x_1_0, x_2_0) plus(z, z, z) <= True } ] -- Equality automata are defined for: {nat} _| Answer of teacher: leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(x, y) \/ min_ite(x, y, y) <= True : No: () leq_nat(z, s(nn2)) <= True : No: () leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () plus(n, z, n) <= True : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () min_ite(x, y, x) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : Yes: { _dha -> s(_nbmaa_0) ; _eha -> s(z) ; _fha -> s(z) ; _gha -> z ; n1 -> s(s(_sdmaa_0)) ; n2 -> s(_sbmaa_0) } minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : No: () mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : No: () ------------------------------------------- Step 14, which took 0.143936 s (model generation: 0.143298, model checking: 0.000638): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(z), s(z), s(z)) <= True min_ite(s(z), z, z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, 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 <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) False <= max_ite(s(s(z)), s(z), s(z)) /\ min_ite(s(s(z)), s(z), s(z)) /\ plus(s(s(z)), s(z), s(z)) False <= max_ite(s(z), s(s(z)), s(z)) /\ min_ite(s(z), s(s(z)), s(z)) /\ plus(s(z), s(s(z)), s(z)) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(z)) False <= max_ite(z, s(s(z)), s(z)) /\ min_ite(z, s(s(z)), z) False <= max_ite(z, s(z), s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), 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)) False <= plus(s(z), z, s(s(z))) False <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_2(s(x_0_0), s(x_1_0)) <= True _r_2(z, z) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= _r_2(x_1_0, x_2_0) max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { min_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True min_ite(s(x_0_0), z, z) <= True min_ite(z, s(x_1_0), z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(s(x_0_0), z) <= True _r_1(z, s(x_1_0)) <= True leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_1(x_0_0, x_2_0) minus(s(x_0_0), s(x_1_0), z) <= leq_nat(x_0_0, x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; plus -> [ plus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(s(x_0_0), z) <= True _r_1(z, s(x_1_0)) <= True _r_2(s(x_0_0), s(x_1_0)) <= True _r_2(z, z) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) /\ _r_1(x_1_0, x_2_0) plus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0, x_2_0) plus(z, s(x_1_0), s(x_2_0)) <= _r_2(x_1_0, x_2_0) plus(z, z, z) <= True } ] -- Equality automata are defined for: {nat} _| Answer of teacher: leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(x, y) \/ min_ite(x, y, y) <= True : No: () leq_nat(z, s(nn2)) <= True : No: () leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () plus(n, z, n) <= True : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () min_ite(x, y, x) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : Yes: { _dha -> s(_xemaa_0) ; _eha -> s(z) ; _fha -> s(z) ; _gha -> z ; n1 -> s(s(_ihmaa_0)) ; n2 -> s(s(_ihmaa_0)) } minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : No: () mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : No: () ------------------------------------------- Step 15, which took 0.139542 s (model generation: 0.138935, model checking: 0.000607): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(z), s(z), s(z)) <= True min_ite(s(z), z, z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, 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 <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) False <= max_ite(s(s(z)), s(s(z)), s(z)) /\ min_ite(s(s(z)), s(s(z)), s(z)) /\ plus(s(s(z)), s(s(z)), s(z)) False <= max_ite(s(s(z)), s(z), s(z)) /\ min_ite(s(s(z)), s(z), s(z)) /\ plus(s(s(z)), s(z), s(z)) False <= max_ite(s(z), s(s(z)), s(z)) /\ min_ite(s(z), s(s(z)), s(z)) /\ plus(s(z), s(s(z)), s(z)) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(z)) False <= max_ite(z, s(s(z)), s(z)) /\ min_ite(z, s(s(z)), z) False <= max_ite(z, s(z), s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), 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)) False <= plus(s(z), z, s(s(z))) False <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_2(s(x_0_0), s(x_1_0)) <= True _r_2(z, z) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_1_0, x_2_0) max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= _r_2(x_1_0, x_2_0) max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { min_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True min_ite(s(x_0_0), z, z) <= True min_ite(z, s(x_1_0), z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(s(x_0_0), z) <= True _r_1(z, s(x_1_0)) <= True leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_1(x_0_0, x_2_0) minus(s(x_0_0), s(x_1_0), z) <= leq_nat(x_0_0, x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; plus -> [ plus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(s(x_0_0), z) <= True _r_1(z, s(x_1_0)) <= True _r_2(s(x_0_0), s(x_1_0)) <= True _r_2(z, z) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) plus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0, x_2_0) plus(z, s(x_1_0), s(x_2_0)) <= _r_2(x_1_0, x_2_0) plus(z, z, z) <= True } ] -- Equality automata are defined for: {nat} _| Answer of teacher: leq_nat(x, y) \/ max_ite(x, y, x) <= True : Yes: { x -> s(s(_rkmaa_0)) ; y -> s(z) } leq_nat(x, y) \/ min_ite(x, y, y) <= True : No: () leq_nat(z, s(nn2)) <= True : No: () leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () plus(n, z, n) <= True : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () min_ite(x, y, x) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : Yes: { _dha -> z ; _eha -> s(z) ; _fha -> s(s(_zkmaa_0)) ; _gha -> s(s(_zkmaa_0)) ; n1 -> s(z) ; n2 -> z } minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : No: () mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : No: () ------------------------------------------- Step 16, which took 0.143093 s (model generation: 0.142522, model checking: 0.000571): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(z), s(z), s(z)) <= True min_ite(s(z), z, z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, 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 <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) False <= max_ite(s(s(z)), s(s(z)), s(z)) /\ min_ite(s(s(z)), s(s(z)), s(z)) /\ plus(s(s(z)), s(s(z)), s(z)) False <= max_ite(s(s(z)), s(z), s(z)) /\ min_ite(s(s(z)), s(z), s(z)) /\ plus(s(s(z)), s(z), s(z)) False <= max_ite(s(z), s(s(z)), s(z)) /\ min_ite(s(z), s(s(z)), s(z)) /\ plus(s(z), s(s(z)), s(z)) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(z)) False <= max_ite(z, s(s(z)), s(z)) /\ min_ite(z, s(s(z)), z) False <= max_ite(z, s(z), s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), 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)) False <= plus(s(z), z, s(s(z))) False <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { min_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True min_ite(s(x_0_0), z, z) <= True min_ite(z, s(x_1_0), z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { _r_2(s(x_0_0)) <= True leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= leq_nat(x_0_0, x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; plus -> [ plus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True _r_2(s(x_0_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_2_0) plus(s(x_0_0), z, s(x_2_0)) <= _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: {nat} _| Answer of teacher: leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(x, y) \/ min_ite(x, y, y) <= True : No: () leq_nat(z, s(nn2)) <= True : No: () leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () plus(n, z, n) <= True : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () min_ite(x, y, x) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : Yes: { _dha -> s(z) ; _eha -> s(s(_znmaa_0)) ; _fha -> s(_wlmaa_0) ; _gha -> s(s(_ynmaa_0)) ; n1 -> s(_ylmaa_0) ; n2 -> s(_zlmaa_0) } minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : No: () mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : No: () ------------------------------------------- Step 17, which took 0.084528 s (model generation: 0.083798, model checking: 0.000730): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(z), s(z), s(z)) <= True min_ite(s(z), z, z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, 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 <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) False <= max_ite(s(s(z)), s(s(z)), s(z)) /\ min_ite(s(s(z)), s(s(z)), s(z)) /\ plus(s(s(z)), s(s(z)), s(z)) False <= max_ite(s(s(z)), s(z), s(z)) /\ min_ite(s(s(z)), s(z), s(z)) /\ plus(s(s(z)), s(z), s(z)) False <= max_ite(s(z), s(s(z)), s(z)) /\ min_ite(s(z), s(s(z)), s(z)) /\ plus(s(z), s(s(z)), s(z)) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(z)) False <= max_ite(z, s(s(z)), s(z)) /\ min_ite(z, s(s(z)), z) False <= max_ite(z, s(z), s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= minus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), 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)) False <= plus(s(z), z, s(s(z))) False <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_1(z) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0) max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { min_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True min_ite(s(x_0_0), z, z) <= True min_ite(z, s(x_1_0), z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { _r_1(z) <= True _r_2(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_2_0) /\ _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; plus -> [ plus : { _r_1(z) <= True _r_2(s(x_0_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_2_0) plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_2_0) plus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) plus(z, s(x_1_0), s(x_2_0)) <= _r_1(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: {nat} _| Answer of teacher: leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(x, y) \/ min_ite(x, y, y) <= True : No: () leq_nat(z, s(nn2)) <= True : No: () leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : Yes: { u -> s(_zrmaa_0) } minus(z, y, z) <= True : No: () plus(n, z, n) <= True : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : Yes: { x -> z ; y -> s(s(_asmaa_0)) } min_ite(x, y, x) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : Yes: { _dha -> z ; _eha -> s(s(_dsmaa_0)) ; _fha -> s(_tpmaa_0) ; _gha -> s(z) ; n1 -> s(s(_esmaa_0)) ; n2 -> z } minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : No: () mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : No: () ------------------------------------------- Step 18, which took 0.121053 s (model generation: 0.120446, model checking: 0.000607): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(z), s(z), s(z)) <= True min_ite(s(z), z, z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, 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 <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) max_ite(z, s(s(z)), s(s(z))) <= leq_nat(z, s(s(z))) False <= max_ite(s(s(z)), s(s(z)), s(z)) /\ min_ite(s(s(z)), s(s(z)), s(z)) /\ plus(s(s(z)), s(s(z)), s(z)) False <= max_ite(s(s(z)), s(z), s(z)) /\ min_ite(s(s(z)), s(z), s(z)) /\ plus(s(s(z)), s(z), s(z)) False <= max_ite(s(s(z)), z, s(z)) /\ min_ite(s(s(z)), z, z) False <= max_ite(s(z), s(s(z)), s(z)) /\ min_ite(s(z), s(s(z)), s(z)) /\ plus(s(z), s(s(z)), s(z)) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(z)) False <= max_ite(z, s(s(z)), s(z)) /\ min_ite(z, s(s(z)), z) False <= max_ite(z, s(z), s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= minus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), 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)) False <= plus(s(z), z, s(s(z))) False <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= True max_ite(z, s(x_1_0), s(x_2_0)) <= True max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { _r_2(z) <= True min_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True min_ite(s(x_0_0), z, z) <= _r_2(x_0_0) min_ite(z, s(x_1_0), z) <= _r_2(x_1_0) min_ite(z, z, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True _r_2(z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) /\ _r_2(x_2_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_1_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_0_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; plus -> [ plus : { _r_1(s(x_0_0)) <= True _r_2(z) <= 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)) <= _r_1(x_0_0) 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_1(x_1_0) plus(z, s(x_1_0), s(x_2_0)) <= _r_2(x_2_0) plus(z, z, z) <= True } ] -- Equality automata are defined for: {nat} _| Answer of teacher: leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(x, y) \/ min_ite(x, y, y) <= True : Yes: { x -> s(s(_hwmaa_0)) ; y -> z } leq_nat(z, s(nn2)) <= True : No: () leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () plus(n, z, n) <= True : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () min_ite(x, y, x) <= leq_nat(x, y) : Yes: { x -> z ; y -> s(s(_hwmaa_0)) } leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : Yes: { _dha -> s(_btmaa_0) ; _eha -> s(s(_jwmaa_0)) ; _fha -> s(s(_iwmaa_0)) ; _gha -> z ; n1 -> s(_ftmaa_0) ; n2 -> s(_gtmaa_0) } minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : Yes: { _uga -> s(s(_lwmaa_0)) ; u -> s(s(_iwmaa_0)) ; x2 -> z } mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : No: () ------------------------------------------- Step 19, which took 0.149364 s (model generation: 0.148059, model checking: 0.001305): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(s(z)), z) \/ min_ite(s(s(z)), z, z) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(z), s(z), s(z)) <= True min_ite(s(z), z, z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, 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 <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) max_ite(z, s(s(z)), s(s(z))) <= leq_nat(z, s(s(z))) min_ite(z, s(s(z)), z) <= leq_nat(z, s(s(z))) False <= max_ite(s(s(z)), s(s(z)), s(z)) /\ min_ite(s(s(z)), s(s(z)), s(z)) /\ plus(s(s(z)), s(s(z)), s(z)) False <= max_ite(s(s(z)), s(z), s(z)) /\ min_ite(s(s(z)), s(z), s(z)) /\ plus(s(s(z)), s(z), s(z)) False <= max_ite(s(s(z)), z, s(z)) /\ min_ite(s(s(z)), z, z) False <= max_ite(s(z), s(s(z)), s(z)) /\ min_ite(s(z), s(s(z)), s(z)) /\ plus(s(z), s(s(z)), s(z)) False <= max_ite(s(z), s(z), s(s(z))) /\ minus(s(s(z)), s(s(z)), z) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(z)) False <= max_ite(z, s(s(z)), s(z)) /\ min_ite(z, s(s(z)), z) False <= max_ite(z, s(z), s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= minus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), 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)) False <= plus(s(z), z, s(s(z))) False <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(s(x_0_0), z) <= _r_2(x_0_0) _r_1(z, z) <= True _r_2(s(x_0_0)) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { min_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True min_ite(s(x_0_0), z, z) <= True min_ite(z, s(x_1_0), z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(s(x_0_0), z) <= _r_2(x_0_0) _r_1(z, z) <= True _r_2(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0, x_1_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; plus -> [ plus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(s(x_0_0), z) <= _r_2(x_0_0) _r_1(z, z) <= True _r_2(s(x_0_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_2_0) plus(s(x_0_0), z, s(x_2_0)) <= _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: {nat} _| Answer of teacher: leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(x, y) \/ min_ite(x, y, y) <= True : No: () leq_nat(z, s(nn2)) <= True : No: () leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () plus(n, z, n) <= True : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : Yes: { x -> s(z) ; y -> s(s(_sbnaa_0)) } min_ite(x, y, x) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : Yes: { _dha -> s(_yxmaa_0) ; _eha -> s(s(_kbnaa_0)) ; _fha -> s(s(_bcnaa_0)) ; _gha -> z ; n1 -> s(s(_acnaa_0)) ; n2 -> s(_dymaa_0) } minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : No: () mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : No: () ------------------------------------------- Step 20, which took 0.251193 s (model generation: 0.250004, model checking: 0.001189): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(s(z)), z) \/ min_ite(s(s(z)), z, z) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(s(z)), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(z), s(z), s(z)) <= True min_ite(s(z), z, z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, 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 <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) max_ite(z, s(s(z)), s(s(z))) <= leq_nat(z, s(s(z))) min_ite(z, s(s(z)), z) <= leq_nat(z, s(s(z))) False <= max_ite(s(s(z)), s(s(z)), s(z)) /\ min_ite(s(s(z)), s(s(z)), s(z)) /\ plus(s(s(z)), s(s(z)), s(z)) False <= max_ite(s(s(z)), s(z), s(z)) /\ min_ite(s(s(z)), s(z), s(z)) /\ plus(s(s(z)), s(z), s(z)) False <= max_ite(s(s(z)), z, s(z)) /\ min_ite(s(s(z)), z, z) False <= max_ite(s(z), s(s(z)), s(z)) /\ min_ite(s(z), s(s(z)), s(z)) /\ plus(s(z), s(s(z)), s(z)) False <= max_ite(s(z), s(z), s(s(z))) /\ minus(s(s(z)), s(s(z)), z) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(z)) False <= max_ite(z, s(s(z)), s(z)) /\ min_ite(z, s(s(z)), z) False <= max_ite(z, s(z), s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= min_ite(s(s(z)), s(z), s(z)) /\ minus(s(s(z)), s(s(z)), z) /\ plus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), 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)) False <= plus(s(z), z, s(s(z))) False <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(s(x_0_0), z) <= _r_2(x_0_0) _r_1(z, z) <= True _r_2(s(x_0_0)) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { min_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True min_ite(s(x_0_0), z, z) <= True min_ite(z, s(x_1_0), z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(s(x_0_0), z) <= _r_2(x_0_0) _r_1(z, z) <= True _r_2(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0, x_1_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; plus -> [ plus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(s(x_0_0), z) <= _r_2(x_0_0) _r_1(z, z) <= True _r_2(s(x_0_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_2(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)) <= _r_1(x_1_0, x_2_0) plus(z, z, z) <= True } ] -- Equality automata are defined for: {nat} _| Answer of teacher: leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(x, y) \/ min_ite(x, y, y) <= True : No: () leq_nat(z, s(nn2)) <= True : No: () leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () plus(n, z, n) <= True : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () min_ite(x, y, x) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : Yes: { _dha -> s(_senaa_0) ; _eha -> s(s(_kinaa_0)) ; _fha -> s(s(_hjnaa_0)) ; _gha -> z ; n1 -> s(s(_ijnaa_0)) ; n2 -> s(s(_gjnaa_0)) } minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : No: () mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : Yes: { _fga -> s(s(_kinaa_0)) ; mm -> s(z) ; n -> s(z) } ------------------------------------------- Step 21, which took 1.128481 s (model generation: 1.127659, model checking: 0.000822): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(s(z)), z) \/ min_ite(s(s(z)), z, z) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(s(z)), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(z), s(z), s(z)) <= True min_ite(s(z), z, z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True plus(s(s(z)), z, s(s(z))) <= True plus(s(z), s(s(z)), s(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 <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) max_ite(z, s(s(z)), s(s(z))) <= leq_nat(z, s(s(z))) min_ite(z, s(s(z)), z) <= leq_nat(z, s(s(z))) False <= max_ite(s(s(z)), s(s(z)), s(s(z))) /\ min_ite(s(s(z)), s(s(z)), s(z)) /\ minus(s(s(z)), s(s(z)), z) /\ plus(s(s(z)), s(s(z)), s(s(z))) False <= max_ite(s(s(z)), s(s(z)), s(z)) /\ min_ite(s(s(z)), s(s(z)), s(z)) /\ plus(s(s(z)), s(s(z)), s(z)) False <= max_ite(s(s(z)), s(z), s(z)) /\ min_ite(s(s(z)), s(z), s(z)) /\ plus(s(s(z)), s(z), s(z)) False <= max_ite(s(s(z)), z, s(z)) /\ min_ite(s(s(z)), z, z) False <= max_ite(s(z), s(s(z)), s(z)) /\ min_ite(s(z), s(s(z)), s(z)) /\ plus(s(z), s(s(z)), s(z)) False <= max_ite(s(z), s(z), s(s(z))) /\ minus(s(s(z)), s(s(z)), z) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(z)) False <= max_ite(z, s(s(z)), s(z)) /\ min_ite(z, s(s(z)), z) False <= max_ite(z, s(z), s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= min_ite(s(s(z)), s(z), s(z)) /\ minus(s(s(z)), s(s(z)), z) /\ plus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), 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)) False <= plus(s(z), z, s(s(z))) False <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { min_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True min_ite(s(x_0_0), z, z) <= True min_ite(z, s(x_1_0), z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True _r_2(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0, x_1_0) _r_2(s(x_0_0), z) <= True _r_2(z, s(x_1_0)) <= True leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0, x_1_0) /\ _r_2(x_0_0, x_2_0) minus(s(x_0_0), s(x_1_0), z) <= leq_nat(x_0_0, x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; plus -> [ plus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True _r_2(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0, x_1_0) _r_2(s(x_0_0), z) <= True _r_2(z, s(x_1_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0, x_2_0) /\ _r_2(x_1_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)) <= _r_1(x_1_0, x_2_0) plus(z, z, z) <= True } ] -- Equality automata are defined for: {nat} _| Answer of teacher: leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(x, y) \/ min_ite(x, y, y) <= True : No: () leq_nat(z, s(nn2)) <= True : No: () leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () plus(n, z, n) <= True : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () min_ite(x, y, x) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : Yes: { _dha -> z ; _eha -> s(s(z)) ; _fha -> s(s(s(_tnnaa_0))) ; _gha -> s(z) ; n1 -> z ; n2 -> s(s(_knnaa_0)) } minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : Yes: { _uga -> s(s(z)) ; u -> s(z) ; x2 -> s(s(_mpnaa_0)) } mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : Yes: { _fga -> s(z) ; mm -> s(s(_nonaa_0)) ; n -> s(s(z)) } ------------------------------------------- Step 22, which took 23.266465 s (model generation: 23.263269, model checking: 0.003196): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(s(z)), z) \/ min_ite(s(s(z)), z, z) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(s(z)), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(z), s(z), s(z)) <= True min_ite(s(z), z, z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True plus(s(s(z)), z, s(s(z))) <= True plus(s(z), s(s(z)), s(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 <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) max_ite(z, s(s(z)), s(s(z))) <= leq_nat(z, s(s(z))) min_ite(z, s(s(z)), z) <= leq_nat(z, s(s(z))) False <= max_ite(s(s(z)), s(s(z)), s(s(z))) /\ min_ite(s(s(z)), s(s(z)), s(z)) /\ minus(s(s(z)), s(s(z)), z) /\ plus(s(s(z)), s(s(z)), s(s(z))) False <= max_ite(s(s(z)), s(s(z)), s(z)) /\ min_ite(s(s(z)), s(s(z)), s(z)) /\ plus(s(s(z)), s(s(z)), s(z)) False <= max_ite(s(s(z)), s(z), s(z)) /\ min_ite(s(s(z)), s(z), s(z)) /\ plus(s(s(z)), s(z), s(z)) False <= max_ite(s(s(z)), z, s(z)) /\ min_ite(s(s(z)), z, z) False <= max_ite(s(z), s(s(z)), s(z)) /\ min_ite(s(z), s(s(z)), s(z)) /\ plus(s(z), s(s(z)), s(z)) False <= max_ite(s(z), s(z), s(s(z))) /\ minus(s(s(z)), s(s(z)), z) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(z)) False <= max_ite(z, s(s(z)), s(s(s(z)))) /\ min_ite(z, s(s(z)), z) /\ minus(s(s(z)), s(s(s(z))), s(z)) False <= max_ite(z, s(s(z)), s(z)) /\ min_ite(z, s(s(z)), z) False <= max_ite(z, s(z), s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= min_ite(s(s(z)), s(z), s(z)) /\ minus(s(s(z)), s(s(z)), z) /\ plus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), z) minus(s(s(z)), s(s(s(z))), s(s(z))) <= minus(s(z), s(s(z)), s(s(z))) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) plus(s(s(z)), s(s(s(z))), s(s(z))) <= plus(s(s(z)), s(s(z)), 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)) False <= plus(s(z), z, s(s(z))) False <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_1(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0) _r_1(z, z) <= True _r_2(s(x_0_0)) <= True leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= plus(x_0_0, x_1_0, x_2_0) max_ite(s(x_0_0), z, s(x_2_0)) <= leq_nat(x_0_0, x_2_0) max_ite(z, s(x_1_0), s(x_2_0)) <= leq_nat(x_1_0, x_2_0) max_ite(z, z, z) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_2_0) plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_1_0) plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) plus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) /\ _r_2(x_2_0) plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) plus(z, s(x_1_0), s(x_2_0)) <= _r_2(x_1_0) plus(z, z, z) <= True } ] ; min_ite -> [ min_ite : { min_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True min_ite(s(x_0_0), z, z) <= True min_ite(z, s(x_1_0), z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0) _r_1(z, z) <= True _r_2(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_1_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0, x_1_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; plus -> [ plus : { _r_1(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0) _r_1(z, z) <= True _r_2(s(x_0_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_2_0) plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_1_0) plus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) plus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) /\ _r_2(x_2_0) plus(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, 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: {nat} _| Answer of teacher: leq_nat(x, y) \/ max_ite(x, y, x) <= True : Yes: { x -> s(s(s(_mcoaa_0))) ; y -> s(s(z)) } leq_nat(x, y) \/ min_ite(x, y, y) <= True : No: () leq_nat(z, s(nn2)) <= True : No: () leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () plus(n, z, n) <= True : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : Yes: { x -> s(s(z)) ; y -> s(s(z)) } min_ite(x, y, x) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : Yes: { _dha -> z ; _eha -> s(s(s(_vboaa_0))) ; _fha -> s(s(z)) ; _gha -> s(s(_udoaa_0)) ; n1 -> z ; n2 -> s(s(z)) } minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : No: () mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : Yes: { _fga -> s(s(_lcoaa_0)) ; mm -> z ; n -> s(s(_rdoaa_0)) } ------------------------------------------- Step 23, which took 21.340420 s (model generation: 21.338986, model checking: 0.001434): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(s(s(z))), s(s(z))) \/ max_ite(s(s(s(z))), s(s(z)), s(s(s(z)))) <= True leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(s(z)), z) \/ min_ite(s(s(z)), z, z) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(s(z)), s(s(z))) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(s(z)), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(z), s(z), s(z)) <= True min_ite(s(z), z, z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, 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(s(z)), s(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 <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(z), z) max_ite(z, s(s(z)), s(s(z))) <= leq_nat(z, s(s(z))) min_ite(z, s(s(z)), z) <= leq_nat(z, s(s(z))) False <= max_ite(s(s(z)), s(s(z)), s(z)) /\ min_ite(s(s(z)), s(s(z)), s(z)) /\ plus(s(s(z)), s(s(z)), s(z)) False <= max_ite(s(s(z)), s(z), s(z)) /\ min_ite(s(s(z)), s(z), s(z)) /\ plus(s(s(z)), s(z), s(z)) False <= max_ite(s(s(z)), z, s(z)) /\ min_ite(s(s(z)), z, z) False <= max_ite(s(z), s(s(z)), s(z)) /\ min_ite(s(z), s(s(z)), s(z)) /\ plus(s(z), s(s(z)), s(z)) False <= max_ite(s(z), s(z), s(s(z))) /\ minus(s(s(z)), s(s(z)), z) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(z)) False <= max_ite(z, s(s(z)), s(s(s(z)))) /\ min_ite(z, s(s(z)), z) /\ minus(s(s(z)), s(s(s(z))), s(z)) False <= max_ite(z, s(s(z)), s(s(z))) /\ min_ite(z, s(s(z)), z) /\ minus(s(s(s(z))), s(s(z)), s(s(z))) /\ plus(z, s(s(z)), s(s(s(z)))) False <= max_ite(z, s(s(z)), s(z)) /\ min_ite(z, s(s(z)), z) False <= max_ite(z, s(z), s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= min_ite(s(s(z)), s(s(z)), s(z)) /\ minus(s(s(z)), s(s(z)), z) /\ plus(s(s(z)), s(s(z)), s(s(z))) False <= min_ite(s(s(z)), s(z), s(z)) /\ minus(s(s(z)), s(s(z)), z) /\ plus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), z) minus(s(s(z)), s(s(s(z))), s(s(z))) <= minus(s(z), s(s(z)), s(s(z))) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) plus(s(s(z)), s(s(s(z))), s(s(z))) <= plus(s(s(z)), s(s(z)), 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)) False <= plus(s(z), z, s(s(z))) False <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None leq_nat -> [ leq_nat : { _r_1(s(x_0_0)) <= True _r_2(s(x_0_0)) <= _r_1(x_0_0) _r_2(z) <= True leq_nat(s(x_0_0), s(x_1_0)) <= _r_1(x_1_0) leq_nat(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0) leq_nat(s(x_0_0), z) <= _r_1(x_0_0) leq_nat(z, s(x_1_0)) <= _r_2(x_1_0) leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_1(s(x_0_0)) <= True _r_2(s(x_0_0)) <= _r_1(x_0_0) _r_2(z) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True max_ite(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) max_ite(z, s(x_1_0), s(x_2_0)) <= _r_2(x_1_0) max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { min_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True min_ite(s(x_0_0), z, z) <= True min_ite(z, s(x_1_0), z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True _r_2(s(x_0_0)) <= _r_1(x_0_0) _r_2(z) <= True leq_nat(s(x_0_0), s(x_1_0)) <= _r_1(x_1_0) leq_nat(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0) leq_nat(s(x_0_0), z) <= _r_1(x_0_0) leq_nat(z, s(x_1_0)) <= _r_2(x_1_0) leq_nat(z, z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) /\ _r_2(x_2_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) /\ leq_nat(x_0_0, x_1_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_1_0) /\ leq_nat(x_0_0, x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; plus -> [ plus : { _r_1(s(x_0_0)) <= True _r_2(s(x_0_0)) <= _r_1(x_0_0) _r_2(z) <= 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)) <= _r_1(x_0_0) 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_1(x_1_0) plus(z, s(x_1_0), s(x_2_0)) <= _r_2(x_2_0) plus(z, z, z) <= True } ] -- Equality automata are defined for: {nat} _| Answer of teacher: leq_nat(x, y) \/ max_ite(x, y, x) <= True : Yes: { x -> z ; y -> s(s(z)) } leq_nat(x, y) \/ min_ite(x, y, y) <= True : Yes: { x -> z ; y -> s(s(z)) } leq_nat(z, s(nn2)) <= True : Yes: { nn2 -> s(z) } leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () plus(n, z, n) <= True : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : Yes: { x -> s(s(_qmoaa_0)) ; y -> z } min_ite(x, y, x) <= leq_nat(x, y) : Yes: { x -> s(s(_qmoaa_0)) ; y -> z } leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : Yes: { nn1 -> z ; nn2 -> s(s(z)) } False <= leq_nat(s(nn1), z) : Yes: { nn1 -> s(_qmoaa_0) } eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : Yes: { _dha -> z ; _eha -> s(s(s(_smoaa_0))) ; _fha -> s(_phoaa_0) ; _gha -> s(z) ; n1 -> s(z) ; n2 -> z } minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : Yes: { _uga -> z ; u -> s(z) ; x2 -> s(z) } mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : No: () ------------------------------------------- Step 24, which took 12.031878 s (model generation: 12.030137, model checking: 0.001741): Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(s(s(z))), s(s(z))) \/ max_ite(s(s(s(z))), s(s(z)), s(s(s(z)))) <= True leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(s(z))) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(s(z)), s(s(z))) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(s(z)), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(s(z)), s(s(z))) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(s(z)), z, z) <= True min_ite(s(z), s(z), s(z)) <= True min_ite(s(z), z, z) <= True min_ite(z, s(s(z)), z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, 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(s(z)), s(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 <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(s(z)), z) False <= leq_nat(s(z), z) False <= max_ite(s(s(z)), s(s(z)), s(z)) /\ min_ite(s(s(z)), s(s(z)), s(z)) /\ plus(s(s(z)), s(s(z)), s(z)) False <= max_ite(s(s(z)), s(z), s(z)) /\ min_ite(s(s(z)), s(z), s(z)) /\ plus(s(s(z)), s(z), s(z)) False <= max_ite(s(s(z)), z, s(z)) False <= max_ite(s(z), s(s(z)), s(z)) /\ min_ite(s(z), s(s(z)), s(z)) /\ plus(s(z), s(s(z)), s(z)) False <= max_ite(s(z), s(z), s(s(z))) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(z)) False <= max_ite(z, s(s(z)), s(s(s(z)))) /\ minus(s(s(z)), s(s(s(z))), s(z)) False <= max_ite(z, s(s(z)), s(z)) False <= max_ite(z, s(z), s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= min_ite(s(s(z)), s(s(z)), s(z)) /\ plus(s(s(z)), s(s(z)), s(s(z))) False <= min_ite(s(s(z)), s(z), s(z)) /\ plus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(s(z))), s(s(z)), s(s(z))) /\ plus(z, s(s(z)), s(s(s(z)))) False <= minus(s(s(s(z))), s(z), s(z)) /\ plus(s(z), z, s(s(s(z)))) False <= minus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), z) minus(s(s(z)), s(s(s(z))), s(s(z))) <= minus(s(z), s(s(z)), s(s(z))) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) plus(s(s(z)), s(s(s(z))), s(s(z))) <= plus(s(s(z)), s(s(z)), 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)) False <= plus(s(z), z, s(s(z))) False <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0) _r_1(s(x_0_0), z) <= _r_2(x_0_0) _r_1(z, z) <= True _r_2(s(x_0_0)) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True min_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= leq_nat(x_0_0, x_2_0) min_ite(s(x_0_0), z, z) <= True min_ite(z, s(x_1_0), z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0) _r_1(s(x_0_0), z) <= _r_2(x_0_0) _r_1(z, z) <= True _r_2(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0, x_1_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; plus -> [ plus : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0) _r_1(s(x_0_0), z) <= _r_2(x_0_0) _r_1(z, z) <= True _r_2(s(x_0_0)) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_2_0) plus(s(x_0_0), z, s(x_2_0)) <= _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: {nat} _| Answer of teacher: leq_nat(x, y) \/ max_ite(x, y, x) <= True : No: () leq_nat(x, y) \/ min_ite(x, y, y) <= True : Yes: { x -> s(s(_auoaa_0)) ; y -> s(z) } leq_nat(z, s(nn2)) <= True : No: () leq_nat(z, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () plus(n, z, n) <= True : No: () leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) : No: () max_ite(x, y, y) <= leq_nat(x, y) : No: () min_ite(x, y, x) <= leq_nat(x, y) : No: () leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) : No: () False <= leq_nat(s(nn1), z) : No: () eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) : Yes: { _dha -> s(z) ; _eha -> s(s(_guoaa_0)) ; _fha -> s(s(z)) ; _gha -> z ; n1 -> s(z) ; n2 -> s(s(z)) } minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) : No: () mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) : No: () plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) : No: () Total time: 60.575028 Learner time: 59.524474 Teacher time: 0.018276 Reasons for stopping: Maybe: timeout during teacher: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> out of time leq_nat(x, y) \/ min_ite(x, y, y) <= True -> out of time leq_nat(z, s(nn2)) <= True -> out of time leq_nat(z, z) <= True -> out of time minus(s(u), z, s(u)) <= True -> out of time minus(z, y, z) <= True -> out of time plus(n, z, n) <= True -> out of time leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> out of time max_ite(x, y, y) <= leq_nat(x, y) -> out of time min_ite(x, y, x) <= leq_nat(x, y) -> out of time leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> out of time False <= leq_nat(s(nn1), z) -> out of time eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> out of time minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> out of time mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> out of time plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> out of time }Last solver state: Clauses: { leq_nat(x, y) \/ max_ite(x, y, x) <= True -> 0 leq_nat(x, y) \/ min_ite(x, y, y) <= True -> 0 leq_nat(z, s(nn2)) <= True -> 0 leq_nat(z, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 plus(n, z, n) <= True -> 0 leq_nat(s(nn1), s(nn2)) <= leq_nat(nn1, nn2) -> 0 max_ite(x, y, y) <= leq_nat(x, y) -> 0 min_ite(x, y, x) <= leq_nat(x, y) -> 0 leq_nat(nn1, nn2) <= leq_nat(s(nn1), s(nn2)) -> 0 False <= leq_nat(s(nn1), z) -> 0 eq_nat(_dha, _gha) <= max_ite(n1, n2, _fha) /\ min_ite(n1, n2, _dha) /\ minus(_eha, _fha, _gha) /\ plus(n1, n2, _eha) -> 0 minus(s(u), s(x2), _uga) <= minus(u, x2, _uga) -> 0 mult(n, s(mm), _lga) <= mult(n, mm, _kga) /\ plus(n, _kga, _lga) -> 0 plus(n, s(mm), s(_fga)) <= plus(n, mm, _fga) -> 0 } Accumulated learning constraints: { leq_nat(s(s(s(z))), s(s(z))) \/ max_ite(s(s(s(z))), s(s(z)), s(s(s(z)))) <= True leq_nat(s(s(z)), s(s(z))) <= True leq_nat(s(z), s(s(z))) <= True leq_nat(s(z), s(z)) <= True leq_nat(z, s(s(z))) <= True leq_nat(z, s(z)) <= True leq_nat(z, z) <= True max_ite(s(s(z)), s(s(z)), s(s(z))) <= True max_ite(s(s(z)), s(z), s(s(z))) <= True max_ite(s(z), s(s(z)), s(s(z))) <= True max_ite(s(z), s(z), s(z)) <= True max_ite(s(z), z, s(z)) <= True max_ite(z, s(s(z)), s(s(z))) <= True max_ite(z, s(z), s(z)) <= True max_ite(z, z, z) <= True min_ite(s(s(z)), s(z), s(z)) <= True min_ite(s(s(z)), z, z) <= True min_ite(s(z), s(z), s(z)) <= True min_ite(s(z), z, z) <= True min_ite(z, s(s(z)), z) <= True min_ite(z, s(z), z) <= True min_ite(z, z, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, 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(s(z)), s(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 <= leq_nat(s(s(z)), s(z)) False <= leq_nat(s(s(z)), z) False <= leq_nat(s(z), z) False <= max_ite(s(s(z)), s(s(z)), s(z)) /\ min_ite(s(s(z)), s(s(z)), s(z)) /\ plus(s(s(z)), s(s(z)), s(z)) False <= max_ite(s(s(z)), s(z), s(z)) /\ plus(s(s(z)), s(z), s(z)) False <= max_ite(s(s(z)), z, s(z)) False <= max_ite(s(z), s(s(z)), s(z)) /\ min_ite(s(z), s(s(z)), s(z)) /\ plus(s(z), s(s(z)), s(z)) False <= max_ite(s(z), s(z), s(s(z))) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= max_ite(s(z), z, s(s(z))) /\ minus(s(z), s(s(z)), s(z)) False <= max_ite(z, s(s(z)), s(s(s(z)))) /\ minus(s(s(z)), s(s(s(z))), s(z)) False <= max_ite(z, s(s(z)), s(z)) False <= max_ite(z, s(z), s(s(z))) /\ minus(s(z), s(s(z)), s(s(z))) False <= min_ite(s(s(z)), s(s(z)), s(z)) /\ plus(s(s(z)), s(s(z)), s(s(z))) False <= min_ite(s(z), s(s(z)), s(z)) /\ plus(s(z), s(s(z)), s(s(z))) False <= minus(s(s(s(z))), s(s(z)), s(s(z))) /\ plus(z, s(s(z)), s(s(s(z)))) False <= minus(s(s(s(z))), s(z), s(z)) /\ plus(s(z), z, s(s(s(z)))) False <= minus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), z) minus(s(s(z)), s(s(s(z))), s(s(z))) <= minus(s(z), s(s(z)), s(s(z))) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) plus(s(s(z)), s(s(s(z))), s(s(z))) <= plus(s(s(z)), s(s(z)), s(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)) False <= plus(s(z), z, s(s(z))) False <= plus(z, s(z), s(s(z))) } Current best model: |_ name: None leq_nat -> [ leq_nat : { leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True } ] ; max_ite -> [ max_ite : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(z, z) <= True max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) max_ite(z, s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) max_ite(z, z, z) <= True } ] ; min_ite -> [ min_ite : { min_ite(s(x_0_0), s(x_1_0), s(x_2_0)) <= True min_ite(s(x_0_0), z, z) <= True min_ite(z, s(x_1_0), z) <= True min_ite(z, z, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(z, z) <= True _r_2(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0, x_1_0) _r_2(s(x_0_0), z) <= True _r_2(z, s(x_1_0)) <= True leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_1_0, x_2_0) /\ leq_nat(x_0_0, x_1_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0, x_1_0) /\ _r_2(x_0_0, x_2_0) minus(s(x_0_0), s(x_1_0), z) <= leq_nat(x_0_0, x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; mult -> [ mult : { } ] ; 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 _r_2(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0, x_1_0) _r_2(s(x_0_0), z) <= True _r_2(z, s(x_1_0)) <= True leq_nat(s(x_0_0), s(x_1_0)) <= leq_nat(x_0_0, x_1_0) leq_nat(z, s(x_1_0)) <= True leq_nat(z, z) <= True plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_0_0, x_2_0) /\ leq_nat(x_1_0, x_2_0) plus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0, x_1_0) /\ _r_2(x_0_0, x_2_0) /\ _r_2(x_1_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)) <= _r_1(x_1_0, x_2_0) plus(z, z, z) <= True } ] -- Equality automata are defined for: {nat} _|