%------------------------------------------------------------------------------
% File     : CSR001+0 : TPTP v7.2.0. Released v3.1.0.
% Domain   : Commonsense Reasoning
% Axioms   : Standard discrete event calculus axioms
% Version  : [Mue04] axioms : Especial.
% English  :

% Refs     : [Mue04] Mueller (2004), A Tool for Satisfiability-based Common
%          : [MS02]  Miller & Shanahan (2002), Some Alternative Formulation
% Source   : [Mue04]
% Names    :

% Status   : Satisfiable
% Syntax   : Number of formulae    :   12 (   0 unit)
%            Number of atoms       :   54 (   0 equality)
%            Maximal formula depth :   12 (   9 average)
%            Number of connectives :   56 (  14 ~  ;   2  |;  28  &)
%                                         (   2 <=>;  10 =>;   0 <=)
%                                         (   0 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :   11 (   0 propositional; 2-4 arity)
%            Number of functors    :    3 (   2 constant; 0-2 arity)
%            Number of variables   :   44 (   0 singleton;  36 !;   8 ?)
%            Maximal term depth    :    2 (   1 average)
% SPC      : 

% Comments :
%------------------------------------------------------------------------------
%----DEC1
fof(stoppedin_defn,axiom,
    ( ! [Time1,Fluent,Time2] :
        ( stoppedIn(Time1,Fluent,Time2)
      <=> ? [Event,Time] :
            ( happens(Event,Time)
            & less(Time1,Time)
            & less(Time,Time2)
            & terminates(Event,Fluent,Time) ) ) )).

%----DEC2
fof(startedin_defn,axiom,
    ( ! [Time1,Time2,Fluent] :
        ( startedIn(Time1,Fluent,Time2)
      <=> ? [Event,Time] :
            ( happens(Event,Time)
            & less(Time1,Time)
            & less(Time,Time2)
            & initiates(Event,Fluent,Time) ) ) )).

%----DEC3
fof(change_holding,axiom,
    ( ! [Event,Time,Fluent,Fluent2,Offset] :
        ( ( happens(Event,Time)
          & initiates(Event,Fluent,Time)
          & less(n0,Offset)
          & trajectory(Fluent,Time,Fluent2,Offset)
          & ~ stoppedIn(Time,Fluent,plus(Time,Offset)) )
       => holdsAt(Fluent2,plus(Time,Offset)) ) )).

%----DEC4
fof(antitrajectory,axiom,
    ( ! [Event,Time1,Fluent1,Time2,Fluent2] :
        ( ( happens(Event,Time1)
          & terminates(Event,Fluent1,Time1)
          & less(n0,Time2)
          & antitrajectory(Fluent1,Time1,Fluent2,Time2)
          & ~ startedIn(Time1,Fluent1,plus(Time1,Time2)) )
       => holdsAt(Fluent2,plus(Time1,Time2)) ) )).

%----DEC5
fof(keep_holding,axiom,
    ( ! [Fluent,Time] :
        ( ( holdsAt(Fluent,Time)
          & ~ releasedAt(Fluent,plus(Time,n1))
          & ~ ( ? [Event] :
                  ( happens(Event,Time)
                  & terminates(Event,Fluent,Time) ) ) )
       => holdsAt(Fluent,plus(Time,n1)) ) )).

%----DEC6
fof(keep_not_holding,axiom,
    ( ! [Fluent,Time] :
        ( ( ~ holdsAt(Fluent,Time)
          & ~ releasedAt(Fluent,plus(Time,n1))
          & ~ ( ? [Event] :
                  ( happens(Event,Time)
                  & initiates(Event,Fluent,Time) ) ) )
       => ~ holdsAt(Fluent,plus(Time,n1)) ) )).

%----DEC7
fof(keep_released,axiom,
    ( ! [Fluent,Time] :
        ( ( releasedAt(Fluent,Time)
          & ~ ( ? [Event] :
                  ( happens(Event,Time)
                  & ( initiates(Event,Fluent,Time)
                    | terminates(Event,Fluent,Time) ) ) ) )
       => releasedAt(Fluent,plus(Time,n1)) ) )).

%----DEC8
fof(keep_not_released,axiom,
    ( ! [Fluent,Time] :
        ( ( ~ releasedAt(Fluent,Time)
          & ~ ( ? [Event] :
                  ( happens(Event,Time)
                  & releases(Event,Fluent,Time) ) ) )
       => ~ releasedAt(Fluent,plus(Time,n1)) ) )).

%----DEC9
fof(happens_holds,axiom,
    ( ! [Event,Time,Fluent] :
        ( ( happens(Event,Time)
          & initiates(Event,Fluent,Time) )
       => holdsAt(Fluent,plus(Time,n1)) ) )).

%----DEC10
fof(happens_terminates_not_holds,axiom,
    ( ! [Event,Time,Fluent] :
        ( ( happens(Event,Time)
          & terminates(Event,Fluent,Time) )
       => ~ holdsAt(Fluent,plus(Time,n1)) ) )).

%----DEC11
fof(happens_releases,axiom,
    ( ! [Event,Time,Fluent] :
        ( ( happens(Event,Time)
          & releases(Event,Fluent,Time) )
       => releasedAt(Fluent,plus(Time,n1)) ) )).

%----DEC12
fof(happens_not_released,axiom,
    ( ! [Event,Time,Fluent] :
        ( ( happens(Event,Time)
          & ( initiates(Event,Fluent,Time)
            | terminates(Event,Fluent,Time) ) )
       => ~ releasedAt(Fluent,plus(Time,n1)) ) )).

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