(vect3Dnil 3322906695"" (skolem 1 ("u" "v" ))"" (expand "eq3D?" )"" (ground)"" (decompose-equality 1)"" (name-replace "X" "x!1" )"" (typepred "X" )"" (case "X=0 OR X=1 OR X=2" )"1" (split -1)"1" (replace -1) (("1" (propax) nil nil )) nil )"2" (replace -1) (("2" (propax) nil nil )) nil )"3" (replace -1) (("3" (propax) nil nil )) nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" vect3D nil )nil vect3D nil )nil vectors nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil ))nil )nil 3322906656 ("" (postpone) nil nil ) nil shostak))nil 3322906660 ("" (grind) nil nil )"Vect3" vect3D nil )) shostak))nil 3322906664 ("" (grind) nil nil )"Vect3" vect3D nil )) shostak))nil 3322906667 ("" (grind) nil nil )"Vect3" vect3D nil )) shostak)))quality 94%
¤ Dauer der Verarbeitung: 0.21 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
