CSR001+2.ax

%------------------------------------------------------------------------------
% File     : CSR001+2 : TPTP v7.2.0. Released v3.1.0.
% Domain   : Commonsense Reasoning
% Axioms   : Supermarket trolley scenario
% Version  : [Sha97] axioms : Especial.
% English  :

% Refs     : [Sha97] Shanahan (1997), Solving the Frame Problem
% Source   : [Sha97]
% Names    :

% Status   : Satisfiable
% Syntax   : Number of formulae    :    8 (   5 unit)
%            Number of atoms       :   43 (  30 equality)
%            Maximal formula depth :   13 (   6 average)
%            Number of connectives :   46 (  11 ~  ;  10  |;  22  &)
%                                         (   3 <=>;   0 =>;   0 <=)
%                                         (   0 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :    5 (   0 propositional; 2-3 arity)
%            Number of functors    :    8 (   8 constant; 0-0 arity)
%            Number of variables   :   11 (   0 singleton;  11 !;   0 ?)
%            Maximal term depth    :    1 (   1 average)
% SPC      : 

% Comments : Requires CSR001+0.ax
%------------------------------------------------------------------------------
fof(initiates_all_defn,axiom,
    ( ! [Event,Fluent,Time] :
        ( initiates(Event,Fluent,Time)
      <=> ( ( Event = push
            & Fluent = forwards
            & ~ happens(pull,Time) )
          | ( Event = pull
            & Fluent = backwards
            & ~ happens(push,Time) )
          | ( Event = pull
            & Fluent = spinning
            & happens(push,Time) ) ) ) )).

fof(terminates_all_defn,axiom,
    ( ! [Event,Fluent,Time] :
        ( terminates(Event,Fluent,Time)
      <=> ( ( Event = push
            & Fluent = backwards
            & ~ happens(pull,Time) )
          | ( Event = pull
            & Fluent = forwards
            & ~ happens(push,Time) )
          | ( Event = pull
            & Fluent = forwards
            & happens(push,Time) )
          | ( Event = pull
            & Fluent = backwards
            & happens(push,Time) )
          | ( Event = push
            & Fluent = spinning
            & ~ happens(pull,Time) )
          | ( Event = pull
            & Fluent = spinning
            & ~ happens(push,Time) ) ) ) )).

fof(releases_all_defn,axiom,
    ( ! [Event,Fluent,Time] : ~ releases(Event,Fluent,Time) )).

fof(happens_all_defn,axiom,
    ( ! [Event,Time] :
        ( happens(Event,Time)
      <=> ( ( Event = push
            & Time = n0 )
          | ( Event = pull
            & Time = n1 )
          | ( Event = pull
            & Time = n2 )
          | ( Event = push
            & Time = n2 ) ) ) )).

%----Distinct events
fof(push_not_pull,axiom,
    (  push != pull )).

%----Distinct fluents
fof(forwards_not_backwards,axiom,
    (  forwards != backwards )).

fof(forwards_not_spinning,axiom,
    (  forwards != spinning )).

fof(spinning_not_backwards,axiom,
    (  spinning != backwards )).

%------------------------------------------------------------------------------