Converts (some) SpacEx input files to KeYmaera X input files.

E.g., works for most of the Sogokon et al. 2016 nonlinear benchmarks:

	{
		"arrowsmith_and_place_fig_1_32_page_14": "x=-1&y=1->[{x'=-x*y,y'=x^2+y^2&true}](!(x>0|y<=0))" ,
		"strogatz_ex_6_3_2": "x>-4/5&x < -1/3&y < 3/2&y>=1->[{x'=-x+x*(x^2+y^2),y'=x+y*(x^2+y^2)&true}](!(x < -1/3&y>=0&2*y < 1&x>-4/5))" ,
		"keymaera_nonlinear_diffcut": "x^3>=-1&y^5>=0->[{x'=(-3+x)^4+y^5,y'=y^2&true}](!(1+x < 0|y < 0))" ,
		"collin_goriely_page_60": "(2+x)^2+(-1+y)^2<=1/4->[{x'=x^2+2*x*y+3*y^2,y'=2*y*(2*x+y)&true}](!x>0)" ,
		"ben_sassi_girard_20104_moore_greitzer_jet": "-1/5000+(1/20+x)^2+(3/200+y)^2<=0->[{x'=-3*x^2/2-x^3/2-y,y'=3*x-y&true}](!49/100+x+x^2+y+y^2<=0)" ,
		"strogatz_ex_6_8_3": "2*(-1/3+x)^2+y^2 < 1/16->[{x'=x^2*y,y'=x^2-y^2&true}](!x<=-2)" ,
		"shimizu_morioka_system": "x=5&y=3&z=-4->[{x'=y,y'=x-y-x*z,z'=x^2-z&true}](!z < -5)" ,
		"strogatz_ex_6_1_5": "(-1/3+x)^2+2*(-1/3+y)^2 < 1/25->[{x'=x*(2-x-y),y'=x-y&true}](!(x>=2|x<=-2))" ,
		"stable_limit_cycle2": "x^2+y^2 < 1/16->[{x'=x-x^3+y-x*y^2,y'=-x+y-x^2*y-y^3&true}](!(x < -1|y < -1|x>1|y>1))" ,
		"keymaera_nonlinear1": "x^3>=-1->[{x'=a+(-3+x)^4,a'=0&a>=0}](!x^3 < -1)" ,
		"arrowsmith_and_place_fig_3_5c_page_79": "x^2+y^2>=1->[{x'=x-y^3,y'=x^3+y&true}](!x^2+y^2 < 1/2)" ,
		"ben_sassi_girard_sankaranarayanan_2014_fitzhugh-nagumo": "-1/20+(5/4+x)^2+(-5/4+y)^2<=0->[{x'=7/8+x-x^3/3-y,y'=2*(7/10+x-4*y/5)/25&true}](!36/5+5*x+x^2+2*y+y^2<=0)" ,
		"dumortier_llibre_artes_ex_1_11a": "x>-1/2&x < -1/3&y < 0&y>=-1/2->[{x'=2*x-x^5-x*y^4,y'=y-x^2*y-y^3&true}](!x+y>0)" ,
		"arrowsmith_and_place_fig_3_11_page_83": "x=1&y=1/8->[{x'=x-y^2,y'=y*(x-y^2)&true}](!x < 0)" ,
		"unstable_unit_circle2": "x=1/2&y=1/2->[{x'=-x+x^3-y+x*y^2,y'=x-y+x^2*y+y^3&true}](!x^2+y^2>2)" ,
		"dumortier_llibre_artes_ex_1_11b": "x>-1/2&x < -1/3&y < 0&y>=-1/2->[{x'=2*x-x^5-x*y^4,y'=y-x^2*y-y^3&true}](!x^2+y^2>5)" ,
		"prajna_phd_thesis_2_4_1_page_31": "(-3/2+x)^2+y^2<=1/4->[{x'=x,y'=-x+x^3/3-y&true}](!(1+x)^2+(1+y)^2<=4/25)" ,
		"arrowsmith_and_place_fig_1_30_page_14": "x=1&y=0->[{x'=y^2,y'=x&true}](!x < 0)" ,
		"arrowsmith_and_place_fig_1_29_page_14": "x=0&y=-1->[{x'=x,y'=y^2&true}](!y>0)" ,
		"forsman_phd_ex_6_1_page_99": "x^2+(-2+y)^2 < 1/24->[{x'=-x+2*x^2*y,y'=-y&true}](!(x<=-2|y<=-1))" ,
		"dumortier_llibre_artes_ex_10_9": "(-1+x)^2+(1+y)^2 < 1/4->[{x'=x^4+2*x*y^2-6*x^2*y^2+y^4+x*(x^2-y^2),y'=2*x^2*y-4*x^3*y+4*x*y^3-y*(x^2-y^2)&true}](!y>=1)" ,
		"lotka_volterra_fourth_quadrant": "x=0&y=1->[{x'=x*(1-y),y'=-(1-x)*y&x>=0&y>=0}](!y < 0)" ,
		"unstable_unit_circle3": "x=0&y=1/2->[{x'=-x+x^3-y+x*y^2,y'=x-y+x^2*y+y^3&x>=0&y>=0}](!x^2+y^2>1)" ,
		"dumortier_llibre_artes_ex_5_1_ii": "x>-1&x < 0&y < 0&y>=-1->[{x'=-1+x^2+y^2,y'=5*(-1+x*y)&true}](!x+y>1)" ,
		"dumortier_llibre_artes_ex_1_9b": "x>-1/2&x < -1/3&y < 0&y>=-1/2->[{x'=x*(1-x^2-y^2)+y*((-1+x^2)^2+y^2),y'=y*(1-x^2-y^2)-y*((-1+x^2)^2+y^2)&true}](!x^2+2*y^2>2)" ,
		"dai_gan_xhia_zhan_jsc14_ex5": "(1+x)^2+(-2+y)^2<=4/25->[{x'=y,y'=2*x-x^3-y-x^2*y&true}](!(-1+x)^2+y^2<=1/25)" ,
		"dumortier_llibre_artes_ex_5_13": "x>-1/2&x < 0&y < 0&y>=-1/2->[{x'=y,y'=2*(-1-y)*y&true}](!y>2)" ,
		"dumortier_llibre_artes_ex_5_2": "x>-1&x < -1/2&y < -1/2&y>=-1->[{x'=y,y'=x^5-x*y&true}](!x+y>1)" ,
		"djaballah_chaputot_kieffer_boussou_2015_ex1": "-1/20+(5/4+x)^2+(-5/4+y)^2<=0->[{x'=x+y,y'=x*y-y^2/2&true}](!(5/2+x)^2+(-4/5+y)^2<=1/20)" ,
		"dai_gan_xhia_zhan_jsc14_ex1": "1/100-x^2-y^2>=0->[{x'=-2*x+x^2+y,y'=x-2*y+y^2&true}](!x^2+y^2>=1/4)" ,
		"wiggins_ex_18_7_3_n": "(-1/3+x)^2+(-1/3+y)^2 < 1/16->[{x'=-x+2*y+x^2*y+x^4*y^5,y'=-y-x^4*y^6+x^8*y^9&true}](!(x<=-1|y<=-1))" ,
		"bhatia_szego_ex_2_4_page_68": "x^2+(-1/2+y)^2 < 1/24->[{x'=-x+2*x^3*y^2,y'=-y&x^2*y^2 < 1}](!(x<=-2|y<=-1))" ,
		"forsman_phd_ex_6_14_page_119": "x^2+(-1+y)^2 < 1/8->[{x'=-2*x+y^4,y'=-y+3*x*y^3&true}](!y<=-1)" ,
		"liu_zhan_zhao_emsoft11_ex_25": "x+y>=0->[{x'=-2*y,y'=x^2&true}](!(x < -1&y<=-1/2))" ,
		"arrowsmith_and_place_fig_3_8_page_82": "x=1&y=-1->[{x'=x*(x+2*y),y'=y*(2*x+y)&true}](!(x < 0|y>0))" ,
		"stable_limit_cycle1": "x^2+y^2 < 1/16->[{x'=x-x^3+y-x*y^2,y'=-x+y-x^2*y-y^3&true}](!(x<=-2|y>2))" ,
		"arrowsmith_and_place_fig_3_5e_page_79": "x=1&y=-1->[{x'=x^2+(x+y)/2,y'=(-x+3*y)/2&true}](!y>0)" ,
		"dumortier_llibre_artes_ex_5_2_ii": "x>-4/5&x < -1/3&y < 0&y>=-1->[{x'=2*x-2*x*y,y'=-x^2+2*y+y^2&true}](!(x=0&y=0|x+y>1))" ,
		"dumortier_llibre_artes_ex_10_15_i": "x>-1&x < -3/4&y<=3/2&y>=1->[{x'=-42*x^7+50*x^2*y+156*x^3*y+258*x^4*y-46*x^5*y+68*x^6*y+20*x*y^6-8*y^7,y'=y*(1110*x^6-3182*x^4*y-220*x^5*y+478*x^3*y^3+487*x^2*y^4-102*x*y^5-12*y^6)&true}](!x>1+y)" ,
		"dai_gan_xhia_zhan_jsc14_ex2": "x^2+(2+y)^2<=1->[{x'=2*x-x*y,y'=2*x^2-y&true}](!x^2+(-1+y)^2<=9/100)" ,
		"arrowsmith_and_place_fig_3_1_page_72": "x^2+y^2<=1/5->[{x'=-4*y+x*(1-x^2-y^2)-y*(x^2+y^2),y'=4*x+y*(1-x^2-y^2)+x*(x^2+y^2)&true}](!x^2+y^2>1)" ,
		"dumortier_llibre_artes_ex_1_9a": "x>-1/2&x < -1/3&y < 0&y>=-1/2->[{x'=x*(1-x^2-y^2)+y*((-1+x^2)^2+y^2),y'=y*(1-x^2-y^2)-y*((-1+x^2)^2+y^2)&true}](!x>=0)" ,
		"arrowsmith_and_place_fig_1_35_page_17": "x=1&y=1->[{x'=x*(2-x-2*y),y'=(2-2*x-y)*y&true}](!(x<=0|y<=0))" ,
		"strogatz_ex_6_6_1_reversible_system": "(-1/3+x)^2+(-1/3+y)^2 < 1/16->[{x'=(1-x^2)*y,y'=1-y^2&true}](!(x>=2|x<=-2))" ,
		"vinograd_system_chicone_1_145_page_80": "x=1&y=0->[{x'=y^5+x^2*(-x+y),y'=y^2*(-2*x+y)&true}](!(y>0|y < 0))" ,
		"dumortier_llibre_artes_ex_10_15_ii": "x>-1&x < -1/2&y<=-1/10&y>=-3/10->[{x'=315*x^7+477*x^6*y-113*x^5*y^2+301*x^4*y^3-300*x^3*y^4-192*x^2*y^5+128*x*y^6-16*y^7,y'=y*(2619*x^6-99*x^5*y-3249*x^4*y^2+1085*x^3*y^3+596*x^2*y^4-416*x*y^5+64*y^6)&true}](!x>1+y)" ,
		"strogatz_ex_7_3_5": "(-1/3+x)^2+(-1/3+y)^2 < 1/16->[{x'=-x-y+x*(x^2+2*y^2),y'=x-y+y*(x^2+2*y^2)&true}](!(x=0&y=0|x<=-2|y<=-1))" ,
		"hamiltonian_system_1": "(2/3+x)^2+y^2<=1/24->[{x'=-2*y,y'=-2*x-3*x^2&true}](!x>0)" ,
		"darboux_christoffel_int_goriely_page_58": "x^2+y^2<=1->[{x'=3*(-4+x^2),y'=3+x*y-y^2&true}](!(x < -4|y < -4|x>4|y>4))" ,
		"strogatz_ex_6_6_2_limit_cycle": "(-1/3+x)^2+(-1/3+y)^2 < 1/16->[{x'=y,y'=-x+y*(1-x^2-y^2)&true}](!(x^2+y^2=0|x>=2|x<=-2))" ,
		"van_der_pol_fourth_quadrant": "x=0&y=1->[{x'=y,y'=-x+(1-x^2)*y&x<=0&y>=0}](!x^2+y^2>10)" ,
		"wiggins_ex_17_1_2": "(-1/3+x)^2+(-1/3+y)^2 < 1/16->[{x'=(2+x)*(-(1-x)*x+y),y'=-y&true}](!x<=-5/2)" ,
		"synthetic_example1": "x=0&y=0->[{x'=-1+x^2+y^2,y'=x^2&true}](!y < 0)" ,
		"wiggins_ex_18_1_2": "(-1/3+x)^2+(-1/3+y)^2 < 1/16->[{x'=-x^6-x*y,y'=x^2-y&true}](!y<=-1)" ,
		"strogatz_ex_6_1_9_dipole": "(-1/3+x)^2+y^2 < 1/25->[{x'=2*x*y,y'=-x^2+y^2&true}](!x<=-2)" ,
		"dumortier_llibre_artes_ex_10_11": "x^2+y^2 < 1/4->[{x'=-70-100*x+70*x^2+100*x^3-200*y+200*x^2*y,y'=146*x+100*y+140*x*y+100*x^2*y+200*x*y^2&true}](!(2*x>=3|x<=-3/2))" ,
		"man_maccallum_goriely_page_57": "x^2+y^2<=1/4->[{x'=-y+2*x^2*y,y'=y+2*x*y^2&true}](!x>3)" ,
		"unstable_unit_circle1": "x=0&y=1/2->[{x'=-x+x^3-y+x*y^2,y'=x-y+x^2*y+y^3&true}](!x^2+y^2>1)" ,
		"alongi_nelson_ex_4_1_9_page_143": "x=1&y=0&z=0->[{x'=x*z,y'=y*z,z'=-x^2-y^2&x^2+y^2+z^2=1}](!(x>1|z>0))" ,
		"ahmadi_parrilo_kristic": "0.5<=x&x<=0.7&0<=y&y<=0.3->[{x'=-x+x*y,y'=-y&true}](!(-0.8>=x&x>=-1&-0.7>=y&y>=-1))" ,
		"arrowsmith_and_place_fig_3_9_page_83": "x=-1&y=-1->[{x'=x*(x-2*y),y'=-(2*x-y)*y&true}](!(x>0|y>0))" ,
		"arrowsmith_and_place_fig_1_31_page_14": "x=-1&y=1->[{x'=x^2,y'=(2*x-y)*y&true}](!(x>0|y<=0))" ,
		"fitzhugh_nagumo_ben_sassi_girard_2": "-1<=x&x<=-0.5&1<=y&y<=1.5->[{x'=7/8+x-x^3/3-y,y'=2*(7/10+x-4*y/5)/25&true}](!(-2.5<=x&x<=-2&-2<=y&y<=-1.5))" ,
		"dumortier_llibre_artes_ex_10_11b": "(-1+x)^2+(1+y)^2 < 1/4->[{x'=1+x+x^2+x^3+2*y+2*x^2*y,y'=-y+2*x*y+x^2*y+2*x*y^2&true}](!y>=1)" ,
		"invariant_3_dim_sphere": "x=1/4&y=1/8&z=1/10->[{x'=x^2-x*(x^3+y^3+z^3),y'=y^2-y*(x^3+y^3+z^3),z'=z^2-z*(x^3+y^3+z^3)&true}](!(x>10|y>5|z<=-20))" 
	}