YES We show the termination of the TRS R: not(not(x)) -> x not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(not(not(x))) p2: not#(or(x,y)) -> not#(not(x)) p3: not#(or(x,y)) -> not#(x) p4: not#(or(x,y)) -> not#(not(not(y))) p5: not#(or(x,y)) -> not#(not(y)) p6: not#(or(x,y)) -> not#(y) p7: not#(and(x,y)) -> not#(not(not(x))) p8: not#(and(x,y)) -> not#(not(x)) p9: not#(and(x,y)) -> not#(x) p10: not#(and(x,y)) -> not#(not(not(y))) p11: not#(and(x,y)) -> not#(not(y)) p12: not#(and(x,y)) -> not#(y) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(not(not(x))) p2: not#(and(x,y)) -> not#(y) p3: not#(and(x,y)) -> not#(not(y)) p4: not#(and(x,y)) -> not#(not(not(y))) p5: not#(and(x,y)) -> not#(x) p6: not#(and(x,y)) -> not#(not(x)) p7: not#(and(x,y)) -> not#(not(not(x))) p8: not#(or(x,y)) -> not#(y) p9: not#(or(x,y)) -> not#(not(y)) p10: not#(or(x,y)) -> not#(not(not(y))) p11: not#(or(x,y)) -> not#(x) p12: not#(or(x,y)) -> not#(not(x)) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The set of usable rules consists of r1, r2, r3 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: not#_A(x1) = max{5, x1 + 3} or_A(x1,x2) = max{7, x1 + 4, x2 + 4} not_A(x1) = max{3, x1} and_A(x1,x2) = max{7, x1 + 4, x2 + 4} base order 2: precedence: not > and > or > not# partial status: pi(not#) = [1] pi(or) = [1, 2] pi(not) = [1] pi(and) = [2] The following rules are removed: p12 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(not(not(x))) p2: not#(and(x,y)) -> not#(y) p3: not#(and(x,y)) -> not#(not(y)) p4: not#(and(x,y)) -> not#(not(not(y))) p5: not#(and(x,y)) -> not#(x) p6: not#(and(x,y)) -> not#(not(x)) p7: not#(and(x,y)) -> not#(not(not(x))) p8: not#(or(x,y)) -> not#(y) p9: not#(or(x,y)) -> not#(not(y)) p10: not#(or(x,y)) -> not#(not(not(y))) p11: not#(or(x,y)) -> not#(x) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(not(not(x))) p2: not#(or(x,y)) -> not#(x) p3: not#(or(x,y)) -> not#(not(not(y))) p4: not#(or(x,y)) -> not#(not(y)) p5: not#(or(x,y)) -> not#(y) p6: not#(and(x,y)) -> not#(not(not(x))) p7: not#(and(x,y)) -> not#(not(x)) p8: not#(and(x,y)) -> not#(x) p9: not#(and(x,y)) -> not#(not(not(y))) p10: not#(and(x,y)) -> not#(not(y)) p11: not#(and(x,y)) -> not#(y) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The set of usable rules consists of r1, r2, r3 Take the monotone reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: not#_A(x1) = max{5, x1 + 2} or_A(x1,x2) = max{11, x1 + 4, x2 + 3} not_A(x1) = max{7, x1} and_A(x1,x2) = max{11, x1 + 4, x2 + 3} base order 2: precedence: or = not > and > not# partial status: pi(not#) = [1] pi(or) = [1, 2] pi(not) = [1] pi(and) = [1, 2] The following rules are removed: p1 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(x) p2: not#(or(x,y)) -> not#(not(not(y))) p3: not#(or(x,y)) -> not#(not(y)) p4: not#(or(x,y)) -> not#(y) p5: not#(and(x,y)) -> not#(not(not(x))) p6: not#(and(x,y)) -> not#(not(x)) p7: not#(and(x,y)) -> not#(x) p8: not#(and(x,y)) -> not#(not(not(y))) p9: not#(and(x,y)) -> not#(not(y)) p10: not#(and(x,y)) -> not#(y) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(x) p2: not#(and(x,y)) -> not#(y) p3: not#(and(x,y)) -> not#(not(y)) p4: not#(and(x,y)) -> not#(not(not(y))) p5: not#(and(x,y)) -> not#(x) p6: not#(and(x,y)) -> not#(not(x)) p7: not#(and(x,y)) -> not#(not(not(x))) p8: not#(or(x,y)) -> not#(y) p9: not#(or(x,y)) -> not#(not(y)) p10: not#(or(x,y)) -> not#(not(not(y))) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The set of usable rules consists of r1, r2, r3 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: not#_A(x1) = x1 + 2 or_A(x1,x2) = max{5, x1 + 3, x2 + 3} and_A(x1,x2) = max{5, x1 + 3, x2 + 3} not_A(x1) = max{2, x1} base order 2: precedence: not > or > and > not# partial status: pi(not#) = [1] pi(or) = [] pi(and) = [2] pi(not) = [1] The following rules are removed: p10 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(x) p2: not#(and(x,y)) -> not#(y) p3: not#(and(x,y)) -> not#(not(y)) p4: not#(and(x,y)) -> not#(not(not(y))) p5: not#(and(x,y)) -> not#(x) p6: not#(and(x,y)) -> not#(not(x)) p7: not#(and(x,y)) -> not#(not(not(x))) p8: not#(or(x,y)) -> not#(y) p9: not#(or(x,y)) -> not#(not(y)) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8, p9} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(x) p2: not#(or(x,y)) -> not#(not(y)) p3: not#(or(x,y)) -> not#(y) p4: not#(and(x,y)) -> not#(not(not(x))) p5: not#(and(x,y)) -> not#(not(x)) p6: not#(and(x,y)) -> not#(x) p7: not#(and(x,y)) -> not#(not(not(y))) p8: not#(and(x,y)) -> not#(not(y)) p9: not#(and(x,y)) -> not#(y) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The set of usable rules consists of r1, r2, r3 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: not#_A(x1) = max{1, x1 - 1} or_A(x1,x2) = max{x1 + 5, x2} not_A(x1) = x1 and_A(x1,x2) = max{x1 + 5, x2} base order 2: precedence: not > or = and > not# partial status: pi(not#) = [] pi(or) = [] pi(not) = [1] pi(and) = [] The following rules are removed: p1 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(not(y)) p2: not#(or(x,y)) -> not#(y) p3: not#(and(x,y)) -> not#(not(not(x))) p4: not#(and(x,y)) -> not#(not(x)) p5: not#(and(x,y)) -> not#(x) p6: not#(and(x,y)) -> not#(not(not(y))) p7: not#(and(x,y)) -> not#(not(y)) p8: not#(and(x,y)) -> not#(y) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7, p8} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(not(y)) p2: not#(and(x,y)) -> not#(y) p3: not#(and(x,y)) -> not#(not(y)) p4: not#(and(x,y)) -> not#(not(not(y))) p5: not#(and(x,y)) -> not#(x) p6: not#(and(x,y)) -> not#(not(x)) p7: not#(and(x,y)) -> not#(not(not(x))) p8: not#(or(x,y)) -> not#(y) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The set of usable rules consists of r1, r2, r3 Take the monotone reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: not#_A(x1) = x1 + 2 or_A(x1,x2) = max{8, x1 + 4, x2 + 2} not_A(x1) = max{3, x1} and_A(x1,x2) = max{8, x1 + 4, x2 + 2} base order 2: precedence: not > and > or > not# partial status: pi(not#) = [1] pi(or) = [1, 2] pi(not) = [1] pi(and) = [1, 2] The following rules are removed: p8 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(not(y)) p2: not#(and(x,y)) -> not#(y) p3: not#(and(x,y)) -> not#(not(y)) p4: not#(and(x,y)) -> not#(not(not(y))) p5: not#(and(x,y)) -> not#(x) p6: not#(and(x,y)) -> not#(not(x)) p7: not#(and(x,y)) -> not#(not(not(x))) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6, p7} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(not(y)) p2: not#(and(x,y)) -> not#(not(not(x))) p3: not#(and(x,y)) -> not#(not(x)) p4: not#(and(x,y)) -> not#(x) p5: not#(and(x,y)) -> not#(not(not(y))) p6: not#(and(x,y)) -> not#(not(y)) p7: not#(and(x,y)) -> not#(y) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The set of usable rules consists of r1, r2, r3 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: not#_A(x1) = max{3, x1 - 3} or_A(x1,x2) = max{10, x1 + 8, x2 + 7} not_A(x1) = max{2, x1} and_A(x1,x2) = max{10, x1 + 8, x2 + 7} base order 2: precedence: not > and > or > not# partial status: pi(not#) = [] pi(or) = [] pi(not) = [1] pi(and) = [2] The following rules are removed: p7 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(not(y)) p2: not#(and(x,y)) -> not#(not(not(x))) p3: not#(and(x,y)) -> not#(not(x)) p4: not#(and(x,y)) -> not#(x) p5: not#(and(x,y)) -> not#(not(not(y))) p6: not#(and(x,y)) -> not#(not(y)) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5, p6} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(not(y)) p2: not#(and(x,y)) -> not#(not(y)) p3: not#(and(x,y)) -> not#(not(not(y))) p4: not#(and(x,y)) -> not#(x) p5: not#(and(x,y)) -> not#(not(x)) p6: not#(and(x,y)) -> not#(not(not(x))) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The set of usable rules consists of r1, r2, r3 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: not#_A(x1) = max{5, x1 + 3} or_A(x1,x2) = max{14, x1 + 4, x2 + 7} not_A(x1) = max{6, x1} and_A(x1,x2) = max{14, x1 + 4, x2 + 7} base order 2: precedence: not > and > or > not# partial status: pi(not#) = [1] pi(or) = [] pi(not) = [1] pi(and) = [2] The following rules are removed: p6 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(not(y)) p2: not#(and(x,y)) -> not#(not(y)) p3: not#(and(x,y)) -> not#(not(not(y))) p4: not#(and(x,y)) -> not#(x) p5: not#(and(x,y)) -> not#(not(x)) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(not(y)) p2: not#(and(x,y)) -> not#(not(x)) p3: not#(and(x,y)) -> not#(x) p4: not#(and(x,y)) -> not#(not(not(y))) p5: not#(and(x,y)) -> not#(not(y)) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The set of usable rules consists of r1, r2, r3 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: not#_A(x1) = x1 + 2 or_A(x1,x2) = max{5, x1 + 4, x2 + 4} not_A(x1) = max{1, x1} and_A(x1,x2) = max{5, x1 + 4, x2 + 4} base order 2: precedence: not# > not > or > and partial status: pi(not#) = [1] pi(or) = [] pi(not) = [1] pi(and) = [2] The following rules are removed: p5 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(not(y)) p2: not#(and(x,y)) -> not#(not(x)) p3: not#(and(x,y)) -> not#(x) p4: not#(and(x,y)) -> not#(not(not(y))) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(not(y)) p2: not#(and(x,y)) -> not#(not(not(y))) p3: not#(and(x,y)) -> not#(x) p4: not#(and(x,y)) -> not#(not(x)) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The set of usable rules consists of r1, r2, r3 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: not#_A(x1) = max{3, x1 - 3} or_A(x1,x2) = max{10, x1 + 8, x2 + 7} not_A(x1) = max{2, x1} and_A(x1,x2) = max{10, x1 + 8, x2 + 7} base order 2: precedence: not > and > or > not# partial status: pi(not#) = [] pi(or) = [2] pi(not) = [1] pi(and) = [1, 2] The following rules are removed: p4 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(not(y)) p2: not#(and(x,y)) -> not#(not(not(y))) p3: not#(and(x,y)) -> not#(x) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The estimated dependency graph contains the following SCCs: {p1, p2, p3} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(not(y)) p2: not#(and(x,y)) -> not#(x) p3: not#(and(x,y)) -> not#(not(not(y))) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The set of usable rules consists of r1, r2, r3 Take the monotone reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: not#_A(x1) = max{7, x1} or_A(x1,x2) = max{7, x1 + 4, x2 + 2} not_A(x1) = max{3, x1} and_A(x1,x2) = max{7, x1 + 4, x2 + 2} base order 2: precedence: not > and > or > not# partial status: pi(not#) = [1] pi(or) = [1, 2] pi(not) = [1] pi(and) = [1, 2] The following rules are removed: p3 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(not(y)) p2: not#(and(x,y)) -> not#(x) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The estimated dependency graph contains the following SCCs: {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(not(y)) p2: not#(and(x,y)) -> not#(x) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The set of usable rules consists of r1, r2, r3 Take the monotone reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: not#_A(x1) = max{4, x1 + 2} or_A(x1,x2) = max{10, x1 + 3, x2 + 3} not_A(x1) = max{6, x1} and_A(x1,x2) = max{10, x1 + 3, x2 + 3} base order 2: precedence: not > or > and > not# partial status: pi(not#) = [1] pi(or) = [1, 2] pi(not) = [1] pi(and) = [1, 2] The following rules are removed: p2 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(not(y)) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: not#(or(x,y)) -> not#(not(y)) and R consists of: r1: not(not(x)) -> x r2: not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) r3: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) The set of usable rules consists of r1, r2, r3 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: not#_A(x1) = x1 + 7 or_A(x1,x2) = max{10, x1 - 3, x2 + 8} not_A(x1) = max{2, x1} and_A(x1,x2) = max{10, x1 - 3, x2 + 8} base order 2: precedence: not > and > or > not# partial status: pi(not#) = [1] pi(or) = [2] pi(not) = [1] pi(and) = [] The following rules are removed: p1 Then no dependency pair remains.