benchmarks : THEORY BEGIN IMPORTING strategy x,x1,x2,x3,x4,x5,x6,x7,x8:VAR real %|- *_ : PROOF (bernstein) QED % Heart dipole Heart(x1,x2,x3,x4,x5,x6,x7,x8): MACRO real = -x1*x6^3+3*x1*x6*x7^2-x3*x7^3+3*x3*x7*x6^2-x2*x5^3+3*x2*x5*x8^2-x4*x8^3+3*x4*x8*x5^2-0.9563453 Heart_forall_: LEMMA -0.1 <= x1 AND x1 <= 0.4 AND 0.4 <= x2 AND x2 <= 1 AND -0.7 <= x3 AND x3 <= -0.4 AND -0.7 <= x4 AND x4 <= 0.4 AND 0.1 <= x5 AND x5 <= 0.2 AND -0.1 <= x6 AND x6 <= 0.2 AND -0.3 <= x7 AND x7 <= 1.1 AND -1.1 <= x8 AND x8 <= -0.3 IMPLIES Heart(x1,x2,x3,x4,x5,x6,x7,x8) >= -1.7435 Heart_exists_: LEMMA EXISTS (x1,x2,x3,x4,x5,x6,x7,x8:real): -0.1 <= x1 AND x1 <= 0.4 AND 0.4 <= x2 AND x2 <= 1 AND -0.7 <= x3 AND x3 <= -0.4 AND -0.7 <= x4 AND x4 <= 0.4 AND 0.1 <= x5 AND x5 <= 0.2 AND -0.1 <= x6 AND x6 <= 0.2 AND -0.3 <= x7 AND x7 <= 1.1 AND -1.1 <= x8 AND x8 <= -0.3 AND Heart(x1,x2,x3,x4,x5,x6,x7,x8) <= -1.7434 Magnetism(x1,x2,x3,x4,x5,x6,x7): MACRO real = x1^2+2*x2^2+2*x3^2+2*x4^2+2*x5^2+2*x6^2+2*x7^2-x1 Magnetism_forall_: LEMMA x1<=1 AND x2<=1 AND x3<=1 AND x4<=1 AND x5<=1 AND x6<=1 AND x7<=1 AND -1<=x1 AND -1<=x2 AND -1<=x3 AND -1<=x4 AND -1<=x5 AND -1<=x6 AND -1<=x7 IMPLIES Magnetism(x1,x2,x3,x4,x5,x6,x7) >=-0.25001 Magnetism_exists_: LEMMA EXISTS (x1,x2,x3,x4,x5,x6,x7): x1<=1 AND x2<=1 AND x3<=1 AND x4<=1 AND x5<=1 AND x6<=1 AND x7<=1 AND -1<=x1 AND -1<=x2 AND -1<=x3 AND -1<=x4 AND -1<=x5 AND -1<=x6 AND -1<=x7 AND Magnetism(x1,x2,x3,x4,x5,x6,x7) <= -0.2499 Butcher(x1,x2,x3,x4,x5,x6): MACRO real = x6*x2^2 + x5*x3^2-x1*x4^2+x4^3+x4^2-(1/3)*x1+(4/3)*x4 Butcher_forall_: LEMMA -1<=x1 AND x1<=0 AND -0.1<=x2 AND x2<=0.9 AND -0.1<=x3 AND x3<=0.5 AND -1<=x4 AND x4<=-0.1 AND -0.1<=x5 AND x5<=-0.05 AND -0.1<=x6 AND x6<=-0.03 IMPLIES Butcher(x1,x2,x3,x4,x5,x6) >= -1.44 %-0.21901 Butcher_exists_: LEMMA EXISTS (x1,x2,x3,x4,x5,x6): -1<=x1 AND x1<=0 AND -0.1<=x2 AND x2<=0.9 AnD -0.1<=x3 AND x3<=0.5 AND -1<=x4 AND x4<=-0.1 AND -0.1<=x5 AND x5<=-0.05 AND -0.1<=x6 AND x6<=-0.03 AND Butcher(x1,x2,x3,x4,x5,x6) <= -0.21899 Trid(x1,x2,x3,x4): MACRO real = (x1-1)^2 + (x2-1)^2 + (x3-1)^2 + (x4-1)^2 -x1*x2-x2*x3-x3*x4 Trid_forall_: LEMMA -16<=x1 AND x1<=16 AND -16<=x2 AND x2<=16 AND -16<=x3 AND x3<=16 AND -16<=x4 AND x4<=16 IMPLIES Trid(x1,x2,x3,x4) >= -16.001 Trid_exists_: LEMMA EXISTS (x1,x2,x3,x4): -16<=x1 AND x1<=16 AND -16<=x2 AND x2<=16 AND -16<=x3 AND x3<=16 AND -16<=x4 AND x4<=16 AND Trid(x1,x2,x3,x4) < -15.999 AdaptiveLV(x1,x2,x3,x4): MACRO real = x1*x2^2+x1*x3^2+x1*x4^2-1.1*x1+1 AdaptiveLV_forall_: LEMMA -2<=x1 AND x1<=2 AND -2<=x2 AND x2<=2 AND -2<=x3 AND x3<=2 AND -2<=x4 AND x4<=2 IMPLIES AdaptiveLV(x1,x2,x3,x4) >= -20.801 AdaptiveLV_exists_: LEMMA EXISTS (x1,x2,x3,x4): -2<=x1 AND x1<=2 AND -2<=x2 AND x2<=2 AND -2<=x3 AND x3<=2 AND -2<=x4 AND x4<=2 AND AdaptiveLV(x1,x2,x3,x4) <= -20.799 Caprasse(x1,x2,x3,x4): MACRO real = -x1*x3^3+4*x2*x3^2*x4+4*x1*x3*x4^2+2*x2*x4^3+4*x1*x3+4*x3^2-10*x2*x4-10*x4^2+2 Caprasse_forall_: LEMMA -0.5<=x1 AND x1<=0.5 AND -0.5<=x2 AND x2<=0.5 AND -0.5<=x3 AND x3<=0.5 AND -0.5<=x4 AND x4<=0.5 IMPLIES Caprasse(x1,x2,x3,x4) >= -3.18010 Caprasse_exists_: LEMMA EXISTS (x1,x2,x3,x4): -2<=x1 AND x1<=2 AND -2<=x2 AND x2<=2 AND -2<=x3 AND x3<=2 AND -2<=x4 AND x4<=2 AND Caprasse(x1,x2,x3,x4) <= -3.18009 Schwefel(x1,x2,x3): MACRO real = (x1-x2^2)^2+(x2-1)^2+(x1-x3^2)^2+(x3-1)^2 Schwefel_forall_: LEMMA -10<=x1 AND x1<=10 AND -10<=x2 AND x2<=10 AND -10<=x3 AND x3<=10 IMPLIES Schwefel(x1,x2,x3) >= -0.00000000058806 Schwefel_exists_: LEMMA EXISTS (x1,x2,x3): -10<=x1 AND x1<=10 AND -10<=x2 AND x2<=10 AND -10<=x3 AND x3<=10 AND Schwefel(x1,x2,x3) <= 0.00000000058806 ReactionDiffusion(x1,x2,x3): MACRO real = -x1+2*x2-x3-0.835634534*x2*(1+x2) ReactionDiffusion_forall_: LEMMA -5<=x1 AND x1<=5 AND -5<=x2 AND x2<=5 AND -5<=x3 AND x3<=5 IMPLIES ReactionDiffusion(x1,x2,x3) >= -36.7126907 ReactionDiffusion_exists_: LEMMA EXISTS (x1,x2,x3): -5<=x1 AND x1<=5 AND -5<=x2 AND x2<=5 AND -5<=x3 AND x3<=5 AND ReactionDiffusion(x1,x2,x3) <= -36.7126 Chebyshev1 : LEMMA abs(x) <= 1 IMPLIES (2*x^2 -1)^2 <= 1 Chebyshev2 : LEMMA abs(x) <= 1 IMPLIES (4*x^3 -3*x)^2 <= 1 END benchmarks