# Generated with http://www.agfa.com/w3c/euler/#28.061 on Sat Dec 01 02:19:53 GMT+01:00 2001 # for query http://www.agfa.com/w3c/euler/tpoint-query.n3 # given [http://www.agfa.com/w3c/euler/tpoint.n3, http://www.agfa.com/w3c/euler/tpoint-facts.n3] @prefix log: . @prefix : . {{[ :center [ :X :0; :Y :2]; :radius [ :product :2; :product [ :slash [ :sqrt :5]]]; :apoint [ :X :3; :Y :6]] } log:implies {[ :center [ :X :0; :Y :2]; :radius [ :product :2; :product [ :slash [ :sqrt :5]]]; :apoint [ :X :3; :Y :6]] :slope [ :product [ :sum [ :minus [ :product :2; :product :3; :product [ :sum :6; :sum [ :minus :2]]]]; :sum [ :sqrt [ :sum [ :product :4; :product [ :square :3]; :product [ :square [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :product :4; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :2; :sum :6]]]; :sum [ :product :2; :product :2; :product [ :sum :0; :sum [ :minus :6]]]]]]]]]; :product [ :slash [ :product :2; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]]]]}} log:implies {[ :center [ :X :0; :Y :2]; :radius [ :product :2; :product [ :slash [ :sqrt :5]]]; :apoint [ :X :3; :Y :6]] :tpoint [ :X [ :product [ :sum [ :product [ :square [ :product [ :sum [ :minus [ :product :2; :product :3; :product [ :sum :6; :sum [ :minus :2]]]]; :sum [ :sqrt [ :sum [ :product :4; :product [ :square :3]; :product [ :square [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :product :4; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :2; :sum :6]]]; :sum [ :product :2; :product :2; :product [ :sum :0; :sum [ :minus :6]]]]]]]]]; :product [ :slash [ :product :2; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]]]]]; :product :3]; :sum [ :minus [ :product [ :product [ :sum [ :minus [ :product :2; :product :3; :product [ :sum :6; :sum [ :minus :2]]]]; :sum [ :sqrt [ :sum [ :product :4; :product [ :square :3]; :product [ :square [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :product :4; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :2; :sum :6]]]; :sum [ :product :2; :product :2; :product [ :sum :0; :sum [ :minus :6]]]]]]]]]; :product [ :slash [ :product :2; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]]]]; :product :6]]; :sum :0; :sum [ :product [ :product [ :sum [ :minus [ :product :2; :product :3; :product [ :sum :6; :sum [ :minus :2]]]]; :sum [ :sqrt [ :sum [ :product :4; :product [ :square :3]; :product [ :square [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :product :4; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :2; :sum :6]]]; :sum [ :product :2; :product :2; :product [ :sum :0; :sum [ :minus :6]]]]]]]]]; :product [ :slash [ :product :2; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]]]]; :product :2]]; :product [ :slash [ :sum [ :square [ :product [ :sum [ :minus [ :product :2; :product :3; :product [ :sum :6; :sum [ :minus :2]]]]; :sum [ :sqrt [ :sum [ :product :4; :product [ :square :3]; :product [ :square [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :product :4; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :2; :sum :6]]]; :sum [ :product :2; :product :2; :product [ :sum :0; :sum [ :minus :6]]]]]]]]]; :product [ :slash [ :product :2; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]]]]]; :sum :1]]]; :Y [ :product [ :sum [ :product [ :product [ :sum [ :minus [ :product :2; :product :3; :product [ :sum :6; :sum [ :minus :2]]]]; :sum [ :sqrt [ :sum [ :product :4; :product [ :square :3]; :product [ :square [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :product :4; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :2; :sum :6]]]; :sum [ :product :2; :product :2; :product [ :sum :0; :sum [ :minus :6]]]]]]]]]; :product [ :slash [ :product :2; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]]]]; :product :0]; :sum [ :product [ :square [ :product [ :sum [ :minus [ :product :2; :product :3; :product [ :sum :6; :sum [ :minus :2]]]]; :sum [ :sqrt [ :sum [ :product :4; :product [ :square :3]; :product [ :square [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :product :4; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :2; :sum :6]]]; :sum [ :product :2; :product :2; :product [ :sum :0; :sum [ :minus :6]]]]]]]]]; :product [ :slash [ :product :2; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]]]]]; :product :2]; :sum [ :minus [ :product [ :product [ :sum [ :minus [ :product :2; :product :3; :product [ :sum :6; :sum [ :minus :2]]]]; :sum [ :sqrt [ :sum [ :product :4; :product [ :square :3]; :product [ :square [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :product :4; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :2; :sum :6]]]; :sum [ :product :2; :product :2; :product [ :sum :0; :sum [ :minus :6]]]]]]]]]; :product [ :slash [ :product :2; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]]]]; :product :3]]; :sum :6]; :product [ :slash [ :sum [ :square [ :product [ :sum [ :minus [ :product :2; :product :3; :product [ :sum :6; :sum [ :minus :2]]]]; :sum [ :sqrt [ :sum [ :product :4; :product [ :square :3]; :product [ :square [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :product :4; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :2; :sum :6]]]; :sum [ :product :2; :product :2; :product [ :sum :0; :sum [ :minus :6]]]]]]]]]; :product [ :slash [ :product :2; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]]]]]; :sum :1]]]]}. {{[ :center [ :X :0; :Y :2]; :radius [ :product :2; :product [ :slash [ :sqrt :5]]]; :apoint [ :X :3; :Y :6]] } log:implies {[ :center [ :X :0; :Y :2]; :radius [ :product :2; :product [ :slash [ :sqrt :5]]]; :apoint [ :X :3; :Y :6]] :slope [ :product [ :sum [ :minus [ :product :2; :product :3; :product [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :sqrt [ :sum [ :product :4; :product [ :square :3]; :product [ :square [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :product :4; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :2; :sum :6]]]; :sum [ :product :2; :product :2; :product [ :sum :0; :sum [ :minus :6]]]]]]]]]]; :product [ :slash [ :product :2; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]]]]}} log:implies {[ :center [ :X :0; :Y :2]; :radius [ :product :2; :product [ :slash [ :sqrt :5]]]; :apoint [ :X :3; :Y :6]] :tpoint [ :X [ :product [ :sum [ :product [ :square [ :product [ :sum [ :minus [ :product :2; :product :3; :product [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :sqrt [ :sum [ :product :4; :product [ :square :3]; :product [ :square [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :product :4; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :2; :sum :6]]]; :sum [ :product :2; :product :2; :product [ :sum :0; :sum [ :minus :6]]]]]]]]]]; :product [ :slash [ :product :2; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]]]]]; :product :3]; :sum [ :minus [ :product [ :product [ :sum [ :minus [ :product :2; :product :3; :product [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :sqrt [ :sum [ :product :4; :product [ :square :3]; :product [ :square [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :product :4; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :2; :sum :6]]]; :sum [ :product :2; :product :2; :product [ :sum :0; :sum [ :minus :6]]]]]]]]]]; :product [ :slash [ :product :2; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]]]]; :product :6]]; :sum :0; :sum [ :product [ :product [ :sum [ :minus [ :product :2; :product :3; :product [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :sqrt [ :sum [ :product :4; :product [ :square :3]; :product [ :square [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :product :4; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :2; :sum :6]]]; :sum [ :product :2; :product :2; :product [ :sum :0; :sum [ :minus :6]]]]]]]]]]; :product [ :slash [ :product :2; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]]]]; :product :2]]; :product [ :slash [ :sum [ :square [ :product [ :sum [ :minus [ :product :2; :product :3; :product [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :sqrt [ :sum [ :product :4; :product [ :square :3]; :product [ :square [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :product :4; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :2; :sum :6]]]; :sum [ :product :2; :product :2; :product [ :sum :0; :sum [ :minus :6]]]]]]]]]]; :product [ :slash [ :product :2; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]]]]]; :sum :1]]]; :Y [ :product [ :sum [ :product [ :product [ :sum [ :minus [ :product :2; :product :3; :product [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :sqrt [ :sum [ :product :4; :product [ :square :3]; :product [ :square [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :product :4; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :2; :sum :6]]]; :sum [ :product :2; :product :2; :product [ :sum :0; :sum [ :minus :6]]]]]]]]]]; :product [ :slash [ :product :2; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]]]]; :product :0]; :sum [ :product [ :square [ :product [ :sum [ :minus [ :product :2; :product :3; :product [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :sqrt [ :sum [ :product :4; :product [ :square :3]; :product [ :square [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :product :4; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :2; :sum :6]]]; :sum [ :product :2; :product :2; :product [ :sum :0; :sum [ :minus :6]]]]]]]]]]; :product [ :slash [ :product :2; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]]]]]; :product :2]; :sum [ :minus [ :product [ :product [ :sum [ :minus [ :product :2; :product :3; :product [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :sqrt [ :sum [ :product :4; :product [ :square :3]; :product [ :square [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :product :4; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :2; :sum :6]]]; :sum [ :product :2; :product :2; :product [ :sum :0; :sum [ :minus :6]]]]]]]]]]; :product [ :slash [ :product :2; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]]]]; :product :3]]; :sum :6]; :product [ :slash [ :sum [ :square [ :product [ :sum [ :minus [ :product :2; :product :3; :product [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :sqrt [ :sum [ :product :4; :product [ :square :3]; :product [ :square [ :sum :6; :sum [ :minus :2]]]]; :sum [ :minus [ :product :4; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :2; :sum :6]]]; :sum [ :product :2; :product :2; :product [ :sum :0; :sum [ :minus :6]]]]]]]]]]; :product [ :slash [ :product :2; :product [ :sum [ :square [ :product :2; :product [ :slash [ :sqrt :5]]]]; :sum [ :minus [ :square [ :sum :0; :sum [ :minus :3]]]]]]]]]; :sum :1]]]]}. # Proof found for http://www.agfa.com/w3c/euler/tpoint-query.n3 in 287 steps (5315 steps/sec)