%------------------------------------------------------------------------------
% File     : CSR001+3 : TPTP v7.2.0. Released v3.1.0.
% Domain   : Commonsense Reasoning
% Axioms   : Supermarket trolley scenario for multiple trolleys
% Version  : [Mue05] axioms : Especial.
% English  :

% Refs     : [Mue05] Mueller (2005), Email to Geoff Sutcliffe
% Source   : [Mue05]
% Names    :

% Status   : Satisfiable
% Syntax   : Number of formulae    :    9 (   5 unit)
%            Number of atoms       :   40 (  28 equality)
%            Maximal formula depth :   15 (   7 average)
%            Number of connectives :   48 (  17 ~  ;   7  |;  20  &)
%                                         (   2 <=>;   2 =>;   0 <=)
%                                         (   0 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :    5 (   0 propositional; 2-3 arity)
%            Number of functors    :    5 (   0 constant; 1-2 arity)
%            Number of variables   :   26 (   0 singleton;  22 !;   4 ?)
%            Maximal term depth    :    2 (   1 average)
% SPC      : 

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

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

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

%----Distinct events
fof(push_not_pull,axiom,
    ( ! [Agent,Trolley] : push(Agent,Trolley) != pull(Agent,Trolley) )).

fof(push_unique,axiom,
    ( ! [Agent1,Agent2,Trolley1,Trolley2] :
        ( ( Agent1 != Agent2
          & Trolley1 != Trolley2 )
       => push(Agent1,Trolley1) != push(Agent2,Trolley2) ) )).

fof(pull_unique,axiom,
    ( ! [Agent1,Agent2,Trolley1,Trolley2] :
        ( ( Agent1 != Agent2
          & Trolley1 != Trolley2 )
       => pull(Agent1,Trolley1) != pull(Agent2,Trolley2) ) )).

%----Distinct fluents
fof(forwards_not_backwards,axiom,
    ( ! [Trolley] : forwards(Trolley) != backwards(Trolley) )).

fof(forwards_not_spinning,axiom,
    ( ! [Trolley] : forwards(Trolley) != spinning(Trolley) )).

fof(spinning_not_backwards,axiom,
    ( ! [Trolley] : spinning(Trolley) != backwards(Trolley) )).

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