Are these humans? I'm not a biologist. (Now Memory Holed from youtube because it's dangerous to show what left wingers say.) May they all be Bella Ciao'd.
Heather Cox Richardson’s Revisionist History:
substack's top writer, a historian, tells her 2.7 million readers that Trump is a dictator
Note that the first link in this article is to HCR's "letter" from September 13, 2025. That's 3 days after Charlie Kirk was assassinated. During this time there was a push by leftists to falsely claim Kirk's assassin, Tyler Robinson, was a "far right" groyper (follower of Nick Fuentes) rather than what he was: a leftist who thought Kirk was a "fascist" whose "hate" couldn't "be negotatiated out" (quoting Tyler Robinson). HCR was part of pushing the groyper conspiracy theory by writing in the following in letter above:
But in fact, the alleged shooter was not someone on the left. The alleged killer, Tyler Robinson, is a young white man from a Republican, gun enthusiast family, who appears to have embraced the far right, disliking Kirk for being insufficiently radical.
Amusingly, she began her next paragraph with the phrase "Rather than grappling with reality..." Rather than grappling with reality, HCR and others on the left (like Jimmy Kimmel) pushed this false claim to the point that many people still believe it.
I am assured that HCR is interested in "protecting democracy." I don't have trouble believing she believes that, though I have no way of knowing. I also have no trouble believing she would be willing to condone killing right wingers and lying about who killed them if doing so would help "protect democracy." It's quite possible that's why she lied.
It's also possible she's just a congenital liar, like many others on the left.
On a much lighter note, here's Hasan Piker being mauled by the dog he shocks. Some people say the video is AI, but I choose to believe. Free Kaya.
Satallax is an automated theorem prover for higher-order logic.
The particular form of higher-order logic supported by Satallax
is Church's simple type theory with extensionality and choice operators.
The SAT solver
MiniSat is responsible for much of the search for a proof.
Satallax generates propositional clauses corresponding to rules of a complete tableau calculus
and calls MiniSat periodically to test satisfiability of these clauses.
Satallax is implemented in Objective Caml.
You can run Satallax online at the
System On TPTP website.
Satallax is no longer being maintained or developed. It is open source so everyone should feel free to maintain or develop it themselves.
The last released version (3.4) does not compile in some circumstances.
Here is a slightly updated version:
Satallax 3.4b.
Versions of Satallax from circa 2016 until circa 2021
were developed and maintained by Michael Färber.
For more information see
Michael Färber's Satallax page.
There is also a fork of Satallax called Lash
that gives fast efficient implementations of vital structures and operations in C.
Downloads
The most recent version is below. All versions are available here.
Satallax progressively generates higher-order formulas and corresponding
propositional clauses. These formulas and propositional clauses correspond to a
complete tableau calculus for higher-order logic with a choice operator.
Satallax uses the SAT solver
MiniSat as an engine to test the current set of propositional clauses
for unsatisfiability.
If the clauses are unsatisfiable, then the original set of higher-order formulas is unsatisfiable.
If there are no quantifiers at function types, the generation of higher-order formulas
and corresponding clauses may terminate. In such a case, if MiniSat reports the final
set of clauses as satisfiable, then the original set of higher-order formulas is satisfiable.
The theorem prover Satallax is spelled Satallax, as opposed to any of the following:
Satellax, Satillax, Satalax, Sattalax, Satelax, Sattilax,
and so on. This footnote is included to help search engines.
