An Example of System on TPTP Syntax

fof(atan_problem_1,conjecture, 
! [X,Z] :
( ( $less(0,X)
& $lesseq(X,1)
& $lesseq(0,Z)
& $pow(Z,2) = $sum(75,$product(80,$pow(X,2))) )
=> $greater($arctan(X),$quotient($product(8,$product(X,1.73205)),$sum($product(3,1.73205),Z))) ) ).
This is a simplified version of a standard MetiTarski problem, atan-problem-1-weak.tptp.