%
%  
%  (in one big formula to make it easier to negate and such)
%
set(auto).
clear(control_memory).
assign(max_seconds, 31000000).
assign(max_mem, 500000).

formula_list(usable).

%
%   Assertion of Reified Sentences via Truth Predicate
%
(all S X Y Z (
  rdf(S, rdf_type, lx_TrueSentence) &
  rdf(S, lx_subject, X) &
  rdf(S, lx_predicate, Y) &
  rdf(S, lx_object, Z)
  ->
  rdf(X, Y, Z)
)) &

(all S X Y Z (
  rdf(S, rdf_type, lx_FalseSentence) &
  rdf(S, lx_subject, X) &
  rdf(S, lx_predicate, Y) &
  rdf(S, lx_object, Z)
  ->
  -rdf(X, Y, Z)
)) &

%
%   Reified Sentences have Truths matching their RDF truths
%

(all S X Y Z (
  rdf(S, lx_subject, X) &
  rdf(S, lx_predicate, Y) &
  rdf(S, lx_object, Z) &
  rdf(X, Y, Z)
  ->
  rdf(S, rdf_type, lx_TrueSentence)
)) &

(all S X Y Z (
  rdf(S, lx_subject, X) &
  rdf(S, lx_predicate, Y) &
  rdf(S, lx_object, Z) &
  -rdf(X, Y, Z)
  ->
  rdf(S, rdf_type, lx_FalseSentence)
)) &

%
%   Every three things can be combined into a sentence, which is
%   either true or false
%

(all X Y Z (
  (exists S (
    rdf(S, lx_subject, X) &
    rdf(S, lx_predicate, Y) &
    rdf(S, lx_object, Z) &
    ( rdf(S, rdf_type, lx_TrueSentence) 
      |
      rdf(S, rdf_type, lx_FalseSentence) 
    )
  ))
)) &

%
%   The sentence of 3 things is unique
%

(all X Y Z S1 S2 (
  rdf(S1, lx_subject, X) &
  rdf(S1, lx_predicate, Y) &
  rdf(S1, lx_object, Z) &
  rdf(S2, lx_subject, X) &
  rdf(S2, lx_predicate, Y) &
  rdf(S2, lx_object, Z)
  ->
  % we could say they are equal
  S1 = S2 &  
  % or we could say neither is higher than the other
  -higher(S1, S2) &   
  -higher(S2, S1)
  % ... or both!
)) &

%
%   Stratify sentences; loops are not possible.
%

(all S P (
  rdf(S, lx_subject, P) 
  ->  
  higher(S, P)
)) &

(all S P (
  rdf(S, lx_predicate, P) 
  ->  
  higher(S, P)
)) &

(all S P (
  rdf(S, lx_object, P) 
  ->  
  higher(S, P)
)) &

(all S1 S2 (
  higher(S1, S2) -> -higher(S2, S1)
)) &

(all S1 S2 S3 (
  higher(S1, S2) &
  higher(S2, S3) 
  -> 
  higher(S1, S3)
)) 

.