As far as I can tell, it mostly ignored the constraint (it came up with encodings for 1 and "true" in terms of S and K, but its "if" and "false" are the usual)

As far as I can tell, it mostly ignored the constraint (it came up with encodings for 1 and "true" in terms of S and K, but its "if" and "false" are the usual) and copy-pasted an existing lambda-calculus implementation.