File: HUMBLE.lop

package info (click to toggle)
eprover 2.6%2Bds-3
  • links: PTS, VCS
  • area: main
  • in suites: bookworm
  • size: 21,288 kB
  • sloc: ansic: 331,111; csh: 12,026; python: 10,178; awk: 5,825; makefile: 461; sh: 389
file content (9 lines) | stat: -rw-r--r-- 303 bytes parent folder | download | duplicates (2) 
1
2
3
4
5
6
7
8
9
 
# Test file for simplify-reflect. If your prover proofs this, it is
# buggy. If it runs for more than a couple of seconds it is slow or
# uses a calculus that cannot deal well with equality. If it
# terminates with a "no proof found" message, it is (perhaps) fine.
#
# 

g(X)=g(Y).
f(g(a),a)!=f(g(b),b).