#--------------------------------------------------------------------------
# File     : PLA002-2 : TPTP v2.2.0. Released v1.0.0.
# Domain   : Planning
# Problem  : Getting from here to there, in all weather
# Version  : Especial.
#            Theorem formulation : Augmented.
# English  : 

# Refs     : [Pla82] Plaisted (1982), A Simplified Problem Reduction Format
# Source   : [TPTP]
# Names    : 

# Status   : unsatisfiable
# Rating   : 0.25 v2.1.0, 0.50 v2.0.0
# Syntax   : Number of clauses    :   23 (   1 non-Horn;   2 unit;  18 RR)
#            Number of literals   :   64 (   0 equality)
#            Maximal clause size  :    4 (   2 average)
#            Number of predicates :    4 (   0 propositional; 1-2 arity)
#            Number of functors   :   12 (   7 constant; 0-2 arity)
#            Number of variables  :   27 (   5 singleton)
#            Maximal term depth   :    2 (   1 average)

# Comments : Includes sort information in the clauses. Inspired by the 
#            problems of building a model if there is no sort info. in the 
#            clauses. In this case the natural interpretation is not a 
#            model of the hypotheses, as meaningless (FALSE) instances of 
#            clauses can be made.
#          : Modified by Geoff Sutcliffe.
#          : tptp2X -f setheo:sign -t rm_equality:rstfp PLA002-2.p 
#--------------------------------------------------------------------------
# warm_or_cold, hypothesis.
warm(Situation1);
cold(Situation2) <- 
    situation(Situation1),
    situation(Situation2).

# walk_a_to_b, hypothesis.
at(b, walk(b, Situation)) <- 
    at(a, Situation),
    situation(Situation).

# drive_a_to_b, hypothesis.
at(b, drive(b, Situation)) <- 
    at(a, Situation),
    situation(Situation).

# walk_b_to_a, hypothesis.
at(a, walk(a, Situation)) <- 
    at(b, Situation),
    situation(Situation).

# drive_b_to_a, hypothesis.
at(a, drive(a, Situation)) <- 
    at(b, Situation),
    situation(Situation).

# cross_river_b_to_c, hypothesis.
at(c, skate(c, Situation)) <- 
    cold(Situation),
    at(b, Situation),
    situation(Situation).

# cross_river_c_to_b, hypothesis.
at(b, skate(b, Situation)) <- 
    cold(Situation),
    at(c, Situation),
    situation(Situation).

# climb_mountain_b_to_d, hypothesis.
at(d, climb(d, Situation)) <- 
    warm(Situation),
    at(b, Situation),
    situation(Situation).

# climb_mountain_d_to_b, hypothesis.
at(b, climb(b, Situation)) <- 
    warm(Situation),
    at(d, Situation),
    situation(Situation).

# go_c_to_d, hypothesis.
at(d, go(d, Situation)) <- 
    at(c, Situation),
    situation(Situation).

# go_d_to_c, hypothesis.
at(c, go(c, Situation)) <- 
    at(d, Situation),
    situation(Situation).

# go_c_to_e, hypothesis.
at(e, go(e, Situation)) <- 
    at(c, Situation),
    situation(Situation).

# go_e_to_c, hypothesis.
at(c, go(c, Situation)) <- 
    at(e, Situation),
    situation(Situation).

# go_d_to_f, hypothesis.
at(f, go(f, Situation)) <- 
    at(d, Situation),
    situation(Situation).

# go_f_to_d, hypothesis.
at(d, go(d, Situation)) <- 
    at(f, Situation),
    situation(Situation).

# initial_situation, hypothesis.
situation(s0) <- .

# walk_situation, hypothesis.
situation(walk(Somewhere, Situation)) <- 
    situation(Situation).

# drive_situation, hypothesis.
situation(drive(Somewhere, Situation)) <- 
    situation(Situation).

# climb_situation, hypothesis.
situation(climb(Somewhere, Situation)) <- 
    situation(Situation).

# skate_situation, hypothesis.
situation(skate(Somewhere, Situation)) <- 
    situation(Situation).

# go_situation, hypothesis.
situation(go(Somewhere, Situation)) <- 
    situation(Situation).

# initial, hypothesis.
at(f, s0) <- .

# prove_you_can_get_to_a_in_a_situation, conjecture.
 <- at(a, S),
    situation(S).

#--------------------------------------------------------------------------