SHARE
TWEET

Untitled

a guest May 19th, 2017 46 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. fof(at_least_four, axiom, ? [A,B,C,D] : ((A != B) & (A != C) & (B != C) & (B != D) & (C != D) & (D != A))).
  2.  
  3. fof (zero, axiom, ! [X] :
  4.     (zero (X) <=> ~one(X))
  5. ).
  6.  
  7. fof (one, axiom, ! [X] :
  8.     (one (X) <=> ~zero (X))
  9. ).
  10.  
  11. fof (less, axiom, ! [X,Y,Z] : (
  12.     ( ~less(X,X) => ( (less(X,Y) & less (Y,Z)) => less(X,Z))))).
  13.    
  14. fof(is_binary, axiom, ! [X] : (zero(X) | one(X))).
  15.  
  16. fof (four_binaries, axiom, ? [W,X,Y,Z] : (
  17.     (is_binary (W) & is_binary (X) & is_binary(Y) & is_binary(Z))) &
  18.     (less (W,X) | less (X,Y) | less(Y,Z) | less(W,Y) | less (X,Z) | less (Z,W)) ).
RAW Paste Data
Top