YES Problem: not(tt()) -> ff() not(ff()) -> tt() or(tt(),x) -> tt() or(ff(),x) -> x eq(0(),0()) -> tt() eq(s(x),0()) -> ff() eq(0(),s(y)) -> ff() eq(s(x),s(y)) -> eq(x,y) main(phi) -> ver(phi,nil()) in(x,nil()) -> ff() in(x,cons(a,l)) -> or(eq(x,a),in(x,l)) ver(Var(x),t()) -> in(x,t()) ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) -> not(ver(phi,t())) ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t())) Proof: DP Processor: DPs: eq#(s(x),s(y)) -> eq#(x,y) main#(phi) -> ver#(phi,nil()) in#(x,cons(a,l)) -> in#(x,l) in#(x,cons(a,l)) -> eq#(x,a) in#(x,cons(a,l)) -> or#(eq(x,a),in(x,l)) ver#(Var(x),t()) -> in#(x,t()) ver#(Or(phi,psi),t()) -> ver#(psi,t()) ver#(Or(phi,psi),t()) -> ver#(phi,t()) ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t())) ver#(Not(phi),t()) -> ver#(phi,t()) ver#(Not(phi),t()) -> not#(ver(phi,t())) ver#(Exists(n,phi),t()) -> ver#(phi,t()) ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t())) TRS: not(tt()) -> ff() not(ff()) -> tt() or(tt(),x) -> tt() or(ff(),x) -> x eq(0(),0()) -> tt() eq(s(x),0()) -> ff() eq(0(),s(y)) -> ff() eq(s(x),s(y)) -> eq(x,y) main(phi) -> ver(phi,nil()) in(x,nil()) -> ff() in(x,cons(a,l)) -> or(eq(x,a),in(x,l)) ver(Var(x),t()) -> in(x,t()) ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) -> not(ver(phi,t())) ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t())) TDG Processor: DPs: eq#(s(x),s(y)) -> eq#(x,y) main#(phi) -> ver#(phi,nil()) in#(x,cons(a,l)) -> in#(x,l) in#(x,cons(a,l)) -> eq#(x,a) in#(x,cons(a,l)) -> or#(eq(x,a),in(x,l)) ver#(Var(x),t()) -> in#(x,t()) ver#(Or(phi,psi),t()) -> ver#(psi,t()) ver#(Or(phi,psi),t()) -> ver#(phi,t()) ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t())) ver#(Not(phi),t()) -> ver#(phi,t()) ver#(Not(phi),t()) -> not#(ver(phi,t())) ver#(Exists(n,phi),t()) -> ver#(phi,t()) ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t())) TRS: not(tt()) -> ff() not(ff()) -> tt() or(tt(),x) -> tt() or(ff(),x) -> x eq(0(),0()) -> tt() eq(s(x),0()) -> ff() eq(0(),s(y)) -> ff() eq(s(x),s(y)) -> eq(x,y) main(phi) -> ver(phi,nil()) in(x,nil()) -> ff() in(x,cons(a,l)) -> or(eq(x,a),in(x,l)) ver(Var(x),t()) -> in(x,t()) ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) -> not(ver(phi,t())) ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t())) graph: in#(x,cons(a,l)) -> in#(x,l) -> in#(x,cons(a,l)) -> or#(eq(x,a),in(x,l)) in#(x,cons(a,l)) -> in#(x,l) -> in#(x,cons(a,l)) -> eq#(x,a) in#(x,cons(a,l)) -> in#(x,l) -> in#(x,cons(a,l)) -> in#(x,l) in#(x,cons(a,l)) -> eq#(x,a) -> eq#(s(x),s(y)) -> eq#(x,y) ver#(Exists(n,phi),t()) -> ver#(phi,t()) -> ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t())) ver#(Exists(n,phi),t()) -> ver#(phi,t()) -> ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ver#(Exists(n,phi),t()) -> ver#(phi,t()) -> ver#(Exists(n,phi),t()) -> ver#(phi,t()) ver#(Exists(n,phi),t()) -> ver#(phi,t()) -> ver#(Not(phi),t()) -> not#(ver(phi,t())) ver#(Exists(n,phi),t()) -> ver#(phi,t()) -> ver#(Not(phi),t()) -> ver#(phi,t()) ver#(Exists(n,phi),t()) -> ver#(phi,t()) -> ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t())) ver#(Exists(n,phi),t()) -> ver#(phi,t()) -> ver#(Or(phi,psi),t()) -> ver#(phi,t()) ver#(Exists(n,phi),t()) -> ver#(phi,t()) -> ver#(Or(phi,psi),t()) -> ver#(psi,t()) ver#(Exists(n,phi),t()) -> ver#(phi,t()) -> ver#(Var(x),t()) -> in#(x,t()) ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) -> ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t())) ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) -> ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) -> ver#(Exists(n,phi),t()) -> ver#(phi,t()) ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) -> ver#(Not(phi),t()) -> not#(ver(phi,t())) ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) -> ver#(Not(phi),t()) -> ver#(phi,t()) ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) -> ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t())) ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) -> ver#(Or(phi,psi),t()) -> ver#(phi,t()) ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) -> ver#(Or(phi,psi),t()) -> ver#(psi,t()) ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) -> ver#(Var(x),t()) -> in#(x,t()) ver#(Not(phi),t()) -> ver#(phi,t()) -> ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t())) ver#(Not(phi),t()) -> ver#(phi,t()) -> ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ver#(Not(phi),t()) -> ver#(phi,t()) -> ver#(Exists(n,phi),t()) -> ver#(phi,t()) ver#(Not(phi),t()) -> ver#(phi,t()) -> ver#(Not(phi),t()) -> not#(ver(phi,t())) ver#(Not(phi),t()) -> ver#(phi,t()) -> ver#(Not(phi),t()) -> ver#(phi,t()) ver#(Not(phi),t()) -> ver#(phi,t()) -> ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t())) ver#(Not(phi),t()) -> ver#(phi,t()) -> ver#(Or(phi,psi),t()) -> ver#(phi,t()) ver#(Not(phi),t()) -> ver#(phi,t()) -> ver#(Or(phi,psi),t()) -> ver#(psi,t()) ver#(Not(phi),t()) -> ver#(phi,t()) -> ver#(Var(x),t()) -> in#(x,t()) ver#(Or(phi,psi),t()) -> ver#(psi,t()) -> ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t())) ver#(Or(phi,psi),t()) -> ver#(psi,t()) -> ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ver#(Or(phi,psi),t()) -> ver#(psi,t()) -> ver#(Exists(n,phi),t()) -> ver#(phi,t()) ver#(Or(phi,psi),t()) -> ver#(psi,t()) -> ver#(Not(phi),t()) -> not#(ver(phi,t())) ver#(Or(phi,psi),t()) -> ver#(psi,t()) -> ver#(Not(phi),t()) -> ver#(phi,t()) ver#(Or(phi,psi),t()) -> ver#(psi,t()) -> ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t())) ver#(Or(phi,psi),t()) -> ver#(psi,t()) -> ver#(Or(phi,psi),t()) -> ver#(phi,t()) ver#(Or(phi,psi),t()) -> ver#(psi,t()) -> ver#(Or(phi,psi),t()) -> ver#(psi,t()) ver#(Or(phi,psi),t()) -> ver#(psi,t()) -> ver#(Var(x),t()) -> in#(x,t()) ver#(Or(phi,psi),t()) -> ver#(phi,t()) -> ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t())) ver#(Or(phi,psi),t()) -> ver#(phi,t()) -> ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) ver#(Or(phi,psi),t()) -> ver#(phi,t()) -> ver#(Exists(n,phi),t()) -> ver#(phi,t()) ver#(Or(phi,psi),t()) -> ver#(phi,t()) -> ver#(Not(phi),t()) -> not#(ver(phi,t())) ver#(Or(phi,psi),t()) -> ver#(phi,t()) -> ver#(Not(phi),t()) -> ver#(phi,t()) ver#(Or(phi,psi),t()) -> ver#(phi,t()) -> ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t())) ver#(Or(phi,psi),t()) -> ver#(phi,t()) -> ver#(Or(phi,psi),t()) -> ver#(phi,t()) ver#(Or(phi,psi),t()) -> ver#(phi,t()) -> ver#(Or(phi,psi),t()) -> ver#(psi,t()) ver#(Or(phi,psi),t()) -> ver#(phi,t()) -> ver#(Var(x),t()) -> in#(x,t()) ver#(Var(x),t()) -> in#(x,t()) -> in#(x,cons(a,l)) -> or#(eq(x,a),in(x,l)) ver#(Var(x),t()) -> in#(x,t()) -> in#(x,cons(a,l)) -> eq#(x,a) ver#(Var(x),t()) -> in#(x,t()) -> in#(x,cons(a,l)) -> in#(x,l) main#(phi) -> ver#(phi,nil()) -> ver#(Exists(n,phi),t()) -> or#(ver(phi,cons(n,t())),ver(phi,t())) main#(phi) -> ver#(phi,nil()) -> ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) main#(phi) -> ver#(phi,nil()) -> ver#(Exists(n,phi),t()) -> ver#(phi,t()) main#(phi) -> ver#(phi,nil()) -> ver#(Not(phi),t()) -> not#(ver(phi,t())) main#(phi) -> ver#(phi,nil()) -> ver#(Not(phi),t()) -> ver#(phi,t()) main#(phi) -> ver#(phi,nil()) -> ver#(Or(phi,psi),t()) -> or#(ver(phi,t()),ver(psi,t())) main#(phi) -> ver#(phi,nil()) -> ver#(Or(phi,psi),t()) -> ver#(phi,t()) main#(phi) -> ver#(phi,nil()) -> ver#(Or(phi,psi),t()) -> ver#(psi,t()) main#(phi) -> ver#(phi,nil()) -> ver#(Var(x),t()) -> in#(x,t()) eq#(s(x),s(y)) -> eq#(x,y) -> eq#(s(x),s(y)) -> eq#(x,y) SCC Processor: #sccs: 3 #rules: 7 #arcs: 62/196 DPs: ver#(Exists(n,phi),t()) -> ver#(phi,t()) ver#(Or(phi,psi),t()) -> ver#(psi,t()) ver#(Or(phi,psi),t()) -> ver#(phi,t()) ver#(Not(phi),t()) -> ver#(phi,t()) ver#(Exists(n,phi),t()) -> ver#(phi,cons(n,t())) TRS: not(tt()) -> ff() not(ff()) -> tt() or(tt(),x) -> tt() or(ff(),x) -> x eq(0(),0()) -> tt() eq(s(x),0()) -> ff() eq(0(),s(y)) -> ff() eq(s(x),s(y)) -> eq(x,y) main(phi) -> ver(phi,nil()) in(x,nil()) -> ff() in(x,cons(a,l)) -> or(eq(x,a),in(x,l)) ver(Var(x),t()) -> in(x,t()) ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) -> not(ver(phi,t())) ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t())) Subterm Criterion Processor: simple projection: pi(ver#) = 0 problem: DPs: TRS: not(tt()) -> ff() not(ff()) -> tt() or(tt(),x) -> tt() or(ff(),x) -> x eq(0(),0()) -> tt() eq(s(x),0()) -> ff() eq(0(),s(y)) -> ff() eq(s(x),s(y)) -> eq(x,y) main(phi) -> ver(phi,nil()) in(x,nil()) -> ff() in(x,cons(a,l)) -> or(eq(x,a),in(x,l)) ver(Var(x),t()) -> in(x,t()) ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) -> not(ver(phi,t())) ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t())) Qed DPs: in#(x,cons(a,l)) -> in#(x,l) TRS: not(tt()) -> ff() not(ff()) -> tt() or(tt(),x) -> tt() or(ff(),x) -> x eq(0(),0()) -> tt() eq(s(x),0()) -> ff() eq(0(),s(y)) -> ff() eq(s(x),s(y)) -> eq(x,y) main(phi) -> ver(phi,nil()) in(x,nil()) -> ff() in(x,cons(a,l)) -> or(eq(x,a),in(x,l)) ver(Var(x),t()) -> in(x,t()) ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) -> not(ver(phi,t())) ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t())) Subterm Criterion Processor: simple projection: pi(in#) = 1 problem: DPs: TRS: not(tt()) -> ff() not(ff()) -> tt() or(tt(),x) -> tt() or(ff(),x) -> x eq(0(),0()) -> tt() eq(s(x),0()) -> ff() eq(0(),s(y)) -> ff() eq(s(x),s(y)) -> eq(x,y) main(phi) -> ver(phi,nil()) in(x,nil()) -> ff() in(x,cons(a,l)) -> or(eq(x,a),in(x,l)) ver(Var(x),t()) -> in(x,t()) ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) -> not(ver(phi,t())) ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t())) Qed DPs: eq#(s(x),s(y)) -> eq#(x,y) TRS: not(tt()) -> ff() not(ff()) -> tt() or(tt(),x) -> tt() or(ff(),x) -> x eq(0(),0()) -> tt() eq(s(x),0()) -> ff() eq(0(),s(y)) -> ff() eq(s(x),s(y)) -> eq(x,y) main(phi) -> ver(phi,nil()) in(x,nil()) -> ff() in(x,cons(a,l)) -> or(eq(x,a),in(x,l)) ver(Var(x),t()) -> in(x,t()) ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) -> not(ver(phi,t())) ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t())) Subterm Criterion Processor: simple projection: pi(eq#) = 1 problem: DPs: TRS: not(tt()) -> ff() not(ff()) -> tt() or(tt(),x) -> tt() or(ff(),x) -> x eq(0(),0()) -> tt() eq(s(x),0()) -> ff() eq(0(),s(y)) -> ff() eq(s(x),s(y)) -> eq(x,y) main(phi) -> ver(phi,nil()) in(x,nil()) -> ff() in(x,cons(a,l)) -> or(eq(x,a),in(x,l)) ver(Var(x),t()) -> in(x,t()) ver(Or(phi,psi),t()) -> or(ver(phi,t()),ver(psi,t())) ver(Not(phi),t()) -> not(ver(phi,t())) ver(Exists(n,phi),t()) -> or(ver(phi,cons(n,t())),ver(phi,t())) Qed