Inference procedure has parameters: Ice fuel: 200 Timeout: 60s Convolution: left Learning problem is: env: { nat -> {s, z} ; natlist -> {cons, nil} } definition: { (le, P: {() -> le([z, s(nn2)]) (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) (le([s(nn1), z])) -> BOT (le([z, z])) -> BOT} ) (length, F: {() -> length([nil, z]) (length([ll, _uca])) -> length([cons(x, ll), s(_uca)])} (length([_vca, _wca]) /\ length([_vca, _xca])) -> eq_nat([_wca, _xca]) ) } properties: {(length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca])} over-approximation: {length} under-approximation: {le} Clause system for inference is: { () -> le([z, s(nn2)]) -> 0 () -> length([nil, z]) -> 0 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 0 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 0 (le([s(nn1), z])) -> BOT -> 0 (le([z, z])) -> BOT -> 0 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 0 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 0 } Solving took 2104.585646 seconds. DontKnow. Stopped because: timeout Working model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7884, q_gen_7885, q_gen_7886, q_gen_7897, q_gen_7898, q_gen_7903, q_gen_7910, q_gen_7911, q_gen_7912, q_gen_7918, q_gen_7926, q_gen_7927, q_gen_7928, q_gen_7929, q_gen_7930, q_gen_7938, q_gen_7939, q_gen_7947, q_gen_7961, q_gen_7975, q_gen_7976, q_gen_7977, q_gen_7987, q_gen_7988, q_gen_8003}, Q_f={}, Delta= { () -> q_gen_7880 (q_gen_7880) -> q_gen_7886 (q_gen_7886) -> q_gen_7930 (q_gen_7930) -> q_gen_7988 (q_gen_7880) -> q_gen_7879 (q_gen_7879) -> q_gen_7884 (q_gen_7886) -> q_gen_7885 (q_gen_7898) -> q_gen_7897 () -> q_gen_7898 (q_gen_7897) -> q_gen_7903 (q_gen_7911) -> q_gen_7910 (q_gen_7912) -> q_gen_7911 (q_gen_7880) -> q_gen_7912 (q_gen_7903) -> q_gen_7918 (q_gen_7927) -> q_gen_7926 (q_gen_7928) -> q_gen_7927 (q_gen_7886) -> q_gen_7928 (q_gen_7930) -> q_gen_7929 (q_gen_7939) -> q_gen_7938 (q_gen_7910) -> q_gen_7939 (q_gen_7926) -> q_gen_7947 (q_gen_7918) -> q_gen_7961 (q_gen_7976) -> q_gen_7975 (q_gen_7977) -> q_gen_7976 (q_gen_7930) -> q_gen_7977 (q_gen_7988) -> q_gen_7987 (q_gen_7947) -> q_gen_8003 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7881, q_gen_7882, q_gen_7883, q_gen_7887, q_gen_7888, q_gen_7889, q_gen_7890, q_gen_7891, q_gen_7892, q_gen_7893, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7899, q_gen_7900, q_gen_7901, q_gen_7902, q_gen_7904, q_gen_7905, q_gen_7906, q_gen_7907, q_gen_7908, q_gen_7909, q_gen_7913, q_gen_7914, q_gen_7915, q_gen_7916, q_gen_7917, q_gen_7919, q_gen_7920, q_gen_7921, q_gen_7922, q_gen_7923, q_gen_7924, q_gen_7925, q_gen_7931, q_gen_7932, q_gen_7933, q_gen_7934, q_gen_7935, q_gen_7936, q_gen_7937, q_gen_7940, q_gen_7941, q_gen_7942, q_gen_7943, q_gen_7944, q_gen_7945, q_gen_7946, q_gen_7948, q_gen_7949, q_gen_7950, q_gen_7951, q_gen_7952, q_gen_7953, q_gen_7954, q_gen_7955, q_gen_7956, q_gen_7957, q_gen_7958, q_gen_7959, q_gen_7960, q_gen_7962, q_gen_7963, q_gen_7964, q_gen_7965, q_gen_7966, q_gen_7967, q_gen_7968, q_gen_7969, q_gen_7970, q_gen_7971, q_gen_7972, q_gen_7973, q_gen_7974, q_gen_7978, q_gen_7979, q_gen_7980, q_gen_7981, q_gen_7982, q_gen_7983, q_gen_7984, q_gen_7985, q_gen_7986, q_gen_7989, q_gen_7990, q_gen_7991, q_gen_7992, q_gen_7993, q_gen_7994, q_gen_7995, q_gen_7996, q_gen_7997, q_gen_7998, q_gen_7999, q_gen_8000, q_gen_8001, q_gen_8002, q_gen_8004, q_gen_8005, q_gen_8006, q_gen_8007, q_gen_8008, q_gen_8009, q_gen_8010, q_gen_8011, q_gen_8012, q_gen_8013, q_gen_8014, q_gen_8015, q_gen_8016, q_gen_8017, q_gen_8018, q_gen_8019, q_gen_8020, q_gen_8021, q_gen_8022, q_gen_8023, q_gen_8024}, Q_f={}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7907, q_gen_7882) -> q_gen_7920 (q_gen_7907) -> q_gen_7924 (q_gen_7924, q_gen_7882) -> q_gen_7932 (q_gen_7889, q_gen_7920) -> q_gen_7934 (q_gen_7889, q_gen_7934) -> q_gen_7937 (q_gen_7892, q_gen_7882) -> q_gen_7941 (q_gen_7889, q_gen_7941) -> q_gen_7949 (q_gen_7889, q_gen_7949) -> q_gen_7951 (q_gen_7889, q_gen_7951) -> q_gen_7956 (q_gen_7889, q_gen_7959) -> q_gen_7958 (q_gen_7889, q_gen_7937) -> q_gen_7959 (q_gen_7889, q_gen_7909) -> q_gen_7966 (q_gen_7889, q_gen_7966) -> q_gen_7968 (q_gen_7892, q_gen_7951) -> q_gen_7983 (q_gen_7892, q_gen_7894) -> q_gen_7986 (q_gen_7889, q_gen_7991) -> q_gen_7990 (q_gen_7892, q_gen_7909) -> q_gen_7991 (q_gen_7889, q_gen_7990) -> q_gen_7993 (q_gen_7889, q_gen_7996) -> q_gen_7995 (q_gen_7892, q_gen_7941) -> q_gen_7996 (q_gen_7924) -> q_gen_8000 (q_gen_7889, q_gen_8006) -> q_gen_8005 (q_gen_7889, q_gen_8007) -> q_gen_8006 (q_gen_7892, q_gen_7932) -> q_gen_8007 (q_gen_7889, q_gen_8005) -> q_gen_8009 (q_gen_7889, q_gen_8013) -> q_gen_8012 (q_gen_7889, q_gen_8014) -> q_gen_8013 (q_gen_7889, q_gen_7986) -> q_gen_8014 (q_gen_7889, q_gen_8012) -> q_gen_8016 (q_gen_8000, q_gen_7920) -> q_gen_8024 () -> q_gen_7878 (q_gen_7883, q_gen_7882) -> q_gen_7881 () -> q_gen_7883 (q_gen_7888, q_gen_7882) -> q_gen_7887 (q_gen_7889) -> q_gen_7888 (q_gen_7891, q_gen_7882) -> q_gen_7890 (q_gen_7892) -> q_gen_7891 (q_gen_7895, q_gen_7894) -> q_gen_7893 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7900) -> q_gen_7899 (q_gen_7892) -> q_gen_7901 (q_gen_7895, q_gen_7882) -> q_gen_7902 (q_gen_7895, q_gen_7900) -> q_gen_7904 (q_gen_7906, q_gen_7882) -> q_gen_7905 (q_gen_7907) -> q_gen_7906 (q_gen_7895, q_gen_7909) -> q_gen_7908 (q_gen_7901, q_gen_7882) -> q_gen_7913 (q_gen_7915, q_gen_7894) -> q_gen_7914 (q_gen_7907) -> q_gen_7915 (q_gen_7915, q_gen_7909) -> q_gen_7916 (q_gen_7901, q_gen_7894) -> q_gen_7917 (q_gen_7895, q_gen_7920) -> q_gen_7919 (q_gen_7901, q_gen_7909) -> q_gen_7921 (q_gen_7923, q_gen_7882) -> q_gen_7922 (q_gen_7924) -> q_gen_7923 (q_gen_7915, q_gen_7882) -> q_gen_7925 (q_gen_7895, q_gen_7932) -> q_gen_7931 (q_gen_7935, q_gen_7934) -> q_gen_7933 (q_gen_7924) -> q_gen_7935 (q_gen_7915, q_gen_7937) -> q_gen_7936 (q_gen_7942, q_gen_7941) -> q_gen_7940 (q_gen_7883) -> q_gen_7942 (q_gen_7883, q_gen_7941) -> q_gen_7943 (q_gen_7895, q_gen_7941) -> q_gen_7944 (q_gen_7935, q_gen_7920) -> q_gen_7945 (q_gen_7901, q_gen_7934) -> q_gen_7946 (q_gen_7901, q_gen_7949) -> q_gen_7948 (q_gen_7952, q_gen_7951) -> q_gen_7950 (q_gen_7901) -> q_gen_7952 (q_gen_7952, q_gen_7882) -> q_gen_7953 (q_gen_7915, q_gen_7951) -> q_gen_7954 (q_gen_7935, q_gen_7956) -> q_gen_7955 (q_gen_7952, q_gen_7958) -> q_gen_7957 (q_gen_7915, q_gen_7959) -> q_gen_7960 (q_gen_7915, q_gen_7920) -> q_gen_7962 (q_gen_7942, q_gen_7949) -> q_gen_7963 (q_gen_7888, q_gen_7934) -> q_gen_7964 (q_gen_7915, q_gen_7966) -> q_gen_7965 (q_gen_7935, q_gen_7968) -> q_gen_7967 (q_gen_7935, q_gen_7941) -> q_gen_7969 (q_gen_7901, q_gen_7920) -> q_gen_7970 (q_gen_7915, q_gen_7934) -> q_gen_7971 (q_gen_7895, q_gen_7934) -> q_gen_7972 (q_gen_7942, q_gen_7894) -> q_gen_7973 (q_gen_7935, q_gen_7882) -> q_gen_7974 (q_gen_7935, q_gen_7966) -> q_gen_7978 (q_gen_7895, q_gen_7937) -> q_gen_7979 (q_gen_7935, q_gen_7894) -> q_gen_7980 (q_gen_7952, q_gen_7909) -> q_gen_7981 (q_gen_7935, q_gen_7983) -> q_gen_7982 (q_gen_7942, q_gen_7909) -> q_gen_7984 (q_gen_7901, q_gen_7986) -> q_gen_7985 (q_gen_7901, q_gen_7990) -> q_gen_7989 (q_gen_7952, q_gen_7993) -> q_gen_7992 (q_gen_7942, q_gen_7995) -> q_gen_7994 (q_gen_7901, q_gen_7996) -> q_gen_7997 (q_gen_7999, q_gen_7882) -> q_gen_7998 (q_gen_8000) -> q_gen_7999 (q_gen_8002, q_gen_7934) -> q_gen_8001 (q_gen_8000) -> q_gen_8002 (q_gen_7935, q_gen_8005) -> q_gen_8004 (q_gen_8002, q_gen_8009) -> q_gen_8008 (q_gen_8002, q_gen_7920) -> q_gen_8010 (q_gen_8002, q_gen_8012) -> q_gen_8011 (q_gen_8017, q_gen_8016) -> q_gen_8015 (q_gen_8018) -> q_gen_8017 (q_gen_7935) -> q_gen_8018 (q_gen_8020, q_gen_7920) -> q_gen_8019 (q_gen_8021) -> q_gen_8020 (q_gen_8022) -> q_gen_8021 (q_gen_7888) -> q_gen_8022 (q_gen_7901, q_gen_8024) -> q_gen_8023 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.029702 s (model generation: 0.029531, model checking: 0.000171): Model: |_ { le -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} ; length -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 0 () -> length([nil, z]) -> 3 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 1 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 1 (le([s(nn1), z])) -> BOT -> 1 (le([z, z])) -> BOT -> 1 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 1 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 1 } Sat witness: Found: (() -> length([nil, z]), { }) ------------------------------------------- Step 1, which took 0.010703 s (model generation: 0.010204, model checking: 0.000499): Model: |_ { le -> {{{ Q={}, Q_f={}, Delta= { } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7878 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 3 () -> length([nil, z]) -> 3 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 1 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 1 (le([s(nn1), z])) -> BOT -> 1 (le([z, z])) -> BOT -> 1 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 1 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 1 } Sat witness: Found: (() -> le([z, s(nn2)]), { nn2 -> z }) ------------------------------------------- Step 2, which took 0.009573 s (model generation: 0.009413, model checking: 0.000160): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880}, Q_f={q_gen_7879}, Delta= { () -> q_gen_7880 (q_gen_7880) -> q_gen_7879 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7878 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 3 () -> length([nil, z]) -> 3 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 1 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 1 (le([s(nn1), z])) -> BOT -> 1 (le([z, z])) -> BOT -> 1 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 1 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 4 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> z ; ll -> nil ; x -> z }) ------------------------------------------- Step 3, which took 0.012195 s (model generation: 0.011927, model checking: 0.000268): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880}, Q_f={q_gen_7879}, Delta= { () -> q_gen_7880 (q_gen_7880) -> q_gen_7879 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 (q_gen_7883, q_gen_7882) -> q_gen_7878 () -> q_gen_7878 () -> q_gen_7883 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 3 () -> length([nil, z]) -> 3 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 2 (le([s(nn1), z])) -> BOT -> 2 (le([z, z])) -> BOT -> 2 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 2 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 4 } Sat witness: Found: ((le([nn1, nn2])) -> le([s(nn1), s(nn2)]), { nn1 -> z ; nn2 -> s(z) }) ------------------------------------------- Step 4, which took 0.025466 s (model generation: 0.025048, model checking: 0.000418): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880}, Q_f={q_gen_7879}, Delta= { () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 (q_gen_7883, q_gen_7882) -> q_gen_7878 () -> q_gen_7878 () -> q_gen_7883 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 6 () -> length([nil, z]) -> 4 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 3 (le([s(nn1), z])) -> BOT -> 3 (le([z, z])) -> BOT -> 3 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 3 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 4 } Sat witness: Found: (() -> le([z, s(nn2)]), { nn2 -> s(z) }) ------------------------------------------- Step 5, which took 0.020483 s (model generation: 0.020031, model checking: 0.000452): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 (q_gen_7883, q_gen_7882) -> q_gen_7878 () -> q_gen_7878 () -> q_gen_7883 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 6 () -> length([nil, z]) -> 4 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 4 (le([s(nn1), z])) -> BOT -> 4 (le([z, z])) -> BOT -> 4 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 4 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 7 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> z ; ll -> nil ; x -> s(z) }) ------------------------------------------- Step 6, which took 0.014588 s (model generation: 0.013472, model checking: 0.001116): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7883, q_gen_7882) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 () -> q_gen_7883 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 7 () -> length([nil, z]) -> 5 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 5 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 5 (le([s(nn1), z])) -> BOT -> 5 (le([z, z])) -> BOT -> 5 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 5 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 10 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> z ; ll -> nil ; x -> s(s(z)) }) ------------------------------------------- Step 7, which took 0.011680 s (model generation: 0.011104, model checking: 0.000576): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 (q_gen_7889) -> q_gen_7889 () -> q_gen_7889 (q_gen_7883, q_gen_7882) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 () -> q_gen_7883 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 8 () -> length([nil, z]) -> 6 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 6 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 6 (le([s(nn1), z])) -> BOT -> 6 (le([z, z])) -> BOT -> 6 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 6 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 13 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> s(z) ; ll -> cons(z, nil) ; x -> z }) ------------------------------------------- Step 8, which took 0.010474 s (model generation: 0.010106, model checking: 0.000368): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7882) -> q_gen_7882 () -> q_gen_7882 (q_gen_7889) -> q_gen_7889 () -> q_gen_7889 (q_gen_7883, q_gen_7882) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7889) -> q_gen_7883 () -> q_gen_7883 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 8 () -> length([nil, z]) -> 6 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 6 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 6 (le([s(nn1), z])) -> BOT -> 6 (le([z, z])) -> BOT -> 6 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 9 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 13 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(z) ; _zca -> s(z) ; l -> cons(z, nil) ; x -> z }) ------------------------------------------- Step 9, which took 0.010554 s (model generation: 0.010537, model checking: 0.000017): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 () -> q_gen_7879 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7882) -> q_gen_7882 () -> q_gen_7882 (q_gen_7889) -> q_gen_7889 () -> q_gen_7889 (q_gen_7883, q_gen_7882) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7889) -> q_gen_7883 () -> q_gen_7883 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 8 () -> length([nil, z]) -> 6 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 6 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 6 (le([s(nn1), z])) -> BOT -> 6 (le([z, z])) -> BOT -> 9 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 9 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 13 } Sat witness: Found: ((le([z, z])) -> BOT, { }) ------------------------------------------- Step 10, which took 0.011763 s (model generation: 0.011686, model checking: 0.000077): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7898}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7898) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 () -> q_gen_7898 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7882) -> q_gen_7882 () -> q_gen_7882 (q_gen_7889) -> q_gen_7889 () -> q_gen_7889 (q_gen_7883, q_gen_7882) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7889) -> q_gen_7883 () -> q_gen_7883 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 8 () -> length([nil, z]) -> 6 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 6 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 9 (le([s(nn1), z])) -> BOT -> 7 (le([z, z])) -> BOT -> 9 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 9 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 13 } Sat witness: Found: ((le([s(nn1), s(nn2)])) -> le([nn1, nn2]), { nn1 -> z ; nn2 -> z }) ------------------------------------------- Step 11, which took 0.012810 s (model generation: 0.011108, model checking: 0.001702): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7894, q_gen_7895, q_gen_7896}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 (q_gen_7889) -> q_gen_7889 () -> q_gen_7889 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 9 () -> length([nil, z]) -> 7 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 7 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 10 (le([s(nn1), z])) -> BOT -> 8 (le([z, z])) -> BOT -> 10 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 10 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 16 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> s(s(z)) ; ll -> cons(z, cons(z, nil)) ; x -> z }) ------------------------------------------- Step 12, which took 0.013013 s (model generation: 0.012008, model checking: 0.001005): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7894, q_gen_7895, q_gen_7896}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7894) -> q_gen_7882 () -> q_gen_7882 (q_gen_7889) -> q_gen_7889 () -> q_gen_7889 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 10 () -> length([nil, z]) -> 8 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 8 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 10 (le([s(nn1), z])) -> BOT -> 9 (le([z, z])) -> BOT -> 10 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 13 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 16 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(z)) ; _zca -> s(s(z)) ; l -> cons(z, nil) ; x -> z }) ------------------------------------------- Step 13, which took 0.013486 s (model generation: 0.012854, model checking: 0.000632): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7894, q_gen_7895, q_gen_7896}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 (q_gen_7889) -> q_gen_7889 () -> q_gen_7889 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7894 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 11 () -> length([nil, z]) -> 9 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 9 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 11 (le([s(nn1), z])) -> BOT -> 10 (le([z, z])) -> BOT -> 11 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 16 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 16 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(z)) ; _zca -> s(s(z)) ; l -> cons(z, cons(z, nil)) ; x -> z }) ------------------------------------------- Step 14, which took 0.017542 s (model generation: 0.015908, model checking: 0.001634): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7894) -> q_gen_7882 () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 12 () -> length([nil, z]) -> 10 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 10 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 12 (le([s(nn1), z])) -> BOT -> 11 (le([z, z])) -> BOT -> 12 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 16 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 19 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> z ; ll -> nil ; x -> s(s(s(z))) }) ------------------------------------------- Step 15, which took 0.016222 s (model generation: 0.015852, model checking: 0.000370): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897, q_gen_7898}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7897) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7898) -> q_gen_7897 () -> q_gen_7898 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7888, q_gen_7889, q_gen_7894, q_gen_7896}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 (q_gen_7889) -> q_gen_7889 () -> q_gen_7889 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7894 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7888, q_gen_7882) -> q_gen_7878 (q_gen_7888, q_gen_7894) -> q_gen_7878 () -> q_gen_7878 () -> q_gen_7883 (q_gen_7889) -> q_gen_7888 (q_gen_7889) -> q_gen_7888 (q_gen_7883, q_gen_7894) -> q_gen_7896 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 12 () -> length([nil, z]) -> 11 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 11 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 15 (le([s(nn1), z])) -> BOT -> 12 (le([z, z])) -> BOT -> 13 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 16 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 19 } Sat witness: Found: ((le([s(nn1), s(nn2)])) -> le([nn1, nn2]), { nn1 -> s(z) ; nn2 -> s(z) }) ------------------------------------------- Step 16, which took 0.023754 s (model generation: 0.021312, model checking: 0.002442): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7894) -> q_gen_7882 () -> q_gen_7882 (q_gen_7892) -> q_gen_7889 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 13 () -> length([nil, z]) -> 12 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 12 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 16 (le([s(nn1), z])) -> BOT -> 13 (le([z, z])) -> BOT -> 14 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 19 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 19 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(s(z))) ; _zca -> s(s(z)) ; l -> cons(z, cons(z, cons(z, nil))) ; x -> z }) ------------------------------------------- Step 17, which took 0.018689 s (model generation: 0.018466, model checking: 0.000223): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7894) -> q_gen_7882 () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7892) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 13 () -> length([nil, z]) -> 13 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 13 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 16 (le([s(nn1), z])) -> BOT -> 16 (le([z, z])) -> BOT -> 14 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 19 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 19 } Sat witness: Found: ((le([s(nn1), z])) -> BOT, { nn1 -> z }) ------------------------------------------- Step 18, which took 0.021790 s (model generation: 0.020166, model checking: 0.001624): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7892) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7889, q_gen_7900) -> q_gen_7900 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7883, q_gen_7900) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 14 () -> length([nil, z]) -> 14 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 14 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 17 (le([s(nn1), z])) -> BOT -> 17 (le([z, z])) -> BOT -> 15 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 19 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 22 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> s(s(s(z))) ; ll -> cons(z, nil) ; x -> z }) ------------------------------------------- Step 19, which took 0.023164 s (model generation: 0.021729, model checking: 0.001435): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 (q_gen_7892) -> q_gen_7889 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7889, q_gen_7900) -> q_gen_7900 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7883, q_gen_7900) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 15 () -> length([nil, z]) -> 15 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 15 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 18 (le([s(nn1), z])) -> BOT -> 18 (le([z, z])) -> BOT -> 16 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 22 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 22 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(s(z))) ; _zca -> s(s(z)) ; l -> cons(z, nil) ; x -> z }) ------------------------------------------- Step 20, which took 0.023479 s (model generation: 0.022770, model checking: 0.000709): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897, q_gen_7912}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7912) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 () -> q_gen_7897 (q_gen_7880) -> q_gen_7912 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7894) -> q_gen_7882 () -> q_gen_7882 (q_gen_7892) -> q_gen_7889 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 16 () -> length([nil, z]) -> 16 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 16 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 21 (le([s(nn1), z])) -> BOT -> 19 (le([z, z])) -> BOT -> 17 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 22 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 22 } Sat witness: Found: ((le([s(nn1), s(nn2)])) -> le([nn1, nn2]), { nn1 -> s(z) ; nn2 -> z }) ------------------------------------------- Step 21, which took 0.021896 s (model generation: 0.021412, model checking: 0.000484): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897, q_gen_7911, q_gen_7912}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7911) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 () -> q_gen_7897 (q_gen_7912) -> q_gen_7911 (q_gen_7880) -> q_gen_7912 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7894) -> q_gen_7882 () -> q_gen_7882 (q_gen_7892) -> q_gen_7889 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 17 () -> length([nil, z]) -> 17 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 17 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 24 (le([s(nn1), z])) -> BOT -> 20 (le([z, z])) -> BOT -> 18 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 22 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 22 } Sat witness: Found: ((le([s(nn1), s(nn2)])) -> le([nn1, nn2]), { nn1 -> s(s(z)) ; nn2 -> s(z) }) ------------------------------------------- Step 22, which took 0.022738 s (model generation: 0.020865, model checking: 0.001873): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7900) -> q_gen_7882 () -> q_gen_7882 (q_gen_7892) -> q_gen_7889 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 18 () -> length([nil, z]) -> 18 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 18 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 24 (le([s(nn1), z])) -> BOT -> 21 (le([z, z])) -> BOT -> 19 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 22 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 25 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> s(s(s(z))) ; ll -> cons(z, cons(z, cons(z, nil))) ; x -> z }) ------------------------------------------- Step 23, which took 0.023820 s (model generation: 0.022220, model checking: 0.001600): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7892) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7889, q_gen_7900) -> q_gen_7900 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 19 () -> length([nil, z]) -> 19 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 19 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 24 (le([s(nn1), z])) -> BOT -> 22 (le([z, z])) -> BOT -> 20 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 25 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 25 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(s(z))) ; _zca -> s(s(s(z))) ; l -> cons(z, cons(z, nil)) ; x -> z }) ------------------------------------------- Step 24, which took 0.027859 s (model generation: 0.024684, model checking: 0.003175): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7892) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7889, q_gen_7900) -> q_gen_7900 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 20 () -> length([nil, z]) -> 20 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 20 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 25 (le([s(nn1), z])) -> BOT -> 23 (le([z, z])) -> BOT -> 21 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 25 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 28 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> s(z) ; ll -> cons(s(s(z)), nil) ; x -> z }) ------------------------------------------- Step 25, which took 0.027851 s (model generation: 0.025945, model checking: 0.001906): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7892) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7889, q_gen_7900) -> q_gen_7900 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 21 () -> length([nil, z]) -> 21 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 21 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 25 (le([s(nn1), z])) -> BOT -> 24 (le([z, z])) -> BOT -> 22 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 28 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 28 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(s(z))) ; _zca -> s(s(s(z))) ; l -> cons(z, cons(z, cons(z, nil))) ; x -> z }) ------------------------------------------- Step 26, which took 0.032555 s (model generation: 0.028305, model checking: 0.004250): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7900) -> q_gen_7882 () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 22 () -> length([nil, z]) -> 22 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 22 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 26 (le([s(nn1), z])) -> BOT -> 25 (le([z, z])) -> BOT -> 23 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 28 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 31 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> z ; ll -> nil ; x -> s(s(s(s(z)))) }) ------------------------------------------- Step 27, which took 0.033240 s (model generation: 0.031100, model checking: 0.002140): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7900) -> q_gen_7882 () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7907) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 23 () -> length([nil, z]) -> 23 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 23 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 27 (le([s(nn1), z])) -> BOT -> 26 (le([z, z])) -> BOT -> 24 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 31 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 31 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(s(s(z)))) ; _zca -> s(s(z)) ; l -> cons(z, nil) ; x -> z }) ------------------------------------------- Step 28, which took 0.035750 s (model generation: 0.035180, model checking: 0.000570): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7886, q_gen_7897}, Q_f={q_gen_7879}, Delta= { () -> q_gen_7880 (q_gen_7880) -> q_gen_7886 (q_gen_7879) -> q_gen_7879 (q_gen_7886) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7886) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7900) -> q_gen_7882 () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7907) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 26 () -> length([nil, z]) -> 24 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 24 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 27 (le([s(nn1), z])) -> BOT -> 26 (le([z, z])) -> BOT -> 24 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 31 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 31 } Sat witness: Found: (() -> le([z, s(nn2)]), { nn2 -> s(s(z)) }) ------------------------------------------- Step 29, which took 0.037545 s (model generation: 0.037149, model checking: 0.000396): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7886, q_gen_7897}, Q_f={q_gen_7879}, Delta= { () -> q_gen_7880 (q_gen_7880) -> q_gen_7886 (q_gen_7886) -> q_gen_7886 (q_gen_7879) -> q_gen_7879 (q_gen_7886) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7886) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7900) -> q_gen_7882 () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7907) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 26 () -> length([nil, z]) -> 25 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 25 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 27 (le([s(nn1), z])) -> BOT -> 29 (le([z, z])) -> BOT -> 25 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 31 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 31 } Sat witness: Found: ((le([s(nn1), z])) -> BOT, { nn1 -> s(z) }) ------------------------------------------- Step 30, which took 0.037363 s (model generation: 0.036819, model checking: 0.000544): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897, q_gen_7898, q_gen_7903}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7903) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7898) -> q_gen_7897 (q_gen_7880) -> q_gen_7898 () -> q_gen_7898 (q_gen_7897) -> q_gen_7903 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7892) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7889, q_gen_7900) -> q_gen_7900 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 27 () -> length([nil, z]) -> 26 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 26 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 30 (le([s(nn1), z])) -> BOT -> 29 (le([z, z])) -> BOT -> 26 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 31 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 31 } Sat witness: Found: ((le([s(nn1), s(nn2)])) -> le([nn1, nn2]), { nn1 -> s(s(z)) ; nn2 -> s(s(z)) }) ------------------------------------------- Step 31, which took 0.045359 s (model generation: 0.036650, model checking: 0.008709): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7907) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 28 () -> length([nil, z]) -> 27 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 27 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 31 (le([s(nn1), z])) -> BOT -> 30 (le([z, z])) -> BOT -> 27 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 31 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 34 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> s(z) ; ll -> cons(s(s(s(z))), nil) ; x -> z }) ------------------------------------------- Step 32, which took 0.042097 s (model generation: 0.038975, model checking: 0.003122): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7907) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 29 () -> length([nil, z]) -> 28 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 28 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 31 (le([s(nn1), z])) -> BOT -> 31 (le([z, z])) -> BOT -> 28 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 34 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 34 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(s(s(s(z))))) ; _zca -> s(s(s(s(z)))) ; l -> cons(z, cons(z, cons(s(s(z)), nil))) ; x -> z }) ------------------------------------------- Step 33, which took 0.050806 s (model generation: 0.050037, model checking: 0.000769): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7886, q_gen_7897, q_gen_7928}, Q_f={q_gen_7879}, Delta= { () -> q_gen_7880 (q_gen_7880) -> q_gen_7886 (q_gen_7886) -> q_gen_7886 (q_gen_7879) -> q_gen_7879 (q_gen_7928) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7886) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 (q_gen_7886) -> q_gen_7928 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7900) -> q_gen_7882 () -> q_gen_7882 (q_gen_7907) -> q_gen_7889 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 30 () -> length([nil, z]) -> 29 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 29 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 34 (le([s(nn1), z])) -> BOT -> 32 (le([z, z])) -> BOT -> 29 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 34 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 34 } Sat witness: Found: ((le([s(nn1), s(nn2)])) -> le([nn1, nn2]), { nn1 -> s(s(z)) ; nn2 -> z }) ------------------------------------------- Step 34, which took 0.066770 s (model generation: 0.051543, model checking: 0.015227): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 (q_gen_7907) -> q_gen_7889 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 31 () -> length([nil, z]) -> 30 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 30 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 34 (le([s(nn1), z])) -> BOT -> 33 (le([z, z])) -> BOT -> 30 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 34 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 37 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> s(z) ; ll -> cons(s(z), nil) ; x -> s(z) }) ------------------------------------------- Step 35, which took 0.056346 s (model generation: 0.054222, model checking: 0.002124): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 (q_gen_7907) -> q_gen_7889 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7892, q_gen_7882) -> q_gen_7909 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7883, q_gen_7909) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7883) -> q_gen_7883 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 32 () -> length([nil, z]) -> 31 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 31 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 34 (le([s(nn1), z])) -> BOT -> 34 (le([z, z])) -> BOT -> 31 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 37 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 37 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(z) ; _zca -> s(z) ; l -> cons(s(z), nil) ; x -> z }) ------------------------------------------- Step 36, which took 0.077180 s (model generation: 0.073100, model checking: 0.004080): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 (q_gen_7907) -> q_gen_7889 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7892, q_gen_7882) -> q_gen_7909 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7909) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7883) -> q_gen_7915 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 33 () -> length([nil, z]) -> 32 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 32 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 35 (le([s(nn1), z])) -> BOT -> 35 (le([z, z])) -> BOT -> 32 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 37 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 40 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> s(z) ; ll -> cons(s(z), nil) ; x -> z }) ------------------------------------------- Step 37, which took 0.062876 s (model generation: 0.058431, model checking: 0.004445): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 (q_gen_7907) -> q_gen_7889 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 34 () -> length([nil, z]) -> 33 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 33 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 36 (le([s(nn1), z])) -> BOT -> 36 (le([z, z])) -> BOT -> 33 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 40 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 40 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(s(s(s(z))))) ; _zca -> s(s(s(z))) ; l -> cons(z, cons(s(s(z)), nil)) ; x -> z }) ------------------------------------------- Step 38, which took 0.080430 s (model generation: 0.066807, model checking: 0.013623): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7907) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 35 () -> length([nil, z]) -> 34 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 34 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 37 (le([s(nn1), z])) -> BOT -> 37 (le([z, z])) -> BOT -> 34 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 40 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 43 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> s(s(s(z))) ; ll -> cons(z, cons(z, cons(s(z), nil))) ; x -> s(z) }) ------------------------------------------- Step 39, which took 0.085160 s (model generation: 0.081130, model checking: 0.004030): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7907) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7883, q_gen_7909) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7901) -> q_gen_7883 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 36 () -> length([nil, z]) -> 35 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 35 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 38 (le([s(nn1), z])) -> BOT -> 38 (le([z, z])) -> BOT -> 35 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 43 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 43 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(s(s(z)))) ; _zca -> s(s(z)) ; l -> cons(s(z), nil) ; x -> s(z) }) ------------------------------------------- Step 40, which took 0.091211 s (model generation: 0.081110, model checking: 0.010101): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7907) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7901) -> q_gen_7915 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 37 () -> length([nil, z]) -> 36 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 36 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 39 (le([s(nn1), z])) -> BOT -> 39 (le([z, z])) -> BOT -> 36 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 43 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 46 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> s(s(s(s(z)))) ; ll -> cons(z, cons(z, cons(z, cons(s(z), nil)))) ; x -> z }) ------------------------------------------- Step 41, which took 0.104852 s (model generation: 0.098756, model checking: 0.006096): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7907) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7889, q_gen_7909) -> q_gen_7909 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7901) -> q_gen_7915 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 38 () -> length([nil, z]) -> 37 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 37 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 40 (le([s(nn1), z])) -> BOT -> 40 (le([z, z])) -> BOT -> 37 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 46 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 46 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(s(s(z)))) ; _zca -> s(s(s(s(z)))) ; l -> cons(z, cons(z, cons(z, cons(z, cons(s(s(z)), nil))))) ; x -> s(z) }) ------------------------------------------- Step 42, which took 0.120465 s (model generation: 0.110785, model checking: 0.009680): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7920}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7920) -> q_gen_7882 () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7907) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7889, q_gen_7909) -> q_gen_7920 (q_gen_7907, q_gen_7882) -> q_gen_7920 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7895, q_gen_7920) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 (q_gen_7915, q_gen_7920) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7901) -> q_gen_7915 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 39 () -> length([nil, z]) -> 38 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 38 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 41 (le([s(nn1), z])) -> BOT -> 41 (le([z, z])) -> BOT -> 38 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 46 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 49 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> s(s(s(s(z)))) ; ll -> cons(z, cons(s(s(z)), nil)) ; x -> z }) ------------------------------------------- Step 43, which took 0.143140 s (model generation: 0.135736, model checking: 0.007404): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7941}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7909) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7907) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7889, q_gen_7941) -> q_gen_7909 (q_gen_7892, q_gen_7882) -> q_gen_7941 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7895, q_gen_7941) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 (q_gen_7915, q_gen_7941) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7901) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7941) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7883) -> q_gen_7915 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 40 () -> length([nil, z]) -> 39 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 39 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 42 (le([s(nn1), z])) -> BOT -> 42 (le([z, z])) -> BOT -> 39 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 49 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 49 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(z)) ; _zca -> s(s(z)) ; l -> cons(z, cons(s(z), nil)) ; x -> s(z) }) ------------------------------------------- Step 44, which took 0.115732 s (model generation: 0.115118, model checking: 0.000614): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7886, q_gen_7897, q_gen_7927, q_gen_7928}, Q_f={q_gen_7879}, Delta= { () -> q_gen_7880 (q_gen_7880) -> q_gen_7886 (q_gen_7886) -> q_gen_7886 (q_gen_7879) -> q_gen_7879 (q_gen_7927) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7886) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 (q_gen_7928) -> q_gen_7927 (q_gen_7886) -> q_gen_7928 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7900) -> q_gen_7882 () -> q_gen_7882 (q_gen_7907) -> q_gen_7889 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7883, q_gen_7900) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 () -> q_gen_7878 (q_gen_7901) -> q_gen_7883 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 41 () -> length([nil, z]) -> 40 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 40 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 45 (le([s(nn1), z])) -> BOT -> 43 (le([z, z])) -> BOT -> 40 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 49 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 49 } Sat witness: Found: ((le([s(nn1), s(nn2)])) -> le([nn1, nn2]), { nn1 -> s(s(s(z))) ; nn2 -> s(z) }) ------------------------------------------- Step 45, which took 0.131339 s (model generation: 0.124510, model checking: 0.006829): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7920}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7920) -> q_gen_7882 () -> q_gen_7882 (q_gen_7907) -> q_gen_7889 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7892, q_gen_7882) -> q_gen_7920 (q_gen_7907, q_gen_7882) -> q_gen_7920 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7895, q_gen_7920) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7901) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7920) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7920) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 42 () -> length([nil, z]) -> 41 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 41 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 46 (le([s(nn1), z])) -> BOT -> 44 (le([z, z])) -> BOT -> 41 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 49 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 52 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> s(s(z)) ; ll -> cons(z, cons(s(z), nil)) ; x -> z }) ------------------------------------------- Step 46, which took 0.125316 s (model generation: 0.122893, model checking: 0.002423): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7920}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7920) -> q_gen_7882 () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7907) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7889, q_gen_7909) -> q_gen_7909 (q_gen_7907, q_gen_7882) -> q_gen_7920 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7895, q_gen_7920) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7915, q_gen_7920) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7901) -> q_gen_7915 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 43 () -> length([nil, z]) -> 42 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 42 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 47 (le([s(nn1), z])) -> BOT -> 45 (le([z, z])) -> BOT -> 42 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 52 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 52 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(z)) ; _zca -> s(z) ; l -> cons(z, cons(s(s(z)), nil)) ; x -> s(z) }) ------------------------------------------- Step 47, which took 0.147647 s (model generation: 0.132721, model checking: 0.014926): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7956}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7956) -> q_gen_7882 () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7907) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7889, q_gen_7909) -> q_gen_7956 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 (q_gen_7915, q_gen_7956) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7901) -> q_gen_7915 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 44 () -> length([nil, z]) -> 43 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 43 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 48 (le([s(nn1), z])) -> BOT -> 46 (le([z, z])) -> BOT -> 43 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 52 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 55 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> s(s(s(s(z)))) ; ll -> cons(z, cons(z, cons(z, cons(z, cons(z, nil))))) ; x -> z }) ------------------------------------------- Step 48, which took 0.163534 s (model generation: 0.158114, model checking: 0.005420): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7920}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 (q_gen_7907) -> q_gen_7889 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7889, q_gen_7909) -> q_gen_7920 (q_gen_7889, q_gen_7920) -> q_gen_7920 (q_gen_7907, q_gen_7882) -> q_gen_7920 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7895, q_gen_7920) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7894) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7920) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7920) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7920) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7901) -> q_gen_7915 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 45 () -> length([nil, z]) -> 44 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 44 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 49 (le([s(nn1), z])) -> BOT -> 47 (le([z, z])) -> BOT -> 44 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 55 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 55 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(s(s(s(z))))) ; _zca -> s(s(s(z))) ; l -> cons(z, cons(s(z), nil)) ; x -> z }) ------------------------------------------- Step 49, which took 0.186084 s (model generation: 0.181229, model checking: 0.004855): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7920}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7907) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7920) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7889, q_gen_7909) -> q_gen_7920 (q_gen_7907, q_gen_7882) -> q_gen_7920 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7895, q_gen_7920) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7901, q_gen_7920) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7915, q_gen_7920) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7901) -> q_gen_7915 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 46 () -> length([nil, z]) -> 45 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 45 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 50 (le([s(nn1), z])) -> BOT -> 48 (le([z, z])) -> BOT -> 45 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 55 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 58 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> s(s(s(z))) ; ll -> cons(z, cons(s(s(z)), nil)) ; x -> z }) ------------------------------------------- Step 50, which took 0.179850 s (model generation: 0.173448, model checking: 0.006402): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7920}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7889, q_gen_7909) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7907) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7889, q_gen_7920) -> q_gen_7920 (q_gen_7907, q_gen_7882) -> q_gen_7920 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7895, q_gen_7920) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7920) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7920) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7920) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7901) -> q_gen_7915 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 47 () -> length([nil, z]) -> 46 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 46 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 51 (le([s(nn1), z])) -> BOT -> 49 (le([z, z])) -> BOT -> 46 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 58 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 58 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(z)) ; _zca -> s(s(z)) ; l -> cons(z, cons(s(s(z)), nil)) ; x -> z }) ------------------------------------------- Step 51, which took 0.180848 s (model generation: 0.176141, model checking: 0.004707): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7920}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7907) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7889, q_gen_7920) -> q_gen_7909 (q_gen_7889, q_gen_7909) -> q_gen_7920 (q_gen_7907, q_gen_7882) -> q_gen_7920 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7895, q_gen_7920) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7901, q_gen_7920) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7909) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7920) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7901) -> q_gen_7915 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 48 () -> length([nil, z]) -> 47 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 47 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 52 (le([s(nn1), z])) -> BOT -> 50 (le([z, z])) -> BOT -> 47 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 58 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 61 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> s(s(z)) ; ll -> cons(z, cons(s(s(z)), nil)) ; x -> z }) ------------------------------------------- Step 52, which took 0.189739 s (model generation: 0.184628, model checking: 0.005111): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7924}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7909) -> q_gen_7882 () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7924, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7907) -> q_gen_7924 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 (q_gen_7924) -> q_gen_7883 (q_gen_7924) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7901) -> q_gen_7915 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 49 () -> length([nil, z]) -> 48 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 48 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 53 (le([s(nn1), z])) -> BOT -> 51 (le([z, z])) -> BOT -> 48 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 61 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 61 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(s(s(s(z))))) ; _zca -> s(s(z)) ; l -> cons(z, nil) ; x -> s(z) }) ------------------------------------------- Step 53, which took 0.231882 s (model generation: 0.209513, model checking: 0.022369): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7920, q_gen_7934}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7909) -> q_gen_7882 () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7889, q_gen_7934) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7907) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7892, q_gen_7882) -> q_gen_7920 (q_gen_7907, q_gen_7882) -> q_gen_7920 (q_gen_7889, q_gen_7920) -> q_gen_7934 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7895, q_gen_7920) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7901, q_gen_7934) -> q_gen_7878 (q_gen_7915, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7920) -> q_gen_7896 (q_gen_7883, q_gen_7934) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7895, q_gen_7934) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7920) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7920) -> q_gen_7896 (q_gen_7915, q_gen_7934) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7901) -> q_gen_7915 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 50 () -> length([nil, z]) -> 49 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 49 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 54 (le([s(nn1), z])) -> BOT -> 52 (le([z, z])) -> BOT -> 49 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 61 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 64 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> s(s(s(s(z)))) ; ll -> cons(z, cons(z, cons(z, cons(z, nil)))) ; x -> z }) ------------------------------------------- Step 54, which took 0.240590 s (model generation: 0.229256, model checking: 0.011334): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7920, q_gen_7934}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7907) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7934) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7889, q_gen_7909) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7892, q_gen_7882) -> q_gen_7920 (q_gen_7907, q_gen_7882) -> q_gen_7920 (q_gen_7889, q_gen_7920) -> q_gen_7934 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7895, q_gen_7920) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7901, q_gen_7934) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7901) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7920) -> q_gen_7896 (q_gen_7883, q_gen_7934) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7895, q_gen_7934) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7920) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7915, q_gen_7920) -> q_gen_7896 (q_gen_7915, q_gen_7934) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 51 () -> length([nil, z]) -> 50 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 50 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 55 (le([s(nn1), z])) -> BOT -> 53 (le([z, z])) -> BOT -> 50 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 64 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 64 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(s(z))) ; _zca -> s(s(z)) ; l -> cons(z, cons(z, cons(s(s(z)), nil))) ; x -> z }) ------------------------------------------- Step 55, which took 0.231485 s (model generation: 0.225741, model checking: 0.005744): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7920, q_gen_7934}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7889, q_gen_7934) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7907) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7889, q_gen_7909) -> q_gen_7909 (q_gen_7892, q_gen_7882) -> q_gen_7920 (q_gen_7907, q_gen_7882) -> q_gen_7920 (q_gen_7889, q_gen_7920) -> q_gen_7934 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7895, q_gen_7920) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7901, q_gen_7934) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7920) -> q_gen_7896 (q_gen_7883, q_gen_7934) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7895, q_gen_7934) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7920) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7915, q_gen_7920) -> q_gen_7896 (q_gen_7915, q_gen_7934) -> q_gen_7896 (q_gen_7901) -> q_gen_7901 (q_gen_7892) -> q_gen_7901 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 52 () -> length([nil, z]) -> 51 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 51 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 56 (le([s(nn1), z])) -> BOT -> 54 (le([z, z])) -> BOT -> 51 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 64 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 67 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> s(s(s(z))) ; ll -> cons(z, cons(z, cons(s(s(z)), nil))) ; x -> z }) ------------------------------------------- Step 56, which took 0.230615 s (model generation: 0.223204, model checking: 0.007411): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7920, q_gen_7934}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7889, q_gen_7934) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7907) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7889, q_gen_7909) -> q_gen_7909 (q_gen_7892, q_gen_7882) -> q_gen_7920 (q_gen_7907, q_gen_7882) -> q_gen_7920 (q_gen_7889, q_gen_7920) -> q_gen_7934 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7895, q_gen_7920) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7901, q_gen_7934) -> q_gen_7878 (q_gen_7915, q_gen_7894) -> q_gen_7878 (q_gen_7915, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7920) -> q_gen_7896 (q_gen_7883, q_gen_7934) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7895, q_gen_7934) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7920) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7920) -> q_gen_7896 (q_gen_7915, q_gen_7934) -> q_gen_7896 (q_gen_7901) -> q_gen_7901 (q_gen_7892) -> q_gen_7901 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 53 () -> length([nil, z]) -> 52 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 52 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 57 (le([s(nn1), z])) -> BOT -> 55 (le([z, z])) -> BOT -> 52 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 67 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 67 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(s(s(s(z))))) ; _zca -> s(s(s(z))) ; l -> cons(z, cons(z, nil)) ; x -> z }) ------------------------------------------- Step 57, which took 0.280528 s (model generation: 0.266827, model checking: 0.013701): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7920, q_gen_7934}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7889, q_gen_7934) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7907) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7889, q_gen_7909) -> q_gen_7909 (q_gen_7892, q_gen_7882) -> q_gen_7920 (q_gen_7907, q_gen_7882) -> q_gen_7920 (q_gen_7889, q_gen_7920) -> q_gen_7934 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7895, q_gen_7920) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7901, q_gen_7934) -> q_gen_7878 (q_gen_7915, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7920) -> q_gen_7896 (q_gen_7883, q_gen_7934) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7895, q_gen_7934) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7920) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7920) -> q_gen_7896 (q_gen_7915, q_gen_7934) -> q_gen_7896 (q_gen_7901) -> q_gen_7901 (q_gen_7892) -> q_gen_7901 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 54 () -> length([nil, z]) -> 53 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 53 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 58 (le([s(nn1), z])) -> BOT -> 56 (le([z, z])) -> BOT -> 53 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 67 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 70 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> s(s(s(z))) ; ll -> cons(z, cons(z, cons(z, nil))) ; x -> s(z) }) ------------------------------------------- Step 58, which took 0.260706 s (model generation: 0.256270, model checking: 0.004436): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7924, q_gen_7932}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7909) -> q_gen_7882 () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7889, q_gen_7932) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7907) -> q_gen_7924 (q_gen_7892, q_gen_7882) -> q_gen_7932 (q_gen_7924, q_gen_7882) -> q_gen_7932 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7895, q_gen_7932) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 (q_gen_7915, q_gen_7932) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 (q_gen_7924) -> q_gen_7883 (q_gen_7924) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7900) -> q_gen_7896 (q_gen_7883, q_gen_7932) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7883) -> q_gen_7915 (q_gen_7901) -> q_gen_7915 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 55 () -> length([nil, z]) -> 54 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 54 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 59 (le([s(nn1), z])) -> BOT -> 57 (le([z, z])) -> BOT -> 54 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 70 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 70 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(s(s(s(z))))) ; _zca -> s(s(z)) ; l -> cons(z, nil) ; x -> z }) ------------------------------------------- Step 59, which took 0.284847 s (model generation: 0.263012, model checking: 0.021835): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7952, q_gen_7956}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7907) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7889, q_gen_7909) -> q_gen_7956 (q_gen_7889, q_gen_7956) -> q_gen_7956 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 (q_gen_7915, q_gen_7956) -> q_gen_7878 (q_gen_7952, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7952, q_gen_7882) -> q_gen_7896 (q_gen_7952, q_gen_7956) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7907) -> q_gen_7915 (q_gen_7901) -> q_gen_7952 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 56 () -> length([nil, z]) -> 55 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 55 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 60 (le([s(nn1), z])) -> BOT -> 58 (le([z, z])) -> BOT -> 55 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 70 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 73 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> s(s(s(s(z)))) ; ll -> cons(s(z), cons(z, cons(z, cons(s(z), nil)))) ; x -> z }) ------------------------------------------- Step 60, which took 0.294498 s (model generation: 0.284393, model checking: 0.010105): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7942, q_gen_7956}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7907) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7892, q_gen_7909) -> q_gen_7909 (q_gen_7889, q_gen_7909) -> q_gen_7956 (q_gen_7889, q_gen_7956) -> q_gen_7956 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 (q_gen_7915, q_gen_7956) -> q_gen_7878 (q_gen_7942, q_gen_7894) -> q_gen_7878 (q_gen_7942, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7942, q_gen_7882) -> q_gen_7896 (q_gen_7942, q_gen_7900) -> q_gen_7896 (q_gen_7942, q_gen_7956) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7907) -> q_gen_7915 (q_gen_7883) -> q_gen_7942 (q_gen_7901) -> q_gen_7942 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 57 () -> length([nil, z]) -> 56 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 56 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 61 (le([s(nn1), z])) -> BOT -> 59 (le([z, z])) -> BOT -> 56 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 73 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 73 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(s(z))) ; _zca -> s(s(z)) ; l -> cons(z, cons(z, cons(z, nil))) ; x -> s(z) }) ------------------------------------------- Step 61, which took 0.414092 s (model generation: 0.390102, model checking: 0.023990): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7952, q_gen_7956}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7907) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7892, q_gen_7909) -> q_gen_7909 (q_gen_7889, q_gen_7909) -> q_gen_7956 (q_gen_7889, q_gen_7956) -> q_gen_7956 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 (q_gen_7915, q_gen_7956) -> q_gen_7878 (q_gen_7952, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7952, q_gen_7882) -> q_gen_7896 (q_gen_7952, q_gen_7956) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7907) -> q_gen_7915 (q_gen_7901) -> q_gen_7952 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 58 () -> length([nil, z]) -> 57 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 57 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 62 (le([s(nn1), z])) -> BOT -> 60 (le([z, z])) -> BOT -> 57 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 73 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 76 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> s(s(z)) ; ll -> cons(s(z), cons(z, nil)) ; x -> z }) ------------------------------------------- Step 62, which took 0.393326 s (model generation: 0.384493, model checking: 0.008833): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7952, q_gen_7956}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7907) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7889, q_gen_7909) -> q_gen_7956 (q_gen_7889, q_gen_7956) -> q_gen_7956 (q_gen_7892, q_gen_7909) -> q_gen_7956 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 (q_gen_7915, q_gen_7956) -> q_gen_7878 (q_gen_7952, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7952, q_gen_7882) -> q_gen_7896 (q_gen_7952, q_gen_7956) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7907) -> q_gen_7915 (q_gen_7901) -> q_gen_7952 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 59 () -> length([nil, z]) -> 58 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 58 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 63 (le([s(nn1), z])) -> BOT -> 61 (le([z, z])) -> BOT -> 58 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 76 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 76 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(s(s(z)))) ; _zca -> s(s(s(s(z)))) ; l -> cons(z, cons(z, cons(z, cons(z, nil)))) ; x -> z }) ------------------------------------------- Step 63, which took 0.365100 s (model generation: 0.364240, model checking: 0.000860): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897, q_gen_7910, q_gen_7911, q_gen_7912}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7910) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 () -> q_gen_7897 (q_gen_7911) -> q_gen_7910 (q_gen_7912) -> q_gen_7911 (q_gen_7880) -> q_gen_7912 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 (q_gen_7907) -> q_gen_7889 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7909) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7909) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7901) -> q_gen_7915 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 60 () -> length([nil, z]) -> 59 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 59 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 66 (le([s(nn1), z])) -> BOT -> 62 (le([z, z])) -> BOT -> 59 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 76 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 76 } Sat witness: Found: ((le([s(nn1), s(nn2)])) -> le([nn1, nn2]), { nn1 -> s(s(s(z))) ; nn2 -> s(s(z)) }) ------------------------------------------- Step 64, which took 0.302399 s (model generation: 0.301365, model checking: 0.001034): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897, q_gen_7898, q_gen_7903, q_gen_7918}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7918) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7898) -> q_gen_7897 (q_gen_7880) -> q_gen_7898 () -> q_gen_7898 (q_gen_7897) -> q_gen_7903 (q_gen_7903) -> q_gen_7918 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7907) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7889, q_gen_7909) -> q_gen_7900 (q_gen_7892, q_gen_7894) -> q_gen_7900 (q_gen_7892, q_gen_7909) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7901) -> q_gen_7915 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 61 () -> length([nil, z]) -> 60 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 60 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 69 (le([s(nn1), z])) -> BOT -> 63 (le([z, z])) -> BOT -> 60 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 76 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 76 } Sat witness: Found: ((le([s(nn1), s(nn2)])) -> le([nn1, nn2]), { nn1 -> s(s(s(z))) ; nn2 -> s(s(s(z))) }) ------------------------------------------- Step 65, which took 0.319302 s (model generation: 0.318534, model checking: 0.000768): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7886, q_gen_7897, q_gen_7930}, Q_f={q_gen_7879}, Delta= { () -> q_gen_7880 (q_gen_7880) -> q_gen_7886 (q_gen_7886) -> q_gen_7930 (q_gen_7879) -> q_gen_7879 (q_gen_7930) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7886) -> q_gen_7879 (q_gen_7930) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 (q_gen_7886) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7924}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7909) -> q_gen_7882 (q_gen_7892, q_gen_7909) -> q_gen_7882 () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7924, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7907) -> q_gen_7924 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 (q_gen_7924) -> q_gen_7883 (q_gen_7924) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7901) -> q_gen_7915 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 64 () -> length([nil, z]) -> 61 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 61 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 69 (le([s(nn1), z])) -> BOT -> 63 (le([z, z])) -> BOT -> 61 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 76 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 76 } Sat witness: Found: (() -> le([z, s(nn2)]), { nn2 -> s(s(s(z))) }) ------------------------------------------- Step 66, which took 0.597102 s (model generation: 0.568693, model checking: 0.028409): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7924, q_gen_7935, q_gen_7956}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7956) -> q_gen_7882 () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7924, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7892, q_gen_7909) -> q_gen_7909 (q_gen_7907) -> q_gen_7924 (q_gen_7889, q_gen_7909) -> q_gen_7956 (q_gen_7892, q_gen_7894) -> q_gen_7956 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7901, q_gen_7956) -> q_gen_7878 (q_gen_7915, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 (q_gen_7935, q_gen_7909) -> q_gen_7878 (q_gen_7935, q_gen_7956) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 (q_gen_7924) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7956) -> q_gen_7896 (q_gen_7935, q_gen_7882) -> q_gen_7896 (q_gen_7935, q_gen_7894) -> q_gen_7896 (q_gen_7935, q_gen_7900) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7901) -> q_gen_7915 (q_gen_7907) -> q_gen_7915 (q_gen_7924) -> q_gen_7935 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 65 () -> length([nil, z]) -> 62 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 62 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 70 (le([s(nn1), z])) -> BOT -> 64 (le([z, z])) -> BOT -> 62 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 76 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 79 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> s(s(s(z))) ; ll -> cons(z, cons(z, cons(s(z), cons(z, cons(z, cons(z, nil)))))) ; x -> s(z) }) ------------------------------------------- Step 67, which took 0.546874 s (model generation: 0.546105, model checking: 0.000769): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7886, q_gen_7897, q_gen_7930}, Q_f={q_gen_7879}, Delta= { (q_gen_7930) -> q_gen_7880 () -> q_gen_7880 (q_gen_7880) -> q_gen_7886 (q_gen_7886) -> q_gen_7930 (q_gen_7879) -> q_gen_7879 (q_gen_7930) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7886) -> q_gen_7879 (q_gen_7930) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 (q_gen_7886) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7924}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7909) -> q_gen_7882 (q_gen_7892, q_gen_7909) -> q_gen_7882 () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7924, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7907) -> q_gen_7924 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 (q_gen_7924) -> q_gen_7883 (q_gen_7924) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7901) -> q_gen_7915 (q_gen_7907) -> q_gen_7915 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 65 () -> length([nil, z]) -> 63 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 63 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 70 (le([s(nn1), z])) -> BOT -> 67 (le([z, z])) -> BOT -> 63 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 76 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 79 } Sat witness: Found: ((le([s(nn1), z])) -> BOT, { nn1 -> s(s(z)) }) ------------------------------------------- Step 68, which took 5.688467 s (model generation: 5.563644, model checking: 0.124823): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7924, q_gen_7935, q_gen_7956}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7956) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7924, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7907) -> q_gen_7924 (q_gen_7889, q_gen_7909) -> q_gen_7956 (q_gen_7892, q_gen_7894) -> q_gen_7956 (q_gen_7892, q_gen_7909) -> q_gen_7956 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7901, q_gen_7956) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 (q_gen_7935, q_gen_7956) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 (q_gen_7924) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7915, q_gen_7956) -> q_gen_7896 (q_gen_7935, q_gen_7882) -> q_gen_7896 (q_gen_7935, q_gen_7894) -> q_gen_7896 (q_gen_7935, q_gen_7900) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7901) -> q_gen_7915 (q_gen_7907) -> q_gen_7915 (q_gen_7924) -> q_gen_7935 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 66 () -> length([nil, z]) -> 64 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 64 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 71 (le([s(nn1), z])) -> BOT -> 68 (le([z, z])) -> BOT -> 64 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 79 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 79 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(s(z))) ; _zca -> s(s(z)) ; l -> cons(z, cons(s(z), cons(s(z), nil))) ; x -> s(z) }) ------------------------------------------- Step 69, which took 5.837011 s (model generation: 5.401484, model checking: 0.435527): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7924, q_gen_7935, q_gen_7956}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7924, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7889, q_gen_7956) -> q_gen_7900 (q_gen_7892, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7907) -> q_gen_7924 (q_gen_7889, q_gen_7909) -> q_gen_7956 (q_gen_7892, q_gen_7909) -> q_gen_7956 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 (q_gen_7935, q_gen_7909) -> q_gen_7878 (q_gen_7935, q_gen_7956) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 (q_gen_7924) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7956) -> q_gen_7896 (q_gen_7935, q_gen_7882) -> q_gen_7896 (q_gen_7935, q_gen_7894) -> q_gen_7896 (q_gen_7935, q_gen_7900) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7907) -> q_gen_7915 (q_gen_7901) -> q_gen_7935 (q_gen_7924) -> q_gen_7935 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 67 () -> length([nil, z]) -> 65 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 65 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 72 (le([s(nn1), z])) -> BOT -> 69 (le([z, z])) -> BOT -> 65 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 79 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 82 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> z ; ll -> nil ; x -> s(s(s(s(s(z))))) }) ------------------------------------------- Step 70, which took 5.298160 s (model generation: 5.132775, model checking: 0.165385): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7924, q_gen_7935, q_gen_7956}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7924) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7924, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7889, q_gen_7956) -> q_gen_7900 (q_gen_7892, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7907) -> q_gen_7924 (q_gen_7889, q_gen_7909) -> q_gen_7956 (q_gen_7892, q_gen_7909) -> q_gen_7956 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 (q_gen_7935, q_gen_7909) -> q_gen_7878 (q_gen_7935, q_gen_7956) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 (q_gen_7924) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7915, q_gen_7956) -> q_gen_7896 (q_gen_7935, q_gen_7882) -> q_gen_7896 (q_gen_7935, q_gen_7894) -> q_gen_7896 (q_gen_7935, q_gen_7900) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7907) -> q_gen_7915 (q_gen_7901) -> q_gen_7935 (q_gen_7924) -> q_gen_7935 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 68 () -> length([nil, z]) -> 66 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 66 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 73 (le([s(nn1), z])) -> BOT -> 70 (le([z, z])) -> BOT -> 66 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 82 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 82 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(s(s(s(s(z)))))) ; _zca -> s(s(s(s(z)))) ; l -> cons(z, cons(z, cons(s(s(z)), nil))) ; x -> z }) ------------------------------------------- Step 71, which took 6.340577 s (model generation: 5.987525, model checking: 0.353052): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7924, q_gen_7935, q_gen_7956}, Q_f={q_gen_7878}, Delta= { (q_gen_7889, q_gen_7956) -> q_gen_7882 () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7924, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7892, q_gen_7909) -> q_gen_7909 (q_gen_7907) -> q_gen_7924 (q_gen_7924) -> q_gen_7924 (q_gen_7889, q_gen_7909) -> q_gen_7956 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 (q_gen_7935, q_gen_7909) -> q_gen_7878 (q_gen_7935, q_gen_7956) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 (q_gen_7924) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7956) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7915, q_gen_7956) -> q_gen_7896 (q_gen_7935, q_gen_7882) -> q_gen_7896 (q_gen_7935, q_gen_7894) -> q_gen_7896 (q_gen_7935, q_gen_7900) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7907) -> q_gen_7915 (q_gen_7901) -> q_gen_7935 (q_gen_7924) -> q_gen_7935 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 69 () -> length([nil, z]) -> 67 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 67 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 74 (le([s(nn1), z])) -> BOT -> 71 (le([z, z])) -> BOT -> 67 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 82 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 85 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> s(s(s(s(s(z))))) ; ll -> cons(z, cons(z, cons(z, cons(s(z), cons(s(s(s(z))), nil))))) ; x -> z }) ------------------------------------------- Step 72, which took 6.828110 s (model generation: 6.674133, model checking: 0.153977): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7924, q_gen_7935, q_gen_7956}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 (q_gen_7924) -> q_gen_7889 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7956) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7924, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7892, q_gen_7909) -> q_gen_7909 (q_gen_7907) -> q_gen_7924 (q_gen_7889, q_gen_7909) -> q_gen_7956 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 (q_gen_7935, q_gen_7909) -> q_gen_7878 (q_gen_7935, q_gen_7956) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 (q_gen_7924) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7956) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7956) -> q_gen_7896 (q_gen_7935, q_gen_7882) -> q_gen_7896 (q_gen_7935, q_gen_7894) -> q_gen_7896 (q_gen_7935, q_gen_7900) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7907) -> q_gen_7915 (q_gen_7901) -> q_gen_7935 (q_gen_7924) -> q_gen_7935 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 70 () -> length([nil, z]) -> 68 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 68 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 75 (le([s(nn1), z])) -> BOT -> 72 (le([z, z])) -> BOT -> 68 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 85 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 85 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(s(s(s(s(z)))))) ; _zca -> s(s(s(s(z)))) ; l -> cons(z, cons(s(s(z)), nil)) ; x -> z }) ------------------------------------------- Step 73, which took 7.533874 s (model generation: 6.827370, model checking: 0.706504): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7924, q_gen_7935, q_gen_7956}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7924, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7892, q_gen_7894) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7892, q_gen_7909) -> q_gen_7909 (q_gen_7907) -> q_gen_7924 (q_gen_7924) -> q_gen_7924 (q_gen_7889, q_gen_7909) -> q_gen_7956 (q_gen_7889, q_gen_7956) -> q_gen_7956 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7900) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 (q_gen_7935, q_gen_7909) -> q_gen_7878 (q_gen_7935, q_gen_7956) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 (q_gen_7924) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7901, q_gen_7956) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7956) -> q_gen_7896 (q_gen_7935, q_gen_7882) -> q_gen_7896 (q_gen_7935, q_gen_7894) -> q_gen_7896 (q_gen_7935, q_gen_7900) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7901) -> q_gen_7915 (q_gen_7907) -> q_gen_7915 (q_gen_7924) -> q_gen_7935 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 71 () -> length([nil, z]) -> 69 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 69 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 76 (le([s(nn1), z])) -> BOT -> 73 (le([z, z])) -> BOT -> 69 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 85 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 88 } Sat witness: Found: ((length([ll, _uca])) -> length([cons(x, ll), s(_uca)]), { _uca -> s(s(s(s(s(s(z)))))) ; ll -> cons(z, cons(z, cons(z, cons(z, cons(s(z), cons(z, nil)))))) ; x -> s(s(z)) }) ------------------------------------------- Step 74, which took 6.600398 s (model generation: 6.396814, model checking: 0.203584): Model: |_ { le -> {{{ Q={q_gen_7879, q_gen_7880, q_gen_7897}, Q_f={q_gen_7879}, Delta= { (q_gen_7880) -> q_gen_7880 () -> q_gen_7880 (q_gen_7879) -> q_gen_7879 (q_gen_7880) -> q_gen_7879 (q_gen_7897) -> q_gen_7897 (q_gen_7880) -> q_gen_7897 () -> q_gen_7897 } Datatype: Convolution form: left }}} ; length -> {{{ Q={q_gen_7878, q_gen_7882, q_gen_7883, q_gen_7889, q_gen_7892, q_gen_7894, q_gen_7895, q_gen_7896, q_gen_7900, q_gen_7901, q_gen_7907, q_gen_7909, q_gen_7915, q_gen_7924, q_gen_7935, q_gen_7956}, Q_f={q_gen_7878}, Delta= { () -> q_gen_7882 (q_gen_7924) -> q_gen_7889 () -> q_gen_7889 (q_gen_7889) -> q_gen_7892 (q_gen_7889, q_gen_7882) -> q_gen_7894 (q_gen_7892, q_gen_7882) -> q_gen_7894 (q_gen_7907, q_gen_7882) -> q_gen_7894 (q_gen_7924, q_gen_7882) -> q_gen_7894 (q_gen_7889, q_gen_7894) -> q_gen_7900 (q_gen_7889, q_gen_7956) -> q_gen_7900 (q_gen_7892) -> q_gen_7907 (q_gen_7889, q_gen_7900) -> q_gen_7909 (q_gen_7907) -> q_gen_7924 (q_gen_7889, q_gen_7909) -> q_gen_7956 (q_gen_7892, q_gen_7894) -> q_gen_7956 (q_gen_7892, q_gen_7909) -> q_gen_7956 (q_gen_7883, q_gen_7882) -> q_gen_7878 (q_gen_7895, q_gen_7894) -> q_gen_7878 (q_gen_7901, q_gen_7900) -> q_gen_7878 (q_gen_7901, q_gen_7956) -> q_gen_7878 (q_gen_7915, q_gen_7909) -> q_gen_7878 (q_gen_7935, q_gen_7956) -> q_gen_7878 () -> q_gen_7878 (q_gen_7889) -> q_gen_7883 (q_gen_7892) -> q_gen_7883 (q_gen_7907) -> q_gen_7883 (q_gen_7924) -> q_gen_7883 () -> q_gen_7883 (q_gen_7883) -> q_gen_7895 (q_gen_7895) -> q_gen_7895 (q_gen_7935) -> q_gen_7895 (q_gen_7889) -> q_gen_7895 (q_gen_7883, q_gen_7894) -> q_gen_7896 (q_gen_7883, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7882) -> q_gen_7896 (q_gen_7895, q_gen_7900) -> q_gen_7896 (q_gen_7895, q_gen_7909) -> q_gen_7896 (q_gen_7895, q_gen_7956) -> q_gen_7896 (q_gen_7901, q_gen_7882) -> q_gen_7896 (q_gen_7901, q_gen_7894) -> q_gen_7896 (q_gen_7901, q_gen_7909) -> q_gen_7896 (q_gen_7915, q_gen_7882) -> q_gen_7896 (q_gen_7915, q_gen_7894) -> q_gen_7896 (q_gen_7915, q_gen_7900) -> q_gen_7896 (q_gen_7915, q_gen_7956) -> q_gen_7896 (q_gen_7935, q_gen_7882) -> q_gen_7896 (q_gen_7935, q_gen_7894) -> q_gen_7896 (q_gen_7935, q_gen_7900) -> q_gen_7896 (q_gen_7935, q_gen_7909) -> q_gen_7896 (q_gen_7892) -> q_gen_7901 (q_gen_7901) -> q_gen_7915 (q_gen_7907) -> q_gen_7915 (q_gen_7924) -> q_gen_7935 } Datatype: Convolution form: left }}} } -- Equality automata are defined for: {eq_nat, eq_natlist} _| Teacher's answer: New clause system: { () -> le([z, s(nn2)]) -> 72 () -> length([nil, z]) -> 70 (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 70 (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 77 (le([s(nn1), z])) -> BOT -> 74 (le([z, z])) -> BOT -> 70 (length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]) -> 88 (length([ll, _uca])) -> length([cons(x, ll), s(_uca)]) -> 88 } Sat witness: Found: ((length([l, _yca]) /\ length([cons(x, l), _zca])) -> le([_yca, _zca]), { _yca -> s(s(s(s(z)))) ; _zca -> s(s(s(z))) ; l -> cons(s(s(s(s(z)))), cons(s(s(z)), nil)) ; x -> z }) Total time: 2104.585646 Reason for stopping: DontKnow. Stopped because: timeout