Parse: ∃x[P(x)∧∀x[Q(x)]]
Parse: ∀y∃x[P(x)∧G(y)]
Parse: ∃x[P(x)∧∀x[Q(x)⇒¬P(x)]]
Parse: ∀x[P(x)⇔(Q(x)∧∃y[Q(y)∧R(y,x)])]
Parse: ∀x[P(x)⇒Y(x)⇒G(x)]
Input is: ∃x[P(x) ∧ ∀x[Q(x)]], Output is: ∃x[P(x)∧∀x[Q(x)]]
Are the same?: true
Input is: ∀y∃x[P(x) ∧ G(y)], Output is: ∀y∃x[P(x)∧G(y)]
Are the same?: true
Input is: ∃x[P(x) ∧ ∀x[Q(x) ⇒ ¬P(x)]], Output is: ∃x[P(x)∧∀x[Q(x)⇒¬P(x)]]
Are the same?: true
Input is: ∀x[P(x) ⇔ (Q(x) ∧ ∃y[Q(y) ∧ R(y, x)])], Output is: ∀x[P(x)⇔(Q(x)∧∃y[Q(y)∧R(y,x)])]
Are the same?: true
Are the same?: true
========== Start Converting ==========
Prepare the expression: ∃x[P(x)∧∀x[Q(x)]]
Starting Expression: ∃x[P(x)∧∀x[Q(x)]]
After removing IFFs: ∃x[P(x)∧∀x[Q(x)]]
After removing Implications: ∃x[P(x)∧∀x[Q(x)]]
After pushing negation: ∃x[P(x)∧∀x[Q(x)]]
After standardizing quantifiers: ∃g[P(g)∧∀f[Q(f)]]
========== Start Converting ==========
Prepare the expression: ∀y∃x[P(x)∧G(y)]
Starting Expression: ∀y∃x[P(x)∧G(y)]
After removing IFFs: ∀y∃x[P(x)∧G(y)]
After removing Implications: ∀y∃x[P(x)∧G(y)]
After pushing negation: ∀y∃x[P(x)∧G(y)]
After standardizing quantifiers: ∀f∃g[P(g)∧G(f)]
========== Start Converting ==========
Prepare the expression: ∃x[P(x)∧∀x[Q(x)⇒¬P(x)]]
Starting Expression: ∃x[P(x)∧∀x[Q(x)⇒¬P(x)]]
After removing IFFs: ∃x[P(x)∧∀x[Q(x)⇒¬P(x)]]
After removing Implications: ∃x[P(x)∧∀x[¬Q(x)|¬P(x)]]
After pushing negation: ∃x[P(x)∧∀x[¬Q(x)|¬P(x)]]
After standardizing quantifiers: ∃g[P(g)∧∀f[¬Q(f)|¬P(f)]]
========== Start Converting ==========
Prepare the expression: ∀x[P(x)⇔(Q(x)∧∃y[Q(y)∧R(y,x)])]
Starting Expression: ∀x[P(x)⇔(Q(x)∧∃y[Q(y)∧R(y,x)])]
After removing IFFs: ∀x[((Q(x)∧∃y[Q(y)∧R(y,x)])⇒P(x))∧(P(x)⇒(Q(x)∧∃y[Q(y)∧R(y,x)]))]
After removing Implications: ∀x[(¬(Q(x)∧∃y[Q(y)∧R(y,x)])|P(x))∧(¬P(x)|(Q(x)∧∃y[Q(y)∧R(y,x)]))]
After pushing negation: ∀x[((¬Q(x)|∃y[¬Q(y)|¬R(y,x)])|P(x))∧(¬P(x)|(¬Q(x)∧∃y[¬Q(y)|¬R(y,x)]))]
After standardizing quantifiers: ∀f[((¬Q(f)|∃y[¬Q(y)|¬R(y,f)])|P(f))∧(¬P(f)|(¬Q(f)∧∃y[¬Q(y)|¬R(y,f)]))]
========== Start Converting ==========
Prepare the expression: ∀x[P(x)⇒Y(x)⇒G(x)]
Starting Expression: ∀x[(P(x)⇒Y(x))⇒G(x)]
After removing IFFs: ∀x[(P(x)⇒Y(x))⇒G(x)]
After removing Implications: ∀x[¬(¬P(x)|Y(x))|G(x)]
After pushing negation: ∀x[(P(x)∧¬Y(x))|G(x)]
After standardizing quantifiers: ∀f[(P(f)∧¬Y(f))|G(f)]