10:04:07	 From  Thomas Del Vecchio : Should be or?
10:05:47	 From  Jordan Hartzell : I’m confused about the goal
10:06:16	 From  Gene Siriviboon : Is it extremely slow since we use quantifier on binary relation?
10:08:02	 From  Thomas Del Vecchio : 5
10:08:36	 From  Thomas Del Vecchio : 2^(5^2)
10:08:40	 From  Jordan Hartzell : 25?
10:09:15	 From  Mia Santomauro : (2 to the 25) + 1
10:09:39	 From  Mia Santomauro : jk just 2^25
10:20:00	 From  Ryan Greenblatt : https://en.wikipedia.org/wiki/Thoralf_Skolem
10:22:25	 From  Jordan Hartzell : is it just the first thing that you found that satisfies ?
10:22:33	 From  Jordan Hartzell : $sg ^
10:25:33	 From  Danielle Rozenblit : How do we find sg?
10:26:39	 From  Thomas Del Vecchio : When you say it can do existential quantification, do you mean without being in the scope of nots?
10:26:56	 From  Thomas Del Vecchio : Darn
10:27:19	 From  Daniel Kostovetsky : More, a lot more
10:27:46	 From  Jordan Hartzell : can you repeat that please
10:31:28	 From  Monica Roy : What is symmetry breaking exactly?
10:32:01	 From  Ryan Greenblatt : Removing instances which are in some way symetric
10:32:19	 From  Monica Roy : ok!
10:32:22	 From  christopher : But when proving unsat isn’t E basically the same as FA?
10:37:41	 From  Justin Sanders : How many Cartesians are there for the run?
10:44:22	 From  Ryan Greenblatt : How slow should we expect this to be?
10:44:47	 From  Thomas Del Vecchio : Is the name related to CTL*?
10:44:55	 From  Thomas Del Vecchio : Fun