Inference procedure has parameters: Ice fuel: 200 Timeout: 60s Convolution: left Learning problem is: env: { nat -> {s, z} ; natlist -> {cons, nil} } definition: { (append, F: {() -> append([nil, l2, l2]) (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)])} (append([_oda, _pda, _qda]) /\ append([_oda, _pda, _rda])) -> eq_natlist([_qda, _rda]) ) (reverse, F: {() -> reverse([nil, nil]) (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda])} (reverse([_uda, _vda]) /\ reverse([_uda, _wda])) -> eq_natlist([_vda, _wda]) ) (leq, P: {() -> leq([z, s(nn2)]) () -> leq([z, z]) (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) (leq([s(nn1), z])) -> BOT} ) (length, F: {() -> length([nil, z]) (length([ll, _xda])) -> length([cons(x, ll), s(_xda)])} (length([_yda, _aea]) /\ length([_yda, _zda])) -> eq_nat([_zda, _aea]) ) } properties: {(length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea])} over-approximation: {append, length, reverse} under-approximation: {leq} Clause system for inference is: { () -> append([nil, l2, l2]) -> 0 () -> length([nil, z]) -> 0 () -> leq([z, s(nn2)]) -> 0 () -> leq([z, z]) -> 0 () -> reverse([nil, nil]) -> 0 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 0 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 0 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 0 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 0 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 0 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 0 (leq([s(nn1), z])) -> BOT -> 0 } Solving took 60.004326 seconds. DontKnow. Stopped because: timeout Working model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8092, q_gen_8093, q_gen_8094, q_gen_8097, q_gen_8098, q_gen_8099, q_gen_8100, q_gen_8106, q_gen_8107, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8111, q_gen_8117, q_gen_8118, q_gen_8119, q_gen_8130, q_gen_8131, q_gen_8132, q_gen_8133, q_gen_8134, q_gen_8148, q_gen_8149, q_gen_8150, q_gen_8156, q_gen_8157, q_gen_8158, q_gen_8159, q_gen_8160, q_gen_8161, q_gen_8162, q_gen_8163, q_gen_8171, q_gen_8172, q_gen_8176, q_gen_8177, q_gen_8178, q_gen_8187, q_gen_8188, q_gen_8189, q_gen_8192, q_gen_8193, q_gen_8201, q_gen_8202, q_gen_8203, q_gen_8204, q_gen_8205, q_gen_8212, q_gen_8213, q_gen_8214, q_gen_8215, q_gen_8216, q_gen_8217, q_gen_8221}, Q_f={}, Delta= { () -> q_gen_8108 () -> q_gen_8109 (q_gen_8109, q_gen_8108) -> q_gen_8132 (q_gen_8109) -> q_gen_8159 (q_gen_8159, q_gen_8108) -> q_gen_8163 () -> q_gen_8093 () -> q_gen_8094 (q_gen_8099, q_gen_8093) -> q_gen_8098 (q_gen_8094) -> q_gen_8099 (q_gen_8109, q_gen_8108) -> q_gen_8118 (q_gen_8109, q_gen_8132) -> q_gen_8134 (q_gen_8159, q_gen_8163) -> q_gen_8162 (q_gen_8094, q_gen_8093) -> q_gen_8188 (q_gen_8159, q_gen_8108) -> q_gen_8215 (q_gen_8109) -> q_gen_8216 () -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8099, q_gen_8098) -> q_gen_8097 (q_gen_8094, q_gen_8093) -> q_gen_8100 (q_gen_8110, q_gen_8107) -> q_gen_8106 (q_gen_8109, q_gen_8108) -> q_gen_8107 () -> q_gen_8110 (q_gen_8099, q_gen_8093) -> q_gen_8111 (q_gen_8094, q_gen_8118) -> q_gen_8117 (q_gen_8094, q_gen_8118) -> q_gen_8119 (q_gen_8110, q_gen_8131) -> q_gen_8130 (q_gen_8109, q_gen_8132) -> q_gen_8131 (q_gen_8094, q_gen_8134) -> q_gen_8133 (q_gen_8149, q_gen_8107) -> q_gen_8148 (q_gen_8094) -> q_gen_8149 (q_gen_8110, q_gen_8087) -> q_gen_8150 (q_gen_8099, q_gen_8118) -> q_gen_8156 (q_gen_8160, q_gen_8158) -> q_gen_8157 (q_gen_8159, q_gen_8132) -> q_gen_8158 (q_gen_8110) -> q_gen_8160 (q_gen_8094, q_gen_8162) -> q_gen_8161 (q_gen_8149, q_gen_8117) -> q_gen_8171 (q_gen_8110, q_gen_8092) -> q_gen_8172 (q_gen_8149, q_gen_8087) -> q_gen_8176 (q_gen_8110, q_gen_8178) -> q_gen_8177 (q_gen_8099, q_gen_8093) -> q_gen_8178 (q_gen_8094, q_gen_8188) -> q_gen_8187 (q_gen_8149, q_gen_8119) -> q_gen_8189 (q_gen_8110, q_gen_8119) -> q_gen_8192 (q_gen_8110, q_gen_8130) -> q_gen_8193 (q_gen_8160, q_gen_8092) -> q_gen_8201 (q_gen_8204, q_gen_8203) -> q_gen_8202 (q_gen_8099, q_gen_8188) -> q_gen_8203 (q_gen_8109) -> q_gen_8204 (q_gen_8160, q_gen_8107) -> q_gen_8205 (q_gen_8094, q_gen_8098) -> q_gen_8212 (q_gen_8149, q_gen_8214) -> q_gen_8213 (q_gen_8216, q_gen_8215) -> q_gen_8214 (q_gen_8216, q_gen_8093) -> q_gen_8217 (q_gen_8094, q_gen_8134) -> q_gen_8221 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8089, q_gen_8090, q_gen_8091, q_gen_8103, q_gen_8104, q_gen_8105, q_gen_8114, q_gen_8115, q_gen_8116, q_gen_8124, q_gen_8125, q_gen_8126, q_gen_8127, q_gen_8138, q_gen_8139, q_gen_8140, q_gen_8141, q_gen_8142, q_gen_8143, q_gen_8144, q_gen_8153, q_gen_8154, q_gen_8155, q_gen_8168, q_gen_8169, q_gen_8170, q_gen_8175, q_gen_8182, q_gen_8184, q_gen_8185, q_gen_8186, q_gen_8191, q_gen_8194, q_gen_8195, q_gen_8196, q_gen_8207, q_gen_8208, q_gen_8209, q_gen_8210, q_gen_8220, q_gen_8222, q_gen_8223, q_gen_8224, q_gen_8225}, Q_f={}, Delta= { () -> q_gen_8090 () -> q_gen_8105 (q_gen_8105) -> q_gen_8116 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8105, q_gen_8125) -> q_gen_8139 (q_gen_8116, q_gen_8090) -> q_gen_8155 (q_gen_8116) -> q_gen_8186 (q_gen_8105, q_gen_8155) -> q_gen_8209 (q_gen_8116, q_gen_8155) -> q_gen_8224 () -> q_gen_8086 (q_gen_8091, q_gen_8090) -> q_gen_8089 () -> q_gen_8091 (q_gen_8104, q_gen_8090) -> q_gen_8103 (q_gen_8105) -> q_gen_8104 (q_gen_8115, q_gen_8090) -> q_gen_8114 (q_gen_8116) -> q_gen_8115 (q_gen_8126, q_gen_8125) -> q_gen_8124 (q_gen_8105) -> q_gen_8126 (q_gen_8126, q_gen_8090) -> q_gen_8127 (q_gen_8140, q_gen_8139) -> q_gen_8138 (q_gen_8126) -> q_gen_8140 (q_gen_8140, q_gen_8125) -> q_gen_8141 (q_gen_8143, q_gen_8090) -> q_gen_8142 (q_gen_8144) -> q_gen_8143 (q_gen_8116) -> q_gen_8144 (q_gen_8140, q_gen_8090) -> q_gen_8153 (q_gen_8143, q_gen_8155) -> q_gen_8154 (q_gen_8169, q_gen_8139) -> q_gen_8168 (q_gen_8170) -> q_gen_8169 (q_gen_8091) -> q_gen_8170 (q_gen_8091, q_gen_8125) -> q_gen_8175 (q_gen_8170, q_gen_8125) -> q_gen_8182 (q_gen_8185, q_gen_8090) -> q_gen_8184 (q_gen_8186) -> q_gen_8185 (q_gen_8144, q_gen_8090) -> q_gen_8191 (q_gen_8144, q_gen_8125) -> q_gen_8194 (q_gen_8196, q_gen_8139) -> q_gen_8195 (q_gen_8186) -> q_gen_8196 (q_gen_8126, q_gen_8155) -> q_gen_8207 (q_gen_8144, q_gen_8209) -> q_gen_8208 (q_gen_8196, q_gen_8125) -> q_gen_8210 (q_gen_8196, q_gen_8155) -> q_gen_8220 (q_gen_8104, q_gen_8155) -> q_gen_8222 (q_gen_8170, q_gen_8224) -> q_gen_8223 (q_gen_8091, q_gen_8155) -> q_gen_8225 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8084, q_gen_8085, q_gen_8088, q_gen_8095, q_gen_8096, q_gen_8128, q_gen_8129, q_gen_8146, q_gen_8147, q_gen_8199, q_gen_8200, q_gen_8211}, Q_f={}, Delta= { () -> q_gen_8085 (q_gen_8085) -> q_gen_8096 () -> q_gen_8083 (q_gen_8085) -> q_gen_8084 (q_gen_8083) -> q_gen_8088 (q_gen_8096) -> q_gen_8095 (q_gen_8129) -> q_gen_8128 (q_gen_8085) -> q_gen_8129 (q_gen_8147) -> q_gen_8146 (q_gen_8128) -> q_gen_8147 (q_gen_8200) -> q_gen_8199 (q_gen_8096) -> q_gen_8200 (q_gen_8199) -> q_gen_8211 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8101, q_gen_8102, q_gen_8112, q_gen_8113, q_gen_8120, q_gen_8121, q_gen_8122, q_gen_8123, q_gen_8135, q_gen_8136, q_gen_8137, q_gen_8145, q_gen_8151, q_gen_8152, q_gen_8164, q_gen_8165, q_gen_8166, q_gen_8167, q_gen_8173, q_gen_8174, q_gen_8179, q_gen_8180, q_gen_8181, q_gen_8183, q_gen_8190, q_gen_8197, q_gen_8198, q_gen_8206, q_gen_8218, q_gen_8219, q_gen_8226}, Q_f={}, Delta= { () -> q_gen_8122 () -> q_gen_8123 (q_gen_8123, q_gen_8122) -> q_gen_8137 (q_gen_8167, q_gen_8122) -> q_gen_8166 (q_gen_8123) -> q_gen_8167 () -> q_gen_8082 (q_gen_8102, q_gen_8082) -> q_gen_8101 () -> q_gen_8102 (q_gen_8113, q_gen_8082) -> q_gen_8112 (q_gen_8102) -> q_gen_8113 (q_gen_8102, q_gen_8121) -> q_gen_8120 (q_gen_8123, q_gen_8122) -> q_gen_8121 (q_gen_8102, q_gen_8136) -> q_gen_8135 (q_gen_8123, q_gen_8137) -> q_gen_8136 (q_gen_8113, q_gen_8121) -> q_gen_8145 (q_gen_8102, q_gen_8152) -> q_gen_8151 (q_gen_8123, q_gen_8122) -> q_gen_8152 (q_gen_8102, q_gen_8165) -> q_gen_8164 (q_gen_8167, q_gen_8166) -> q_gen_8165 (q_gen_8102, q_gen_8101) -> q_gen_8173 (q_gen_8102, q_gen_8151) -> q_gen_8174 (q_gen_8167, q_gen_8122) -> q_gen_8179 (q_gen_8181, q_gen_8121) -> q_gen_8180 (q_gen_8123) -> q_gen_8181 (q_gen_8113, q_gen_8101) -> q_gen_8183 (q_gen_8102, q_gen_8120) -> q_gen_8190 (q_gen_8198, q_gen_8082) -> q_gen_8197 (q_gen_8167) -> q_gen_8198 (q_gen_8181, q_gen_8082) -> q_gen_8206 (q_gen_8219, q_gen_8082) -> q_gen_8218 (q_gen_8123) -> q_gen_8219 (q_gen_8219, q_gen_8179) -> q_gen_8226 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.007701 s (model generation: 0.007348, model checking: 0.000353): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} ; length -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} ; leq -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 0 () -> length([nil, z]) -> 0 () -> leq([z, s(nn2)]) -> 0 () -> leq([z, z]) -> 0 () -> reverse([nil, nil]) -> 3 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 1 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 1 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 1 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 1 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1 (leq([s(nn1), z])) -> BOT -> 1 } Sat witness: Found: (() -> reverse([nil, nil]), { }) ------------------------------------------- Step 1, which took 0.008238 s (model generation: 0.008131, model checking: 0.000107): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} ; length -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} ; leq -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082}, Q_f={q_gen_8082}, Delta= { () -> q_gen_8082 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 0 () -> length([nil, z]) -> 0 () -> leq([z, s(nn2)]) -> 0 () -> leq([z, z]) -> 3 () -> reverse([nil, nil]) -> 3 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 1 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 1 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 1 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 1 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1 (leq([s(nn1), z])) -> BOT -> 1 } Sat witness: Found: (() -> leq([z, z]), { }) ------------------------------------------- Step 2, which took 0.010694 s (model generation: 0.010628, model checking: 0.000066): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} ; length -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083}, Q_f={q_gen_8083}, Delta= { () -> q_gen_8083 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082}, Q_f={q_gen_8082}, Delta= { () -> q_gen_8082 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 0 () -> length([nil, z]) -> 0 () -> leq([z, s(nn2)]) -> 3 () -> leq([z, z]) -> 3 () -> reverse([nil, nil]) -> 3 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 1 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 1 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 1 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 1 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1 (leq([s(nn1), z])) -> BOT -> 1 } Sat witness: Found: (() -> leq([z, s(nn2)]), { nn2 -> z }) ------------------------------------------- Step 3, which took 0.012996 s (model generation: 0.012903, model checking: 0.000093): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} ; length -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085}, Q_f={q_gen_8083}, Delta= { () -> q_gen_8085 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082}, Q_f={q_gen_8082}, Delta= { () -> q_gen_8082 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 0 () -> length([nil, z]) -> 3 () -> leq([z, s(nn2)]) -> 3 () -> leq([z, z]) -> 3 () -> reverse([nil, nil]) -> 3 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 1 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 1 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 1 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 1 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1 (leq([s(nn1), z])) -> BOT -> 1 } Sat witness: Found: (() -> length([nil, z]), { }) ------------------------------------------- Step 4, which took 0.008799 s (model generation: 0.008638, model checking: 0.000161): Model: |_ { append -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8086 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085}, Q_f={q_gen_8083}, Delta= { () -> q_gen_8085 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082}, Q_f={q_gen_8082}, Delta= { () -> q_gen_8082 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 () -> length([nil, z]) -> 3 () -> leq([z, s(nn2)]) -> 3 () -> leq([z, z]) -> 3 () -> reverse([nil, nil]) -> 3 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 1 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 1 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 1 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 1 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1 (leq([s(nn1), z])) -> BOT -> 1 } Sat witness: Found: (() -> append([nil, l2, l2]), { l2 -> nil }) ------------------------------------------- Step 5, which took 0.008330 s (model generation: 0.007910, model checking: 0.000420): Model: |_ { append -> {{{ Q={q_gen_8087}, Q_f={q_gen_8087}, Delta= { () -> q_gen_8087 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8086 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085}, Q_f={q_gen_8083}, Delta= { () -> q_gen_8085 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082}, Q_f={q_gen_8082}, Delta= { () -> q_gen_8082 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 () -> length([nil, z]) -> 3 () -> leq([z, s(nn2)]) -> 3 () -> leq([z, z]) -> 3 () -> reverse([nil, nil]) -> 3 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 1 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 1 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 1 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 1 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2 (leq([s(nn1), z])) -> BOT -> 2 } Sat witness: Found: ((leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]), { nn1 -> z ; nn2 -> z }) ------------------------------------------- Step 6, which took 0.008233 s (model generation: 0.008093, model checking: 0.000140): Model: |_ { append -> {{{ Q={q_gen_8087}, Q_f={q_gen_8087}, Delta= { () -> q_gen_8087 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8086 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085}, Q_f={q_gen_8083}, Delta= { () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082}, Q_f={q_gen_8082}, Delta= { () -> q_gen_8082 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 () -> length([nil, z]) -> 3 () -> leq([z, s(nn2)]) -> 3 () -> leq([z, z]) -> 3 () -> reverse([nil, nil]) -> 3 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 1 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 1 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 1 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 4 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2 (leq([s(nn1), z])) -> BOT -> 2 } Sat witness: Found: ((length([ll, _xda])) -> length([cons(x, ll), s(_xda)]), { _xda -> z ; ll -> nil ; x -> z }) ------------------------------------------- Step 7, which took 0.013764 s (model generation: 0.013489, model checking: 0.000275): Model: |_ { append -> {{{ Q={q_gen_8087}, Q_f={q_gen_8087}, Delta= { () -> q_gen_8087 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8091, q_gen_8090) -> q_gen_8086 () -> q_gen_8086 () -> q_gen_8091 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085}, Q_f={q_gen_8083}, Delta= { () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082}, Q_f={q_gen_8082}, Delta= { () -> q_gen_8082 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 () -> length([nil, z]) -> 3 () -> leq([z, s(nn2)]) -> 3 () -> leq([z, z]) -> 3 () -> reverse([nil, nil]) -> 3 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 1 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 4 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 2 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 4 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2 (leq([s(nn1), z])) -> BOT -> 2 } Sat witness: Found: ((append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]), { _nda -> nil ; h1 -> z ; l2 -> nil ; t1 -> nil }) ------------------------------------------- Step 8, which took 0.017653 s (model generation: 0.017162, model checking: 0.000491): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094}, Q_f={q_gen_8087}, Delta= { () -> q_gen_8093 () -> q_gen_8094 (q_gen_8094, q_gen_8093) -> q_gen_8087 () -> q_gen_8087 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8091, q_gen_8090) -> q_gen_8086 () -> q_gen_8086 () -> q_gen_8091 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085}, Q_f={q_gen_8083}, Delta= { () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082}, Q_f={q_gen_8082}, Delta= { () -> q_gen_8082 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 3 () -> length([nil, z]) -> 3 () -> leq([z, s(nn2)]) -> 6 () -> leq([z, z]) -> 4 () -> reverse([nil, nil]) -> 4 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 2 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 4 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 3 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 4 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 3 (leq([s(nn1), z])) -> BOT -> 3 } Sat witness: Found: (() -> leq([z, s(nn2)]), { nn2 -> s(z) }) ------------------------------------------- Step 9, which took 0.009226 s (model generation: 0.008705, model checking: 0.000521): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094}, Q_f={q_gen_8087}, Delta= { () -> q_gen_8093 () -> q_gen_8094 (q_gen_8094, q_gen_8093) -> q_gen_8087 () -> q_gen_8087 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8091, q_gen_8090) -> q_gen_8086 () -> q_gen_8086 () -> q_gen_8091 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082}, Q_f={q_gen_8082}, Delta= { () -> q_gen_8082 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 6 () -> length([nil, z]) -> 4 () -> leq([z, s(nn2)]) -> 6 () -> leq([z, z]) -> 4 () -> reverse([nil, nil]) -> 4 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 3 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 4 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 4 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 4 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4 (leq([s(nn1), z])) -> BOT -> 4 } Sat witness: Found: (() -> append([nil, l2, l2]), { l2 -> cons(s(z), cons(s(z), nil)) }) ------------------------------------------- Step 10, which took 0.009653 s (model generation: 0.009488, model checking: 0.000165): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094}, Q_f={q_gen_8087}, Delta= { (q_gen_8094, q_gen_8093) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 () -> q_gen_8087 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8091, q_gen_8090) -> q_gen_8086 () -> q_gen_8086 () -> q_gen_8091 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082}, Q_f={q_gen_8082}, Delta= { () -> q_gen_8082 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 6 () -> length([nil, z]) -> 4 () -> leq([z, s(nn2)]) -> 6 () -> leq([z, z]) -> 4 () -> reverse([nil, nil]) -> 4 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 6 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 4 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 4 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 4 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4 (leq([s(nn1), z])) -> BOT -> 4 } Sat witness: Found: ((append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]), { _sda -> nil ; _tda -> cons(z, nil) ; h1 -> z ; t1 -> nil }) ------------------------------------------- Step 11, which took 0.010286 s (model generation: 0.009982, model checking: 0.000304): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094}, Q_f={q_gen_8087}, Delta= { (q_gen_8094, q_gen_8093) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 () -> q_gen_8087 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8091, q_gen_8090) -> q_gen_8086 () -> q_gen_8086 () -> q_gen_8091 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102}, Q_f={q_gen_8082}, Delta= { (q_gen_8102, q_gen_8082) -> q_gen_8082 () -> q_gen_8082 () -> q_gen_8102 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 6 () -> length([nil, z]) -> 4 () -> leq([z, s(nn2)]) -> 6 () -> leq([z, z]) -> 4 () -> reverse([nil, nil]) -> 4 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 6 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 4 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 4 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 7 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5 (leq([s(nn1), z])) -> BOT -> 5 } Sat witness: Found: ((length([ll, _xda])) -> length([cons(x, ll), s(_xda)]), { _xda -> z ; ll -> nil ; x -> s(z) }) ------------------------------------------- Step 12, which took 0.011320 s (model generation: 0.010093, model checking: 0.001227): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094}, Q_f={q_gen_8087}, Delta= { (q_gen_8094, q_gen_8093) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 () -> q_gen_8087 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 () -> q_gen_8105 (q_gen_8091, q_gen_8090) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102}, Q_f={q_gen_8082}, Delta= { (q_gen_8102, q_gen_8082) -> q_gen_8082 () -> q_gen_8082 () -> q_gen_8102 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 6 () -> length([nil, z]) -> 4 () -> leq([z, s(nn2)]) -> 6 () -> leq([z, z]) -> 4 () -> reverse([nil, nil]) -> 4 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 6 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 7 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 5 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 7 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5 (leq([s(nn1), z])) -> BOT -> 5 } Sat witness: Found: ((append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]), { _nda -> cons(z, nil) ; h1 -> z ; l2 -> cons(z, nil) ; t1 -> nil }) ------------------------------------------- Step 13, which took 0.011504 s (model generation: 0.010833, model checking: 0.000671): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110}, Q_f={q_gen_8087}, Delta= { () -> q_gen_8108 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8110, q_gen_8087) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8109, q_gen_8108) -> q_gen_8087 () -> q_gen_8087 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 () -> q_gen_8105 (q_gen_8091, q_gen_8090) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102}, Q_f={q_gen_8082}, Delta= { (q_gen_8102, q_gen_8082) -> q_gen_8082 () -> q_gen_8082 () -> q_gen_8102 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 6 () -> length([nil, z]) -> 5 () -> leq([z, s(nn2)]) -> 6 () -> leq([z, z]) -> 5 () -> reverse([nil, nil]) -> 5 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 9 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 7 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 6 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 7 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 6 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 6 (leq([s(nn1), z])) -> BOT -> 6 } Sat witness: Found: ((append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]), { _sda -> nil ; _tda -> cons(s(z), nil) ; h1 -> s(z) ; t1 -> nil }) ------------------------------------------- Step 14, which took 0.012588 s (model generation: 0.011601, model checking: 0.000987): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110}, Q_f={q_gen_8087}, Delta= { () -> q_gen_8108 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8110, q_gen_8087) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8109, q_gen_8108) -> q_gen_8087 () -> q_gen_8087 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 () -> q_gen_8105 (q_gen_8091, q_gen_8090) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102}, Q_f={q_gen_8082}, Delta= { (q_gen_8102, q_gen_8082) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 7 () -> length([nil, z]) -> 6 () -> leq([z, s(nn2)]) -> 7 () -> leq([z, z]) -> 6 () -> reverse([nil, nil]) -> 6 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 9 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 7 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 7 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 10 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 7 (leq([s(nn1), z])) -> BOT -> 7 } Sat witness: Found: ((length([ll, _xda])) -> length([cons(x, ll), s(_xda)]), { _xda -> z ; ll -> nil ; x -> s(s(z)) }) ------------------------------------------- Step 15, which took 0.013353 s (model generation: 0.012398, model checking: 0.000955): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110}, Q_f={q_gen_8087}, Delta= { () -> q_gen_8108 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8110, q_gen_8087) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8109, q_gen_8108) -> q_gen_8087 () -> q_gen_8087 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8091, q_gen_8090) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102}, Q_f={q_gen_8082}, Delta= { (q_gen_8102, q_gen_8082) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 7 () -> length([nil, z]) -> 7 () -> leq([z, s(nn2)]) -> 7 () -> leq([z, z]) -> 7 () -> reverse([nil, nil]) -> 7 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 9 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 10 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 8 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 10 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 8 (leq([s(nn1), z])) -> BOT -> 8 } Sat witness: Found: ((append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]), { _nda -> cons(z, nil) ; h1 -> z ; l2 -> nil ; t1 -> nil }) ------------------------------------------- Step 16, which took 0.014568 s (model generation: 0.013504, model checking: 0.001064): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110}, Q_f={q_gen_8087}, Delta= { () -> q_gen_8108 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8110, q_gen_8087) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8109, q_gen_8108) -> q_gen_8087 () -> q_gen_8087 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8091, q_gen_8090) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102}, Q_f={q_gen_8082}, Delta= { (q_gen_8102, q_gen_8082) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 8 () -> length([nil, z]) -> 8 () -> leq([z, s(nn2)]) -> 8 () -> leq([z, z]) -> 8 () -> reverse([nil, nil]) -> 8 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 12 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 10 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 9 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 10 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 9 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 9 (leq([s(nn1), z])) -> BOT -> 9 } Sat witness: Found: ((append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]), { _sda -> nil ; _tda -> cons(z, cons(z, nil)) ; h1 -> z ; t1 -> nil }) ------------------------------------------- Step 17, which took 0.015199 s (model generation: 0.014086, model checking: 0.001113): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110}, Q_f={q_gen_8087}, Delta= { () -> q_gen_8108 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8110, q_gen_8087) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8109, q_gen_8108) -> q_gen_8087 () -> q_gen_8087 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8091, q_gen_8090) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123}, Q_f={q_gen_8082}, Delta= { () -> q_gen_8122 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 9 () -> length([nil, z]) -> 9 () -> leq([z, s(nn2)]) -> 9 () -> leq([z, z]) -> 9 () -> reverse([nil, nil]) -> 9 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 12 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 10 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 10 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 13 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10 (leq([s(nn1), z])) -> BOT -> 10 } Sat witness: Found: ((length([ll, _xda])) -> length([cons(x, ll), s(_xda)]), { _xda -> s(z) ; ll -> cons(z, nil) ; x -> z }) ------------------------------------------- Step 18, which took 0.016276 s (model generation: 0.015373, model checking: 0.000903): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110}, Q_f={q_gen_8087}, Delta= { () -> q_gen_8108 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8110, q_gen_8087) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8109, q_gen_8108) -> q_gen_8087 () -> q_gen_8087 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105}, Q_f={q_gen_8086}, Delta= { (q_gen_8105, q_gen_8090) -> q_gen_8090 () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8091, q_gen_8090) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123}, Q_f={q_gen_8082}, Delta= { () -> q_gen_8122 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 10 () -> length([nil, z]) -> 10 () -> leq([z, s(nn2)]) -> 10 () -> leq([z, z]) -> 10 () -> reverse([nil, nil]) -> 10 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 12 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 10 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 13 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 13 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11 (leq([s(nn1), z])) -> BOT -> 11 } Sat witness: Found: ((length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]), { _bea -> s(s(z)) ; _cea -> cons(z, nil) ; _dea -> s(z) ; l1 -> cons(z, nil) }) ------------------------------------------- Step 19, which took 0.023763 s (model generation: 0.022641, model checking: 0.001122): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110}, Q_f={q_gen_8087}, Delta= { () -> q_gen_8108 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8110, q_gen_8087) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8109, q_gen_8108) -> q_gen_8087 () -> q_gen_8087 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105}, Q_f={q_gen_8086}, Delta= { (q_gen_8105, q_gen_8090) -> q_gen_8090 () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8091, q_gen_8090) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123}, Q_f={q_gen_8082}, Delta= { () -> q_gen_8122 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 10 () -> length([nil, z]) -> 10 () -> leq([z, s(nn2)]) -> 10 () -> leq([z, z]) -> 10 () -> reverse([nil, nil]) -> 10 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 12 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 13 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 13 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 13 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11 (leq([s(nn1), z])) -> BOT -> 11 } Sat witness: Found: ((append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]), { _nda -> cons(z, cons(z, nil)) ; h1 -> z ; l2 -> cons(z, nil) ; t1 -> nil }) ------------------------------------------- Step 20, which took 0.017698 s (model generation: 0.017103, model checking: 0.000595): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8110, q_gen_8087) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8109, q_gen_8108) -> q_gen_8087 () -> q_gen_8087 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105}, Q_f={q_gen_8086}, Delta= { (q_gen_8105, q_gen_8090) -> q_gen_8090 () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8091, q_gen_8090) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123}, Q_f={q_gen_8082}, Delta= { () -> q_gen_8122 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 11 () -> length([nil, z]) -> 11 () -> leq([z, s(nn2)]) -> 11 () -> leq([z, z]) -> 11 () -> reverse([nil, nil]) -> 11 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 12 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 13 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 13 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 13 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11 (leq([s(nn1), z])) -> BOT -> 14 } Sat witness: Found: ((leq([s(nn1), z])) -> BOT, { nn1 -> z }) ------------------------------------------- Step 21, which took 0.019678 s (model generation: 0.019557, model checking: 0.000121): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8110, q_gen_8087) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8109, q_gen_8108) -> q_gen_8087 () -> q_gen_8087 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105}, Q_f={q_gen_8086}, Delta= { (q_gen_8105, q_gen_8090) -> q_gen_8090 () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8091, q_gen_8090) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8129}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8129) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8085) -> q_gen_8129 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123}, Q_f={q_gen_8082}, Delta= { () -> q_gen_8122 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 11 () -> length([nil, z]) -> 11 () -> leq([z, s(nn2)]) -> 11 () -> leq([z, z]) -> 11 () -> reverse([nil, nil]) -> 11 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 12 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 13 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 13 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 13 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14 (leq([s(nn1), z])) -> BOT -> 14 } Sat witness: Found: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), { nn1 -> s(z) ; nn2 -> z }) ------------------------------------------- Step 22, which took 0.019830 s (model generation: 0.019164, model checking: 0.000666): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8098, q_gen_8100, q_gen_8108, q_gen_8109, q_gen_8110}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 () -> q_gen_8109 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8094, q_gen_8093) -> q_gen_8098 (q_gen_8110, q_gen_8100) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8098) -> q_gen_8087 () -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8100 (q_gen_8109, q_gen_8108) -> q_gen_8100 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105}, Q_f={q_gen_8086}, Delta= { (q_gen_8105, q_gen_8090) -> q_gen_8090 () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8091, q_gen_8090) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8101, q_gen_8102, q_gen_8122, q_gen_8123}, Q_f={q_gen_8082}, Delta= { () -> q_gen_8122 () -> q_gen_8123 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102, q_gen_8082) -> q_gen_8101 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 14 () -> length([nil, z]) -> 12 () -> leq([z, s(nn2)]) -> 12 () -> leq([z, z]) -> 12 () -> reverse([nil, nil]) -> 12 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 12 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 13 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 13 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 13 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 12 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14 (leq([s(nn1), z])) -> BOT -> 14 } Sat witness: Found: (() -> append([nil, l2, l2]), { l2 -> cons(z, nil) }) ------------------------------------------- Step 23, which took 0.027356 s (model generation: 0.026480, model checking: 0.000876): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8110, q_gen_8087) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8109, q_gen_8108) -> q_gen_8087 () -> q_gen_8087 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 (q_gen_8105) -> q_gen_8126 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123}, Q_f={q_gen_8082}, Delta= { () -> q_gen_8122 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 14 () -> length([nil, z]) -> 12 () -> leq([z, s(nn2)]) -> 12 () -> leq([z, z]) -> 12 () -> reverse([nil, nil]) -> 12 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 15 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 13 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 13 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 13 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 13 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14 (leq([s(nn1), z])) -> BOT -> 14 } Sat witness: Found: ((append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]), { _sda -> nil ; _tda -> cons(z, cons(z, cons(z, nil))) ; h1 -> z ; t1 -> nil }) ------------------------------------------- Step 24, which took 0.026323 s (model generation: 0.025130, model checking: 0.001193): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8110, q_gen_8087) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8109, q_gen_8108) -> q_gen_8087 () -> q_gen_8087 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 (q_gen_8105) -> q_gen_8126 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 14 () -> length([nil, z]) -> 13 () -> leq([z, s(nn2)]) -> 13 () -> leq([z, z]) -> 13 () -> reverse([nil, nil]) -> 13 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 15 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 13 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 13 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 16 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 14 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14 (leq([s(nn1), z])) -> BOT -> 14 } Sat witness: Found: ((length([ll, _xda])) -> length([cons(x, ll), s(_xda)]), { _xda -> s(s(z)) ; ll -> cons(z, cons(z, nil)) ; x -> s(z) }) ------------------------------------------- Step 25, which took 0.022019 s (model generation: 0.021417, model checking: 0.000602): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8110, q_gen_8087) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8109, q_gen_8108) -> q_gen_8087 () -> q_gen_8087 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8105, q_gen_8125) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8091, q_gen_8125) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8126) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 (q_gen_8105) -> q_gen_8126 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 14 () -> length([nil, z]) -> 13 () -> leq([z, s(nn2)]) -> 13 () -> leq([z, z]) -> 13 () -> reverse([nil, nil]) -> 13 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 15 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 13 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 16 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 16 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 14 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14 (leq([s(nn1), z])) -> BOT -> 14 } Sat witness: Found: ((length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]), { _bea -> s(s(s(s(z)))) ; _cea -> cons(s(z), cons(z, nil)) ; _dea -> s(s(s(z))) ; l1 -> cons(s(z), nil) }) ------------------------------------------- Step 26, which took 0.028176 s (model generation: 0.025894, model checking: 0.002282): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8110, q_gen_8087) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8109, q_gen_8108) -> q_gen_8087 () -> q_gen_8087 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8105, q_gen_8125) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 (q_gen_8126) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 14 () -> length([nil, z]) -> 13 () -> leq([z, s(nn2)]) -> 13 () -> leq([z, z]) -> 13 () -> reverse([nil, nil]) -> 13 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 15 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 16 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 16 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 16 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 14 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14 (leq([s(nn1), z])) -> BOT -> 14 } Sat witness: Found: ((append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]), { _nda -> cons(z, nil) ; h1 -> s(z) ; l2 -> cons(z, nil) ; t1 -> nil }) ------------------------------------------- Step 27, which took 0.033019 s (model generation: 0.030865, model checking: 0.002154): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8110, q_gen_8087) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8109, q_gen_8108) -> q_gen_8087 () -> q_gen_8087 (q_gen_8094) -> q_gen_8110 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { (q_gen_8105, q_gen_8125) -> q_gen_8090 () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8126) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 (q_gen_8105) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 15 () -> length([nil, z]) -> 14 () -> leq([z, s(nn2)]) -> 14 () -> leq([z, z]) -> 14 () -> reverse([nil, nil]) -> 14 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 18 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 16 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 16 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 16 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 15 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 15 (leq([s(nn1), z])) -> BOT -> 15 } Sat witness: Found: ((append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]), { _sda -> cons(z, nil) ; _tda -> cons(z, nil) ; h1 -> z ; t1 -> cons(z, nil) }) ------------------------------------------- Step 28, which took 0.035301 s (model generation: 0.033523, model checking: 0.001778): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8110, q_gen_8087) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8109, q_gen_8108) -> q_gen_8087 () -> q_gen_8087 (q_gen_8094) -> q_gen_8110 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { (q_gen_8105, q_gen_8125) -> q_gen_8090 () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8126) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 (q_gen_8105) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 16 () -> length([nil, z]) -> 15 () -> leq([z, s(nn2)]) -> 15 () -> leq([z, z]) -> 15 () -> reverse([nil, nil]) -> 15 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 18 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 16 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 16 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 19 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 16 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 16 (leq([s(nn1), z])) -> BOT -> 16 } Sat witness: Found: ((length([ll, _xda])) -> length([cons(x, ll), s(_xda)]), { _xda -> s(s(s(z))) ; ll -> cons(s(z), nil) ; x -> s(z) }) ------------------------------------------- Step 29, which took 0.042661 s (model generation: 0.041860, model checking: 0.000801): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8110, q_gen_8087) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8109, q_gen_8108) -> q_gen_8087 () -> q_gen_8087 (q_gen_8094) -> q_gen_8110 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8105, q_gen_8125) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 (q_gen_8126) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 16 () -> length([nil, z]) -> 16 () -> leq([z, s(nn2)]) -> 16 () -> leq([z, z]) -> 16 () -> reverse([nil, nil]) -> 16 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 18 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 16 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 19 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 19 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 17 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 17 (leq([s(nn1), z])) -> BOT -> 17 } Sat witness: Found: ((length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]), { _bea -> s(z) ; _cea -> nil ; _dea -> z ; l1 -> cons(z, nil) }) ------------------------------------------- Step 30, which took 0.040252 s (model generation: 0.036800, model checking: 0.003452): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8110, q_gen_8087) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8109, q_gen_8108) -> q_gen_8087 () -> q_gen_8087 (q_gen_8094) -> q_gen_8110 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8105, q_gen_8125) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 (q_gen_8126) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8121, q_gen_8122, q_gen_8123}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8102, q_gen_8121) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 (q_gen_8123, q_gen_8122) -> q_gen_8121 (q_gen_8123, q_gen_8122) -> q_gen_8121 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 16 () -> length([nil, z]) -> 16 () -> leq([z, s(nn2)]) -> 16 () -> leq([z, z]) -> 16 () -> reverse([nil, nil]) -> 16 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 18 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 19 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 19 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 19 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 17 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 17 (leq([s(nn1), z])) -> BOT -> 17 } Sat witness: Found: ((append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]), { _nda -> cons(s(z), cons(z, nil)) ; h1 -> s(z) ; l2 -> cons(s(z), nil) ; t1 -> nil }) ------------------------------------------- Step 31, which took 0.037463 s (model generation: 0.036237, model checking: 0.001226): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8110, q_gen_8087) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8109, q_gen_8108) -> q_gen_8087 () -> q_gen_8087 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8105, q_gen_8125) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 (q_gen_8126) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8121, q_gen_8122, q_gen_8123}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8102, q_gen_8121) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 (q_gen_8123, q_gen_8122) -> q_gen_8121 (q_gen_8123, q_gen_8122) -> q_gen_8121 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 17 () -> length([nil, z]) -> 17 () -> leq([z, s(nn2)]) -> 17 () -> leq([z, z]) -> 17 () -> reverse([nil, nil]) -> 17 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 21 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 19 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 19 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 19 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 18 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 18 (leq([s(nn1), z])) -> BOT -> 18 } Sat witness: Found: ((append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]), { _sda -> nil ; _tda -> cons(z, cons(s(z), cons(s(z), nil))) ; h1 -> z ; t1 -> nil }) ------------------------------------------- Step 32, which took 0.054173 s (model generation: 0.052413, model checking: 0.001760): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8110, q_gen_8087) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8109, q_gen_8108) -> q_gen_8087 () -> q_gen_8087 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8105, q_gen_8125) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 (q_gen_8126) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8121, q_gen_8122, q_gen_8123}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8102, q_gen_8121) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 (q_gen_8123, q_gen_8122) -> q_gen_8121 (q_gen_8123, q_gen_8122) -> q_gen_8121 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 18 () -> length([nil, z]) -> 18 () -> leq([z, s(nn2)]) -> 18 () -> leq([z, z]) -> 18 () -> reverse([nil, nil]) -> 18 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 21 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 19 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 19 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 22 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 19 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 19 (leq([s(nn1), z])) -> BOT -> 19 } Sat witness: Found: ((length([ll, _xda])) -> length([cons(x, ll), s(_xda)]), { _xda -> s(s(z)) ; ll -> cons(z, cons(z, nil)) ; x -> s(s(z)) }) ------------------------------------------- Step 33, which took 0.067358 s (model generation: 0.065640, model checking: 0.001718): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8110, q_gen_8087) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8109, q_gen_8108) -> q_gen_8087 () -> q_gen_8087 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8105, q_gen_8125) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8091, q_gen_8125) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8091) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 (q_gen_8126) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8121, q_gen_8122, q_gen_8123}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8102, q_gen_8121) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 (q_gen_8123, q_gen_8122) -> q_gen_8121 (q_gen_8123, q_gen_8122) -> q_gen_8121 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 19 () -> length([nil, z]) -> 19 () -> leq([z, s(nn2)]) -> 19 () -> leq([z, z]) -> 19 () -> reverse([nil, nil]) -> 19 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 21 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 19 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 22 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 22 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 20 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 20 (leq([s(nn1), z])) -> BOT -> 20 } Sat witness: Found: ((length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]), { _bea -> s(s(z)) ; _cea -> cons(z, nil) ; _dea -> s(z) ; l1 -> cons(z, cons(z, nil)) }) ------------------------------------------- Step 34, which took 0.059932 s (model generation: 0.059192, model checking: 0.000740): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8107, q_gen_8108, q_gen_8109, q_gen_8110}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8110, q_gen_8107) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 () -> q_gen_8087 (q_gen_8110, q_gen_8087) -> q_gen_8107 (q_gen_8109, q_gen_8108) -> q_gen_8107 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8105, q_gen_8125) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8091, q_gen_8125) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8091) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 (q_gen_8126) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123, q_gen_8151}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8151) -> q_gen_8151 (q_gen_8123, q_gen_8122) -> q_gen_8151 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 19 () -> length([nil, z]) -> 19 () -> leq([z, s(nn2)]) -> 19 () -> leq([z, z]) -> 19 () -> reverse([nil, nil]) -> 19 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 21 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 22 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 22 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 22 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 20 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 20 (leq([s(nn1), z])) -> BOT -> 20 } Sat witness: Found: ((append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]), { _nda -> cons(z, cons(z, nil)) ; h1 -> s(z) ; l2 -> cons(z, nil) ; t1 -> cons(z, nil) }) ------------------------------------------- Step 35, which took 0.102316 s (model generation: 0.099911, model checking: 0.002405): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8092, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8150}, Q_f={q_gen_8087, q_gen_8092}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 () -> q_gen_8087 (q_gen_8110, q_gen_8092) -> q_gen_8092 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8109, q_gen_8108) -> q_gen_8092 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 () -> q_gen_8110 (q_gen_8110, q_gen_8087) -> q_gen_8150 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8105, q_gen_8125) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8091, q_gen_8125) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8091) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 (q_gen_8126) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123, q_gen_8151}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8151) -> q_gen_8151 (q_gen_8123, q_gen_8122) -> q_gen_8151 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 20 () -> length([nil, z]) -> 20 () -> leq([z, s(nn2)]) -> 20 () -> leq([z, z]) -> 20 () -> reverse([nil, nil]) -> 20 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 24 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 22 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 22 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 22 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 21 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 21 (leq([s(nn1), z])) -> BOT -> 21 } Sat witness: Found: ((append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]), { _sda -> cons(z, cons(z, nil)) ; _tda -> cons(z, cons(z, nil)) ; h1 -> z ; t1 -> cons(z, cons(z, nil)) }) ------------------------------------------- Step 36, which took 0.140509 s (model generation: 0.138940, model checking: 0.001569): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8107, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8118}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8109, q_gen_8108) -> q_gen_8118 (q_gen_8110, q_gen_8107) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 () -> q_gen_8087 (q_gen_8110, q_gen_8087) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8109, q_gen_8108) -> q_gen_8107 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8105, q_gen_8125) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8091, q_gen_8125) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8091) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 (q_gen_8126) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8120, q_gen_8122, q_gen_8123}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8120) -> q_gen_8120 (q_gen_8123, q_gen_8122) -> q_gen_8120 (q_gen_8123, q_gen_8122) -> q_gen_8120 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 21 () -> length([nil, z]) -> 21 () -> leq([z, s(nn2)]) -> 21 () -> leq([z, z]) -> 21 () -> reverse([nil, nil]) -> 21 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 24 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 22 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 25 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 23 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 22 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 22 (leq([s(nn1), z])) -> BOT -> 22 } Sat witness: Found: ((length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]), { _bea -> s(s(z)) ; _cea -> cons(z, cons(z, nil)) ; _dea -> s(z) ; l1 -> cons(z, cons(z, nil)) }) ------------------------------------------- Step 37, which took 0.109146 s (model generation: 0.107603, model checking: 0.001543): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8107, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8149}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8110, q_gen_8107) -> q_gen_8087 (q_gen_8149, q_gen_8087) -> q_gen_8087 (q_gen_8149, q_gen_8107) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 () -> q_gen_8087 (q_gen_8110, q_gen_8087) -> q_gen_8107 (q_gen_8109, q_gen_8108) -> q_gen_8107 () -> q_gen_8110 (q_gen_8110) -> q_gen_8149 (q_gen_8094) -> q_gen_8149 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8105, q_gen_8125) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 (q_gen_8091) -> q_gen_8126 (q_gen_8126) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123, q_gen_8151}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8151) -> q_gen_8151 (q_gen_8123, q_gen_8122) -> q_gen_8151 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 22 () -> length([nil, z]) -> 22 () -> leq([z, s(nn2)]) -> 22 () -> leq([z, z]) -> 22 () -> reverse([nil, nil]) -> 22 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 24 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 25 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 25 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 23 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 23 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 23 (leq([s(nn1), z])) -> BOT -> 23 } Sat witness: Found: ((append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]), { _nda -> cons(s(z), nil) ; h1 -> z ; l2 -> cons(z, nil) ; t1 -> cons(s(z), nil) }) ------------------------------------------- Step 38, which took 0.159772 s (model generation: 0.157740, model checking: 0.002032): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8107, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8118}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8109, q_gen_8108) -> q_gen_8118 (q_gen_8110, q_gen_8107) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 () -> q_gen_8087 (q_gen_8110, q_gen_8087) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8109, q_gen_8108) -> q_gen_8107 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8105, q_gen_8125) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 (q_gen_8091) -> q_gen_8126 (q_gen_8126) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123, q_gen_8151}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8151) -> q_gen_8151 (q_gen_8123, q_gen_8122) -> q_gen_8151 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 23 () -> length([nil, z]) -> 23 () -> leq([z, s(nn2)]) -> 23 () -> leq([z, z]) -> 23 () -> reverse([nil, nil]) -> 23 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 27 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 25 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 25 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 24 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 24 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 24 (leq([s(nn1), z])) -> BOT -> 24 } Sat witness: Found: ((append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]), { _sda -> cons(s(z), nil) ; _tda -> cons(s(z), cons(z, nil)) ; h1 -> z ; t1 -> nil }) ------------------------------------------- Step 39, which took 0.473450 s (model generation: 0.472021, model checking: 0.001429): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8107, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8118}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8109, q_gen_8108) -> q_gen_8118 (q_gen_8110, q_gen_8107) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 () -> q_gen_8087 (q_gen_8110, q_gen_8087) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8109, q_gen_8108) -> q_gen_8107 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8105, q_gen_8125) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 (q_gen_8091) -> q_gen_8126 (q_gen_8126) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8120, q_gen_8122, q_gen_8123}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8120) -> q_gen_8120 (q_gen_8123, q_gen_8122) -> q_gen_8120 (q_gen_8123, q_gen_8122) -> q_gen_8120 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 24 () -> length([nil, z]) -> 24 () -> leq([z, s(nn2)]) -> 24 () -> leq([z, z]) -> 24 () -> reverse([nil, nil]) -> 24 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 27 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 25 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 28 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 25 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 25 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 25 (leq([s(nn1), z])) -> BOT -> 25 } Sat witness: Found: ((length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]), { _bea -> s(s(s(z))) ; _cea -> cons(s(z), cons(z, nil)) ; _dea -> s(s(z)) ; l1 -> cons(s(z), cons(z, nil)) }) ------------------------------------------- Step 40, which took 0.107869 s (model generation: 0.104257, model checking: 0.003612): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8107, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8118}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8109, q_gen_8108) -> q_gen_8118 (q_gen_8110, q_gen_8107) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 () -> q_gen_8087 (q_gen_8110, q_gen_8087) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8109, q_gen_8108) -> q_gen_8107 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8116, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { (q_gen_8105, q_gen_8125) -> q_gen_8090 () -> q_gen_8090 () -> q_gen_8105 (q_gen_8105) -> q_gen_8116 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8116, q_gen_8090) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8126) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 (q_gen_8116) -> q_gen_8091 (q_gen_8116) -> q_gen_8091 () -> q_gen_8091 (q_gen_8091) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8120, q_gen_8122, q_gen_8123}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8120) -> q_gen_8120 (q_gen_8123, q_gen_8122) -> q_gen_8120 (q_gen_8123, q_gen_8122) -> q_gen_8120 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 25 () -> length([nil, z]) -> 25 () -> leq([z, s(nn2)]) -> 25 () -> leq([z, z]) -> 25 () -> reverse([nil, nil]) -> 25 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 27 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 25 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 28 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 28 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 26 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 26 (leq([s(nn1), z])) -> BOT -> 26 } Sat witness: Found: ((length([ll, _xda])) -> length([cons(x, ll), s(_xda)]), { _xda -> z ; ll -> nil ; x -> s(s(s(z))) }) ------------------------------------------- Step 41, which took 0.401858 s (model generation: 0.400377, model checking: 0.001481): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8092, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8150}, Q_f={q_gen_8087, q_gen_8092}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8110, q_gen_8092) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 () -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8109, q_gen_8108) -> q_gen_8092 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 () -> q_gen_8110 (q_gen_8110, q_gen_8087) -> q_gen_8150 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8105, q_gen_8125) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 (q_gen_8091) -> q_gen_8126 (q_gen_8126) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8101, q_gen_8102, q_gen_8122, q_gen_8123, q_gen_8151}, Q_f={q_gen_8082, q_gen_8101}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102, q_gen_8082) -> q_gen_8101 (q_gen_8102) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8101) -> q_gen_8151 (q_gen_8102, q_gen_8151) -> q_gen_8151 (q_gen_8123, q_gen_8122) -> q_gen_8151 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 25 () -> length([nil, z]) -> 25 () -> leq([z, s(nn2)]) -> 25 () -> leq([z, z]) -> 25 () -> reverse([nil, nil]) -> 25 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 27 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 28 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 28 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 28 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 26 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 26 (leq([s(nn1), z])) -> BOT -> 26 } Sat witness: Found: ((append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]), { _nda -> cons(z, cons(z, nil)) ; h1 -> s(z) ; l2 -> cons(z, cons(z, nil)) ; t1 -> nil }) ------------------------------------------- Step 42, which took 0.481121 s (model generation: 0.477744, model checking: 0.003377): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8107, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8118}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8109, q_gen_8108) -> q_gen_8118 (q_gen_8110, q_gen_8107) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 () -> q_gen_8087 (q_gen_8110, q_gen_8087) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8109, q_gen_8108) -> q_gen_8107 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8104, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { (q_gen_8105, q_gen_8125) -> q_gen_8090 () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8104, q_gen_8090) -> q_gen_8086 (q_gen_8104, q_gen_8125) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8091) -> q_gen_8091 () -> q_gen_8091 (q_gen_8126) -> q_gen_8104 (q_gen_8105) -> q_gen_8104 (q_gen_8105) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8120, q_gen_8122, q_gen_8123}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8120) -> q_gen_8120 (q_gen_8123, q_gen_8122) -> q_gen_8120 (q_gen_8123, q_gen_8122) -> q_gen_8120 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 26 () -> length([nil, z]) -> 26 () -> leq([z, s(nn2)]) -> 26 () -> leq([z, z]) -> 26 () -> reverse([nil, nil]) -> 26 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 30 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 28 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 28 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 28 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 27 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 27 (leq([s(nn1), z])) -> BOT -> 27 } Sat witness: Found: ((append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]), { _sda -> cons(z, nil) ; _tda -> cons(z, cons(z, cons(z, nil))) ; h1 -> z ; t1 -> cons(z, nil) }) ------------------------------------------- Step 43, which took 0.687124 s (model generation: 0.685777, model checking: 0.001347): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8107, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8118}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8109, q_gen_8108) -> q_gen_8118 (q_gen_8110, q_gen_8107) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 () -> q_gen_8087 (q_gen_8110, q_gen_8087) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8109, q_gen_8108) -> q_gen_8107 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8104, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8105, q_gen_8125) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8104, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 () -> q_gen_8091 (q_gen_8091) -> q_gen_8104 (q_gen_8105) -> q_gen_8104 (q_gen_8104) -> q_gen_8126 (q_gen_8126) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8104, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123, q_gen_8151}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8151) -> q_gen_8151 (q_gen_8123, q_gen_8122) -> q_gen_8151 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 27 () -> length([nil, z]) -> 27 () -> leq([z, s(nn2)]) -> 27 () -> leq([z, z]) -> 27 () -> reverse([nil, nil]) -> 27 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 30 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 28 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 28 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 31 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 28 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 28 (leq([s(nn1), z])) -> BOT -> 28 } Sat witness: Found: ((length([ll, _xda])) -> length([cons(x, ll), s(_xda)]), { _xda -> s(z) ; ll -> cons(z, nil) ; x -> s(z) }) ------------------------------------------- Step 44, which took 1.085095 s (model generation: 1.084007, model checking: 0.001088): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8107, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8118}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8109, q_gen_8108) -> q_gen_8118 (q_gen_8110, q_gen_8107) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 () -> q_gen_8087 (q_gen_8110, q_gen_8087) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8109, q_gen_8108) -> q_gen_8107 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8105, q_gen_8125) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 (q_gen_8091) -> q_gen_8126 (q_gen_8126) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128, q_gen_8129}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8128) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8129) -> q_gen_8128 (q_gen_8085) -> q_gen_8129 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123, q_gen_8151}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8151) -> q_gen_8151 (q_gen_8123, q_gen_8122) -> q_gen_8151 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 28 () -> length([nil, z]) -> 28 () -> leq([z, s(nn2)]) -> 28 () -> leq([z, z]) -> 28 () -> reverse([nil, nil]) -> 28 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 30 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 28 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 28 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 31 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 28 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 31 (leq([s(nn1), z])) -> BOT -> 29 } Sat witness: Found: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), { nn1 -> s(s(z)) ; nn2 -> s(z) }) ------------------------------------------- Step 45, which took 0.178557 s (model generation: 0.177767, model checking: 0.000790): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8107, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8118}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8109, q_gen_8108) -> q_gen_8118 (q_gen_8110, q_gen_8107) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 () -> q_gen_8087 (q_gen_8110, q_gen_8087) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8109, q_gen_8108) -> q_gen_8107 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8116, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { (q_gen_8105, q_gen_8125) -> q_gen_8090 () -> q_gen_8090 () -> q_gen_8105 (q_gen_8105) -> q_gen_8116 (q_gen_8116) -> q_gen_8116 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8116, q_gen_8090) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8126) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 (q_gen_8116) -> q_gen_8091 (q_gen_8116) -> q_gen_8091 () -> q_gen_8091 (q_gen_8091) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123, q_gen_8151}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8151) -> q_gen_8151 (q_gen_8123, q_gen_8122) -> q_gen_8151 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 28 () -> length([nil, z]) -> 28 () -> leq([z, s(nn2)]) -> 28 () -> leq([z, z]) -> 28 () -> reverse([nil, nil]) -> 28 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 30 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 28 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 31 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 31 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 29 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 31 (leq([s(nn1), z])) -> BOT -> 29 } Sat witness: Found: ((length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]), { _bea -> s(s(s(z))) ; _cea -> cons(z, cons(z, nil)) ; _dea -> s(s(z)) ; l1 -> cons(z, nil) }) ------------------------------------------- Step 46, which took 0.150254 s (model generation: 0.148917, model checking: 0.001337): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8107, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8118}, Q_f={q_gen_8087}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8109, q_gen_8108) -> q_gen_8118 (q_gen_8110, q_gen_8107) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 () -> q_gen_8087 (q_gen_8110, q_gen_8087) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8109, q_gen_8108) -> q_gen_8107 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8116, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { (q_gen_8105, q_gen_8125) -> q_gen_8090 (q_gen_8116, q_gen_8090) -> q_gen_8090 () -> q_gen_8090 (q_gen_8116) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105) -> q_gen_8116 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8126) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 (q_gen_8116) -> q_gen_8091 () -> q_gen_8091 (q_gen_8091) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8116) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123, q_gen_8151}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8151) -> q_gen_8151 (q_gen_8123, q_gen_8122) -> q_gen_8151 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 28 () -> length([nil, z]) -> 28 () -> leq([z, s(nn2)]) -> 28 () -> leq([z, z]) -> 28 () -> reverse([nil, nil]) -> 28 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 30 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 31 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 31 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 31 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 29 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 31 (leq([s(nn1), z])) -> BOT -> 29 } Sat witness: Found: ((append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]), { _nda -> cons(z, cons(z, cons(z, nil))) ; h1 -> z ; l2 -> cons(z, cons(z, nil)) ; t1 -> cons(z, nil) }) ------------------------------------------- Step 47, which took 0.155941 s (model generation: 0.154713, model checking: 0.001228): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8092, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8150}, Q_f={q_gen_8087, q_gen_8092}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 () -> q_gen_8087 (q_gen_8110, q_gen_8092) -> q_gen_8092 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8109, q_gen_8108) -> q_gen_8092 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 () -> q_gen_8110 (q_gen_8110, q_gen_8087) -> q_gen_8150 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8105, q_gen_8125) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 (q_gen_8091) -> q_gen_8126 (q_gen_8126) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8101, q_gen_8102, q_gen_8121, q_gen_8122, q_gen_8123, q_gen_8152}, Q_f={q_gen_8082, q_gen_8101}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8121) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102, q_gen_8082) -> q_gen_8101 (q_gen_8102) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8101) -> q_gen_8121 (q_gen_8102, q_gen_8152) -> q_gen_8121 (q_gen_8123, q_gen_8122) -> q_gen_8121 (q_gen_8123, q_gen_8122) -> q_gen_8152 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 29 () -> length([nil, z]) -> 29 () -> leq([z, s(nn2)]) -> 29 () -> leq([z, z]) -> 29 () -> reverse([nil, nil]) -> 29 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 33 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 31 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 31 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 31 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 30 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 31 (leq([s(nn1), z])) -> BOT -> 30 } Sat witness: Found: ((append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]), { _sda -> cons(z, nil) ; _tda -> cons(z, cons(z, nil)) ; h1 -> z ; t1 -> cons(z, nil) }) ------------------------------------------- Step 48, which took 0.187359 s (model generation: 0.185014, model checking: 0.002345): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8092, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8150}, Q_f={q_gen_8087, q_gen_8092}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 () -> q_gen_8087 (q_gen_8110, q_gen_8092) -> q_gen_8092 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8109, q_gen_8108) -> q_gen_8092 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 () -> q_gen_8110 (q_gen_8110, q_gen_8087) -> q_gen_8150 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8116, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { (q_gen_8105, q_gen_8125) -> q_gen_8090 (q_gen_8116, q_gen_8090) -> q_gen_8090 () -> q_gen_8090 () -> q_gen_8105 (q_gen_8105) -> q_gen_8116 (q_gen_8116) -> q_gen_8116 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8126) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 (q_gen_8116) -> q_gen_8091 () -> q_gen_8091 (q_gen_8091) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8116) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8121, q_gen_8122, q_gen_8123, q_gen_8152}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8102, q_gen_8121) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8152) -> q_gen_8121 (q_gen_8123, q_gen_8122) -> q_gen_8121 (q_gen_8123, q_gen_8122) -> q_gen_8152 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 30 () -> length([nil, z]) -> 30 () -> leq([z, s(nn2)]) -> 30 () -> leq([z, z]) -> 30 () -> reverse([nil, nil]) -> 30 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 33 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 31 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 31 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 34 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 31 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 32 (leq([s(nn1), z])) -> BOT -> 31 } Sat witness: Found: ((length([ll, _xda])) -> length([cons(x, ll), s(_xda)]), { _xda -> s(s(s(z))) ; ll -> cons(z, cons(z, nil)) ; x -> z }) ------------------------------------------- Step 49, which took 0.230673 s (model generation: 0.229174, model checking: 0.001499): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8107, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8118, q_gen_8132}, Q_f={q_gen_8087}, Delta= { () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8109, q_gen_8108) -> q_gen_8132 (q_gen_8094, q_gen_8093) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8109, q_gen_8108) -> q_gen_8118 (q_gen_8109, q_gen_8132) -> q_gen_8118 (q_gen_8110, q_gen_8107) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8109, q_gen_8132) -> q_gen_8087 () -> q_gen_8087 (q_gen_8110, q_gen_8087) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8109, q_gen_8108) -> q_gen_8107 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8116, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { (q_gen_8105, q_gen_8125) -> q_gen_8090 () -> q_gen_8090 (q_gen_8116) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105) -> q_gen_8116 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8116, q_gen_8090) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8126) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 (q_gen_8116) -> q_gen_8091 (q_gen_8116) -> q_gen_8091 () -> q_gen_8091 (q_gen_8091) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8120, q_gen_8122, q_gen_8123}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8120) -> q_gen_8120 (q_gen_8123, q_gen_8122) -> q_gen_8120 (q_gen_8123, q_gen_8122) -> q_gen_8120 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 31 () -> length([nil, z]) -> 31 () -> leq([z, s(nn2)]) -> 31 () -> leq([z, z]) -> 31 () -> reverse([nil, nil]) -> 31 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 33 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 31 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 34 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 34 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 32 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 32 (leq([s(nn1), z])) -> BOT -> 32 } Sat witness: Found: ((length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]), { _bea -> s(s(s(z))) ; _cea -> cons(s(s(z)), nil) ; _dea -> s(z) ; l1 -> cons(z, nil) }) ------------------------------------------- Step 50, which took 0.244259 s (model generation: 0.242274, model checking: 0.001985): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8092, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8150}, Q_f={q_gen_8087, q_gen_8092}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 () -> q_gen_8087 (q_gen_8110, q_gen_8092) -> q_gen_8092 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8109, q_gen_8108) -> q_gen_8092 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 () -> q_gen_8110 (q_gen_8110, q_gen_8087) -> q_gen_8150 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8105, q_gen_8125) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 (q_gen_8091) -> q_gen_8126 (q_gen_8126) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8101, q_gen_8102, q_gen_8113, q_gen_8122, q_gen_8123, q_gen_8145, q_gen_8151}, Q_f={q_gen_8082, q_gen_8101}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8151) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102, q_gen_8082) -> q_gen_8101 (q_gen_8102, q_gen_8101) -> q_gen_8101 (q_gen_8113, q_gen_8082) -> q_gen_8101 (q_gen_8123, q_gen_8122) -> q_gen_8101 (q_gen_8123) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102) -> q_gen_8113 (q_gen_8113, q_gen_8101) -> q_gen_8145 (q_gen_8123, q_gen_8122) -> q_gen_8145 (q_gen_8102, q_gen_8145) -> q_gen_8151 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 31 () -> length([nil, z]) -> 31 () -> leq([z, s(nn2)]) -> 31 () -> leq([z, z]) -> 31 () -> reverse([nil, nil]) -> 31 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 33 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 34 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 34 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 34 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 32 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 32 (leq([s(nn1), z])) -> BOT -> 32 } Sat witness: Found: ((append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]), { _nda -> cons(s(z), cons(z, nil)) ; h1 -> z ; l2 -> cons(s(z), nil) ; t1 -> cons(s(z), cons(z, nil)) }) ------------------------------------------- Step 51, which took 0.280237 s (model generation: 0.278014, model checking: 0.002223): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8092, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8150}, Q_f={q_gen_8087, q_gen_8092}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 () -> q_gen_8087 (q_gen_8110, q_gen_8092) -> q_gen_8092 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8109, q_gen_8108) -> q_gen_8092 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 (q_gen_8109) -> q_gen_8110 () -> q_gen_8110 (q_gen_8110, q_gen_8087) -> q_gen_8150 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8105) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8105, q_gen_8125) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8105) -> q_gen_8091 () -> q_gen_8091 (q_gen_8091) -> q_gen_8126 (q_gen_8126) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8101, q_gen_8102, q_gen_8113, q_gen_8122, q_gen_8123, q_gen_8151, q_gen_8152}, Q_f={q_gen_8082, q_gen_8101}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8151) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102, q_gen_8082) -> q_gen_8101 (q_gen_8102, q_gen_8101) -> q_gen_8101 (q_gen_8113, q_gen_8082) -> q_gen_8101 () -> q_gen_8102 (q_gen_8102) -> q_gen_8113 (q_gen_8123) -> q_gen_8113 (q_gen_8102, q_gen_8152) -> q_gen_8151 (q_gen_8113, q_gen_8101) -> q_gen_8152 (q_gen_8123, q_gen_8122) -> q_gen_8152 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 32 () -> length([nil, z]) -> 32 () -> leq([z, s(nn2)]) -> 32 () -> leq([z, z]) -> 32 () -> reverse([nil, nil]) -> 32 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 36 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 34 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 34 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 34 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 33 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 33 (leq([s(nn1), z])) -> BOT -> 33 } Sat witness: Found: ((append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]), { _sda -> cons(s(z), nil) ; _tda -> cons(s(z), cons(z, nil)) ; h1 -> s(z) ; t1 -> cons(z, nil) }) ------------------------------------------- Step 52, which took 0.565148 s (model generation: 0.561358, model checking: 0.003790): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8107, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8118, q_gen_8132}, Q_f={q_gen_8087}, Delta= { () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8109, q_gen_8108) -> q_gen_8132 (q_gen_8094, q_gen_8093) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 (q_gen_8109, q_gen_8108) -> q_gen_8118 (q_gen_8109, q_gen_8132) -> q_gen_8118 (q_gen_8110, q_gen_8107) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8109, q_gen_8132) -> q_gen_8087 () -> q_gen_8087 (q_gen_8110, q_gen_8087) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8109, q_gen_8108) -> q_gen_8107 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 (q_gen_8109) -> q_gen_8110 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8116, q_gen_8125, q_gen_8126, q_gen_8127, q_gen_8144}, Q_f={q_gen_8086}, Delta= { (q_gen_8105, q_gen_8125) -> q_gen_8090 () -> q_gen_8090 (q_gen_8116) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105) -> q_gen_8116 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8116, q_gen_8090) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8126) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 (q_gen_8116) -> q_gen_8091 () -> q_gen_8091 (q_gen_8091) -> q_gen_8126 (q_gen_8144) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 (q_gen_8144, q_gen_8090) -> q_gen_8127 (q_gen_8144, q_gen_8125) -> q_gen_8127 (q_gen_8116) -> q_gen_8144 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123, q_gen_8151}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8151) -> q_gen_8151 (q_gen_8123, q_gen_8122) -> q_gen_8151 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 33 () -> length([nil, z]) -> 33 () -> leq([z, s(nn2)]) -> 33 () -> leq([z, z]) -> 33 () -> reverse([nil, nil]) -> 33 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 36 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 34 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 34 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 37 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 34 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 34 (leq([s(nn1), z])) -> BOT -> 34 } Sat witness: Found: ((length([ll, _xda])) -> length([cons(x, ll), s(_xda)]), { _xda -> s(s(z)) ; ll -> cons(z, cons(s(z), nil)) ; x -> z }) ------------------------------------------- Step 53, which took 0.486921 s (model generation: 0.483090, model checking: 0.003831): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8092, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8150}, Q_f={q_gen_8087, q_gen_8092}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 () -> q_gen_8087 (q_gen_8110, q_gen_8092) -> q_gen_8092 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8109, q_gen_8108) -> q_gen_8092 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 (q_gen_8109) -> q_gen_8110 () -> q_gen_8110 (q_gen_8110, q_gen_8087) -> q_gen_8150 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8116, q_gen_8125, q_gen_8126, q_gen_8127, q_gen_8139}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 (q_gen_8116) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105) -> q_gen_8116 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8105, q_gen_8125) -> q_gen_8139 (q_gen_8105, q_gen_8139) -> q_gen_8139 (q_gen_8116, q_gen_8090) -> q_gen_8139 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8091, q_gen_8139) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 (q_gen_8126, q_gen_8139) -> q_gen_8086 () -> q_gen_8086 (q_gen_8126) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 (q_gen_8116) -> q_gen_8091 () -> q_gen_8091 (q_gen_8091) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8116) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123, q_gen_8151, q_gen_8152}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8102, q_gen_8151) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8152) -> q_gen_8151 (q_gen_8123, q_gen_8122) -> q_gen_8152 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 34 () -> length([nil, z]) -> 34 () -> leq([z, s(nn2)]) -> 34 () -> leq([z, z]) -> 34 () -> reverse([nil, nil]) -> 34 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 36 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 34 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 37 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 37 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 35 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 35 (leq([s(nn1), z])) -> BOT -> 35 } Sat witness: Found: ((length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]), { _bea -> s(s(s(s(z)))) ; _cea -> cons(z, cons(z, nil)) ; _dea -> s(s(z)) ; l1 -> cons(z, cons(z, nil)) }) ------------------------------------------- Step 54, which took 0.622114 s (model generation: 0.609863, model checking: 0.012251): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8092, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8150}, Q_f={q_gen_8087, q_gen_8092}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 () -> q_gen_8094 () -> q_gen_8087 (q_gen_8110, q_gen_8092) -> q_gen_8092 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8109, q_gen_8108) -> q_gen_8092 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 (q_gen_8109) -> q_gen_8110 () -> q_gen_8110 (q_gen_8110, q_gen_8087) -> q_gen_8150 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8116, q_gen_8125, q_gen_8126, q_gen_8127, q_gen_8144}, Q_f={q_gen_8086}, Delta= { (q_gen_8105, q_gen_8125) -> q_gen_8090 (q_gen_8116, q_gen_8090) -> q_gen_8090 () -> q_gen_8090 () -> q_gen_8105 (q_gen_8105) -> q_gen_8116 (q_gen_8116) -> q_gen_8116 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8126) -> q_gen_8091 (q_gen_8144) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 (q_gen_8116) -> q_gen_8091 () -> q_gen_8091 (q_gen_8091) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 (q_gen_8144, q_gen_8090) -> q_gen_8127 (q_gen_8144, q_gen_8125) -> q_gen_8127 (q_gen_8116) -> q_gen_8144 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123, q_gen_8151, q_gen_8152}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8102, q_gen_8151) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8152) -> q_gen_8151 (q_gen_8123, q_gen_8122) -> q_gen_8152 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 34 () -> length([nil, z]) -> 34 () -> leq([z, s(nn2)]) -> 34 () -> leq([z, z]) -> 34 () -> reverse([nil, nil]) -> 34 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 36 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 37 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 37 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 37 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 35 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 35 (leq([s(nn1), z])) -> BOT -> 35 } Sat witness: Found: ((append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]), { _nda -> cons(z, cons(s(z), nil)) ; h1 -> s(z) ; l2 -> cons(z, cons(s(z), nil)) ; t1 -> nil }) ------------------------------------------- Step 55, which took 1.058067 s (model generation: 1.056329, model checking: 0.001738): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8092, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8150}, Q_f={q_gen_8087, q_gen_8092}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 (q_gen_8109) -> q_gen_8094 () -> q_gen_8094 () -> q_gen_8087 (q_gen_8110, q_gen_8092) -> q_gen_8092 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8109, q_gen_8108) -> q_gen_8092 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 (q_gen_8109) -> q_gen_8110 () -> q_gen_8110 (q_gen_8110, q_gen_8087) -> q_gen_8150 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8116, q_gen_8125, q_gen_8126, q_gen_8127, q_gen_8144}, Q_f={q_gen_8086}, Delta= { (q_gen_8105, q_gen_8125) -> q_gen_8090 (q_gen_8116, q_gen_8090) -> q_gen_8090 () -> q_gen_8090 () -> q_gen_8105 (q_gen_8105) -> q_gen_8116 (q_gen_8116) -> q_gen_8116 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8126) -> q_gen_8091 (q_gen_8144) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 (q_gen_8116) -> q_gen_8091 () -> q_gen_8091 (q_gen_8091) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 (q_gen_8144, q_gen_8090) -> q_gen_8127 (q_gen_8144, q_gen_8125) -> q_gen_8127 (q_gen_8116) -> q_gen_8144 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123, q_gen_8151, q_gen_8152}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8102, q_gen_8151) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8152) -> q_gen_8151 (q_gen_8123, q_gen_8122) -> q_gen_8152 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 35 () -> length([nil, z]) -> 35 () -> leq([z, s(nn2)]) -> 35 () -> leq([z, z]) -> 35 () -> reverse([nil, nil]) -> 35 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 39 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 37 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 37 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 37 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 36 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 36 (leq([s(nn1), z])) -> BOT -> 36 } Sat witness: Found: ((append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]), { _sda -> nil ; _tda -> cons(z, nil) ; h1 -> s(z) ; t1 -> nil }) ------------------------------------------- Step 56, which took 0.859251 s (model generation: 0.814440, model checking: 0.044811): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8092, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8150}, Q_f={q_gen_8087, q_gen_8092}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 (q_gen_8109) -> q_gen_8094 () -> q_gen_8094 () -> q_gen_8087 (q_gen_8110, q_gen_8092) -> q_gen_8092 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8109, q_gen_8108) -> q_gen_8092 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 (q_gen_8109) -> q_gen_8110 () -> q_gen_8110 (q_gen_8110, q_gen_8087) -> q_gen_8150 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8116, q_gen_8125, q_gen_8126, q_gen_8127, q_gen_8144}, Q_f={q_gen_8086}, Delta= { (q_gen_8105, q_gen_8125) -> q_gen_8090 (q_gen_8116, q_gen_8090) -> q_gen_8090 () -> q_gen_8090 () -> q_gen_8105 (q_gen_8105) -> q_gen_8116 (q_gen_8116) -> q_gen_8116 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8126) -> q_gen_8091 (q_gen_8144) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 (q_gen_8116) -> q_gen_8091 () -> q_gen_8091 (q_gen_8091) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 (q_gen_8144, q_gen_8090) -> q_gen_8127 (q_gen_8144, q_gen_8125) -> q_gen_8127 (q_gen_8116) -> q_gen_8144 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123, q_gen_8151, q_gen_8152}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8102, q_gen_8151) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8152) -> q_gen_8151 (q_gen_8123, q_gen_8122) -> q_gen_8152 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 36 () -> length([nil, z]) -> 36 () -> leq([z, s(nn2)]) -> 36 () -> leq([z, z]) -> 36 () -> reverse([nil, nil]) -> 36 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 39 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 37 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 37 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 40 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 37 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 37 (leq([s(nn1), z])) -> BOT -> 37 } Sat witness: Found: ((length([ll, _xda])) -> length([cons(x, ll), s(_xda)]), { _xda -> s(s(s(z))) ; ll -> cons(s(z), nil) ; x -> z }) ------------------------------------------- Step 57, which took 7.138043 s (model generation: 7.108435, model checking: 0.029608): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8092, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8150}, Q_f={q_gen_8087, q_gen_8092}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 (q_gen_8109) -> q_gen_8094 () -> q_gen_8094 () -> q_gen_8087 (q_gen_8110, q_gen_8092) -> q_gen_8092 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8109, q_gen_8108) -> q_gen_8092 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 (q_gen_8109) -> q_gen_8110 () -> q_gen_8110 (q_gen_8110, q_gen_8087) -> q_gen_8150 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8116, q_gen_8125, q_gen_8126, q_gen_8127, q_gen_8186}, Q_f={q_gen_8086}, Delta= { (q_gen_8105, q_gen_8125) -> q_gen_8090 (q_gen_8116, q_gen_8090) -> q_gen_8090 () -> q_gen_8090 () -> q_gen_8105 (q_gen_8105) -> q_gen_8116 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8116) -> q_gen_8186 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8126) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 (q_gen_8116) -> q_gen_8091 (q_gen_8186) -> q_gen_8091 (q_gen_8186) -> q_gen_8091 () -> q_gen_8091 (q_gen_8091) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8116) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123, q_gen_8151, q_gen_8152}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8102, q_gen_8151) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8152) -> q_gen_8151 (q_gen_8123, q_gen_8122) -> q_gen_8152 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 37 () -> length([nil, z]) -> 37 () -> leq([z, s(nn2)]) -> 37 () -> leq([z, z]) -> 37 () -> reverse([nil, nil]) -> 37 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 39 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 37 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 40 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 40 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 38 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 38 (leq([s(nn1), z])) -> BOT -> 38 } Sat witness: Found: ((length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]), { _bea -> s(s(s(z))) ; _cea -> cons(z, cons(z, nil)) ; _dea -> s(s(z)) ; l1 -> cons(z, cons(z, nil)) }) ------------------------------------------- Step 58, which took 7.844005 s (model generation: 7.834874, model checking: 0.009131): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8107, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8118, q_gen_8132}, Q_f={q_gen_8087}, Delta= { () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8109, q_gen_8108) -> q_gen_8132 (q_gen_8094, q_gen_8093) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 (q_gen_8109) -> q_gen_8094 () -> q_gen_8094 (q_gen_8109, q_gen_8108) -> q_gen_8118 (q_gen_8109, q_gen_8132) -> q_gen_8118 (q_gen_8110, q_gen_8107) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 (q_gen_8109, q_gen_8132) -> q_gen_8087 () -> q_gen_8087 (q_gen_8110, q_gen_8087) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8094, q_gen_8118) -> q_gen_8107 (q_gen_8109, q_gen_8108) -> q_gen_8107 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 (q_gen_8109) -> q_gen_8110 () -> q_gen_8110 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8116, q_gen_8125, q_gen_8126, q_gen_8127}, Q_f={q_gen_8086}, Delta= { (q_gen_8105, q_gen_8125) -> q_gen_8090 () -> q_gen_8090 (q_gen_8116) -> q_gen_8105 () -> q_gen_8105 (q_gen_8105) -> q_gen_8116 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8116, q_gen_8090) -> q_gen_8125 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8126) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 (q_gen_8116) -> q_gen_8091 (q_gen_8116) -> q_gen_8091 () -> q_gen_8091 (q_gen_8091) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8096, q_gen_8128}, Q_f={q_gen_8083}, Delta= { () -> q_gen_8085 (q_gen_8085) -> q_gen_8096 (q_gen_8083) -> q_gen_8083 (q_gen_8096) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 (q_gen_8096) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8120, q_gen_8122, q_gen_8123}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8120) -> q_gen_8120 (q_gen_8123, q_gen_8122) -> q_gen_8120 (q_gen_8123, q_gen_8122) -> q_gen_8120 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 37 () -> length([nil, z]) -> 37 () -> leq([z, s(nn2)]) -> 37 () -> leq([z, z]) -> 37 () -> reverse([nil, nil]) -> 37 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 39 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 40 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 40 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 40 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 38 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 38 (leq([s(nn1), z])) -> BOT -> 38 } Sat witness: Found: ((append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]), { _nda -> cons(z, cons(z, nil)) ; h1 -> z ; l2 -> nil ; t1 -> nil }) ------------------------------------------- Step 59, which took 8.637352 s (model generation: 8.543653, model checking: 0.093699): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8092, q_gen_8093, q_gen_8094, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8150}, Q_f={q_gen_8087, q_gen_8092}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 (q_gen_8109, q_gen_8108) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 (q_gen_8109) -> q_gen_8094 () -> q_gen_8094 () -> q_gen_8087 (q_gen_8110, q_gen_8092) -> q_gen_8092 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8094, q_gen_8093) -> q_gen_8092 (q_gen_8109, q_gen_8108) -> q_gen_8092 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 (q_gen_8109) -> q_gen_8110 () -> q_gen_8110 (q_gen_8110, q_gen_8087) -> q_gen_8150 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8116, q_gen_8125, q_gen_8126, q_gen_8127, q_gen_8144, q_gen_8186}, Q_f={q_gen_8086}, Delta= { (q_gen_8105, q_gen_8125) -> q_gen_8090 (q_gen_8116, q_gen_8090) -> q_gen_8090 () -> q_gen_8090 () -> q_gen_8105 (q_gen_8105) -> q_gen_8116 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8116) -> q_gen_8186 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 () -> q_gen_8086 (q_gen_8126) -> q_gen_8091 (q_gen_8144) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 (q_gen_8116) -> q_gen_8091 (q_gen_8186) -> q_gen_8091 (q_gen_8186) -> q_gen_8091 () -> q_gen_8091 (q_gen_8091) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 (q_gen_8144, q_gen_8090) -> q_gen_8127 (q_gen_8144, q_gen_8125) -> q_gen_8127 (q_gen_8116) -> q_gen_8144 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8121, q_gen_8122, q_gen_8123, q_gen_8152}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8102, q_gen_8121) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8152) -> q_gen_8121 (q_gen_8123, q_gen_8122) -> q_gen_8121 (q_gen_8123, q_gen_8122) -> q_gen_8152 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 38 () -> length([nil, z]) -> 38 () -> leq([z, s(nn2)]) -> 38 () -> leq([z, z]) -> 38 () -> reverse([nil, nil]) -> 38 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 40 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 40 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 40 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 43 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 39 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 39 (leq([s(nn1), z])) -> BOT -> 39 } Sat witness: Found: ((length([ll, _xda])) -> length([cons(x, ll), s(_xda)]), { _xda -> s(z) ; ll -> cons(s(z), cons(s(z), nil)) ; x -> s(z) }) ------------------------------------------- Step 60, which took 9.257794 s (model generation: 9.226696, model checking: 0.031098): Model: |_ { append -> {{{ Q={q_gen_8087, q_gen_8093, q_gen_8094, q_gen_8097, q_gen_8108, q_gen_8109, q_gen_8110, q_gen_8118, q_gen_8119}, Q_f={q_gen_8087, q_gen_8097}, Delta= { (q_gen_8109, q_gen_8108) -> q_gen_8108 () -> q_gen_8108 (q_gen_8109) -> q_gen_8109 () -> q_gen_8109 (q_gen_8094, q_gen_8093) -> q_gen_8093 () -> q_gen_8093 (q_gen_8094) -> q_gen_8094 (q_gen_8109) -> q_gen_8094 () -> q_gen_8094 (q_gen_8109, q_gen_8108) -> q_gen_8118 (q_gen_8110, q_gen_8119) -> q_gen_8087 (q_gen_8094, q_gen_8093) -> q_gen_8087 () -> q_gen_8087 (q_gen_8110, q_gen_8097) -> q_gen_8097 (q_gen_8094, q_gen_8118) -> q_gen_8097 (q_gen_8094, q_gen_8093) -> q_gen_8097 (q_gen_8109, q_gen_8108) -> q_gen_8097 (q_gen_8110) -> q_gen_8110 (q_gen_8094) -> q_gen_8110 (q_gen_8109) -> q_gen_8110 () -> q_gen_8110 (q_gen_8110, q_gen_8087) -> q_gen_8119 (q_gen_8094, q_gen_8118) -> q_gen_8119 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_8086, q_gen_8090, q_gen_8091, q_gen_8105, q_gen_8116, q_gen_8125, q_gen_8126, q_gen_8127, q_gen_8139, q_gen_8144}, Q_f={q_gen_8086}, Delta= { () -> q_gen_8090 () -> q_gen_8105 (q_gen_8105) -> q_gen_8116 (q_gen_8116) -> q_gen_8116 (q_gen_8105, q_gen_8090) -> q_gen_8125 (q_gen_8105, q_gen_8125) -> q_gen_8139 (q_gen_8105, q_gen_8139) -> q_gen_8139 (q_gen_8116, q_gen_8090) -> q_gen_8139 (q_gen_8116, q_gen_8139) -> q_gen_8139 (q_gen_8091, q_gen_8090) -> q_gen_8086 (q_gen_8091, q_gen_8139) -> q_gen_8086 (q_gen_8126, q_gen_8125) -> q_gen_8086 (q_gen_8126, q_gen_8139) -> q_gen_8086 (q_gen_8144, q_gen_8139) -> q_gen_8086 () -> q_gen_8086 (q_gen_8126) -> q_gen_8091 (q_gen_8105) -> q_gen_8091 (q_gen_8116) -> q_gen_8091 () -> q_gen_8091 (q_gen_8091) -> q_gen_8126 (q_gen_8144) -> q_gen_8126 (q_gen_8105) -> q_gen_8126 (q_gen_8091, q_gen_8125) -> q_gen_8127 (q_gen_8126, q_gen_8090) -> q_gen_8127 (q_gen_8144, q_gen_8090) -> q_gen_8127 (q_gen_8144, q_gen_8125) -> q_gen_8127 (q_gen_8116) -> q_gen_8144 } Datatype: Convolution form: left }}} ; leq -> {{{ Q={q_gen_8083, q_gen_8085, q_gen_8128}, Q_f={q_gen_8083}, Delta= { (q_gen_8085) -> q_gen_8085 () -> q_gen_8085 (q_gen_8083) -> q_gen_8083 (q_gen_8085) -> q_gen_8083 () -> q_gen_8083 (q_gen_8128) -> q_gen_8128 (q_gen_8085) -> q_gen_8128 } Datatype: Convolution form: left }}} ; reverse -> {{{ Q={q_gen_8082, q_gen_8102, q_gen_8122, q_gen_8123, q_gen_8151}, Q_f={q_gen_8082}, Delta= { (q_gen_8123, q_gen_8122) -> q_gen_8122 () -> q_gen_8122 (q_gen_8123) -> q_gen_8123 () -> q_gen_8123 (q_gen_8102, q_gen_8082) -> q_gen_8082 (q_gen_8123, q_gen_8122) -> q_gen_8082 () -> q_gen_8082 (q_gen_8102) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 (q_gen_8123) -> q_gen_8102 () -> q_gen_8102 (q_gen_8102, q_gen_8151) -> q_gen_8151 (q_gen_8123, q_gen_8122) -> q_gen_8151 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> append([nil, l2, l2]) -> 39 () -> length([nil, z]) -> 39 () -> leq([z, s(nn2)]) -> 39 () -> leq([z, z]) -> 39 () -> reverse([nil, nil]) -> 39 (append([_sda, cons(h1, nil), _tda]) /\ reverse([t1, _sda])) -> reverse([cons(h1, t1), _tda]) -> 40 (append([t1, l2, _nda])) -> append([cons(h1, t1), l2, cons(h1, _nda)]) -> 40 (length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]) -> 43 (length([ll, _xda])) -> length([cons(x, ll), s(_xda)]) -> 43 (leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 40 (leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 40 (leq([s(nn1), z])) -> BOT -> 40 } Sat witness: Found: ((length([_cea, _dea]) /\ length([l1, _bea]) /\ reverse([l1, _cea])) -> leq([_bea, _dea]), { _bea -> s(s(s(z))) ; _cea -> cons(z, cons(s(z), nil)) ; _dea -> s(z) ; l1 -> cons(s(z), nil) }) Total time: 60.004326 Reason for stopping: DontKnow. Stopped because: timeout