#include <civlc.cvh>

/*
Path condition:
(0 < -1*(X10[1]*X10[3])+X10[1]*X10[5]+X10[2]*X10[3]+-1*(X10[2]*X10[4])+X10[4]*X10[0]+-1*(X10[5]*X10[0])+-1/115470000000000) && 
(0 != 11547/10000*(X10[1]*X10[3])+-11547/10000*(X10[1]*X10[5])+-11547/10000*(X10[2]*X10[3])+11547/10000*(X10[2]*X10[4])+-11547/10000*(X10[4]*X10[0])+11547/10000*(X10[5]*X10[0]))
*/
$input double x[6];

int main(){
  double a = 11547/10000 * (x[1]*x[3] - x[1]*x[5] - x[2]*x[3] + x[2]*x[4] - x[4]*x[0] + x[5]*x[0]);
  double b = -x[1]*x[3] + x[1]*x[5] + x[2]*x[3] - x[2]*x[4] + x[4]*x[0] - x[5]*x[0] - 1/115470000000000;

  $assume(0 < b);
  $assume(0 != a);
  $assert((a*a) != 0);
}