The square root of 2 is irrational proof

Step	Using
integer(X) and exists(X) and integer(Y) and exists(Y) and true=> not (X > 0 and Y > 0 and 2 * X * X = Y * Y) ;
integer(X) and exists(X) and integer(Y) and exists(Y) and integer(V0) and any (V0) and integer(V1) and any(V1) and true=> not (X > 0 and Y > 0 and 2 * X * X = Y * Y and ( V0 > 0 and V1 > 0 and 2 * V0 * V0 = V1 * V1=> not X > V0 )) ;	Ascendancy
integer(X) and exists(X) and integer(Y) and exists(Y) and integer(V0) and any (V0) and integer(V1) and any(V1) and true=> not (X > 0 and Y > 0 and 2 * X * X = Y * Y and ( V0 > 0 and V1 > 0 and 2 * V0 * V0 = V1 * V1=> not X > V0 ) and (factor(2,Y * Y))) ;	Induction factor
integer(X) and exists(X) and integer(Y) and exists(Y) and integer(V0) and any (V0) and integer(V1) and any(V1) and true=> not (X > 0 and Y > 0 and 2 * X * X = Y * Y and ( V0 > 0 and V1 > 0 and 2 * V0 * V0 = V1 * V1=> not X > V0 ) and (factor(2,Y * Y)) and (factor(2,Y))) ;	Induction prime_factor
integer(X) and exists(X) and integer(Y) and exists(Y) and integer(V0) and any (V0) and integer(V1) and any(V1) and integer(V2) and exists(V2) and true=> not (X > 0 and Y > 0 and 2 * X * X = Y * Y and ( V0 > 0 and V1 > 0 and 2 * V0 * V0 = V1 * V1=> not X > V0 ) and (factor(2,Y * Y)) and 2 * V2 = Y) ;	Induction factor
integer(X) and exists(X) and integer(Y) and exists(Y) and integer(V0) and any (V0) and integer(V1) and any(V1) and integer(V2) and exists(V2) and true=> not (X > 0 and Y > 0 and 2 * X * X = Y * Y and ( V0 > 0 and V1 > 0 and 2 * V0 * V0 = V1 * V1=> not X > V0 ) and (factor(2,Y * Y)) and 2 * V2 = Y and 2 * V2 > 0) ;	Inference
integer(X) and exists(X) and integer(Y) and exists(Y) and integer(V0) and any (V0) and integer(V1) and any(V1) and integer(V2) and exists(V2) and true=> not (X > 0 and Y > 0 and 2 * X * X = Y * Y and ( V0 > 0 and V1 > 0 and 2 * V0 * V0 = V1 * V1=> not X > V0 ) and (factor(2,Y * Y)) and 2 * V2 = Y and 2 * V2 > 0 and V2 > 0) ;	Induction magnitude2
integer(X) and exists(X) and integer(Y) and exists(Y) and integer(V0) and any (V0) and integer(V1) and any(V1) and integer(V2) and exists(V2) and true=> not (X > 0 and Y > 0 and 2 * X * X = Y * Y and ( V0 > 0 and V1 > 0 and 2 * V0 * V0 = V1 * V1=> not X > V0 ) and (factor(2,Y * Y)) and 2 * V2 = Y and 2 * V2 > 0 and V2 > 0 and 2 * X * X = 2 * V2 * 2 * V2) ;	Inference
integer(X) and exists(X) and integer(Y) and exists(Y) and integer(V0) and any (V0) and integer(V1) and any(V1) and integer(V2) and exists(V2) and true=> not (X > 0 and Y > 0 and 2 * X * X = Y * Y and ( V0 > 0 and V1 > 0 and 2 * V0 * V0 = V1 * V1=> not X > V0 ) and (factor(2,Y * Y)) and 2 * V2 = Y and 2 * V2 > 0 and V2 > 0 and 2 * X * X = 2 * V2 * 2 * V2 and V2 * 2 * V2 = X * X) ;	Induction division
integer(X) and exists(X) and integer(Y) and exists(Y) and integer(V0) and any (V0) and integer(V1) and any(V1) and integer(V2) and exists(V2) and true=> not (X > 0 and Y > 0 and 2 * X * X = Y * Y and ( V0 > 0 and V1 > 0 and 2 * V0 * V0 = V1 * V1=> not X > V0 ) and (factor(2,Y * Y)) and 2 * V2 = Y and 2 * V2 > 0 and V2 > 0 and 2 * X * X = 2 * V2 * 2 * V2 and V2 * 2 * V2 = X * X and (factor(2,X * X))) ;	Induction factor
integer(X) and exists(X) and integer(Y) and exists(Y) and integer(V0) and any (V0) and integer(V1) and any(V1) and integer(V2) and exists(V2) and true=> not (X > 0 and Y > 0 and 2 * X * X = Y * Y and ( V0 > 0 and V1 > 0 and 2 * V0 * V0 = V1 * V1=> not X > V0 ) and (factor(2,Y * Y)) and 2 * V2 = Y and 2 * V2 > 0 and V2 > 0 and 2 * X * X = 2 * V2 * 2 * V2 and V2 * 2 * V2 = X * X and (factor(2,X * X)) and (factor(2,X)) ) ;	Induction prime_factor
integer(X) and exists(X) and integer(Y) and exists(Y) and integer(V0) and any (V0) and integer(V1) and any(V1) and integer(V2) and exists(V2) and integer(V3) and exists(V3) and true=> not (X > 0 and Y > 0 and 2 * X * X = Y * Y and ( V0 > 0 and V1 > 0 and 2 * V0 * V0 = V1 * V1=> not X > V0 ) and (factor(2,Y * Y)) and 2 * V2 = Y and 2 * V2 > 0 and V2 > 0 and 2 * X * X = 2 * V2 * 2 * V2 and V2 * 2 * V2 = X * X and (factor(2,X * X)) and 2 * V3 = X) ;	Induction factor
integer(X) and exists(X) and integer(Y) and exists(Y) and integer(V0) and any (V0) and integer(V1) and any(V1) and integer(V2) and exists(V2) and integer(V3) and exists(V3) and true=> not (X > 0 and Y > 0 and 2 * X * X = Y * Y and ( V0 > 0 and V1 > 0 and 2 * V0 * V0 = V1 * V1=> not X > V0 ) and (factor(2,Y * Y)) and 2 * V2 = Y and 2 * V2 > 0 and V2 > 0 and 2 * X * X = 2 * V2 * 2 * V2 and V2 * 2 * V2 = X * X and (factor(2,X * X)) and 2 * V3 = X and V2 * 2 * V2 = 2 * V3 * 2 * V3) ;	Inference
integer(X) and exists(X) and integer(Y) and exists(Y) and integer(V0) and any (V0) and integer(V1) and any(V1) and integer(V2) and exists(V2) and integer(V3) and exists(V3) and true=> not (X > 0 and Y > 0 and 2 * X * X = Y * Y and ( V0 > 0 and V1 > 0 and 2 * V0 * V0 = V1 * V1=> not X > V0 ) and (factor(2,Y * Y)) and 2 * V2 = Y and 2 * V2 > 0 and V2 > 0 and 2 * X * X = 2 * V2 * 2 * V2 and V2 * 2 * V2 = X * X and (factor(2,X * X)) and 2 * V3 = X and V2 * 2 * V2 = 2 * V3 * 2 * V3 and X > V3) ;	Induction magnitude1
integer(X) and exists(X) and integer(Y) and exists(Y) and integer(V0) and any (V0) and integer(V1) and any(V1) and integer(V2) and exists(V2) and integer(V3) and exists(V3) and true=> not (X > 0 and Y > 0 and 2 * X * X = Y * Y and ( V0 > 0 and V1 > 0 and 2 * V0 * V0 = V1 * V1=> not X > V0 ) and (factor(2,Y * Y)) and 2 * V2 = Y and 2 * V2 > 0 and V2 > 0 and 2 * X * X = 2 * V2 * 2 * V2 and V2 * 2 * V2 = X * X and (factor(2,X * X)) and 2 * V3 = X and V2 * 2 * V2 = 2 * V3 * 2 * V3 and X > V3 and 2 * V3 > 0) ;	Inference
integer(X) and exists(X) and integer(Y) and exists(Y) and integer(V0) and any (V0) and integer(V1) and any(V1) and integer(V2) and exists(V2) and integer(V3) and exists(V3) and true=> not (X > 0 and Y > 0 and 2 * X * X = Y * Y and ( V0 > 0 and V1 > 0 and 2 * V0 * V0 = V1 * V1=> not X > V0 ) and (factor(2,Y * Y)) and 2 * V2 = Y and 2 * V2 > 0 and V2 > 0 and 2 * X * X = 2 * V2 * 2 * V2 and V2 * 2 * V2 = X * X and (factor(2,X * X)) and 2 * V3 = X and V2 * 2 * V2 = 2 * V3 * 2 * V3 and X > V3 and 2 * V3 > 0 and V3 > 0) ;	Induction magnitude2
integer(X) and exists(X) and integer(Y) and exists(Y) and integer(V0) and any (V0) and integer(V1) and any(V1) and integer(V2) and exists(V2) and integer(V3) and exists(V3) and true=> not (X > 0 and Y > 0 and 2 * X * X = Y * Y and ( V0 > 0 and V1 > 0 and 2 * V0 * V0 = V1 * V1=> not X > V0 ) and (factor(2,Y * Y)) and 2 * V2 = Y and 2 * V2 > 0 and V2 > 0 and 2 * X * X = 2 * V2 * 2 * V2 and V2 * 2 * V2 = X * X and (factor(2,X * X)) and 2 * V3 = X and V2 * 2 * V2 = 2 * V3 * 2 * V3 and X > V3 and 2 * V3 > 0 and V3 > 0 and V3 * 2 * V3 = V2 * V2) ;	Induction division
true;	Induction local