%--------------------------------------------------------------------------
% File     : PLA012-1 : TPTP v2.1.0. Released v1.1.0.
% Domain   : Planning (Blocks world)
% Problem  : Block D on B on C
% Version  : [SE94] axioms.
% English  : 

% Refs     : [Sus73] Sussman (1973), A Computational Model of Skill Acquisi
%          : [SE94]  Segre & Elkan (1994), A High-Performance Explanation-B
% Source   : [SE94]
% Names    : - [SE94]

% Status   : unsatisfiable
% Rating   : 0.78 v2.1.0, 0.71 v2.0.0
% Syntax   : Number of clauses    :   31 (   0 non-Horn;  20 unit;  28 RR)
%            Number of literals   :   53 (   0 equality)
%            Maximal clause size  :    4 (   1 average)
%            Number of predicates :    2 (   0 propositional; 2-2 arity)
%            Number of functors   :   14 (   7 constant; 0-2 arity)
%            Number of variables  :   37 (   5 singleton)
%            Maximal term depth   :    3 (   1 average)

% Comments : The axioms are a reconstruction of the situation calculus 
%            blocks world as in [Sus73].
%          : tptp2X -f tptp -t rm_equality:rstfp PLA012-1.p 
%--------------------------------------------------------------------------
input_clause(and_definition,axiom,
    [++ holds(and(X, Y), State),
     -- holds(X, State),
     -- holds(Y, State)]).

input_clause(pickup_1,axiom,
    [++ holds(holding(X), do(pickup(X), State)),
     -- holds(empty, State),
     -- holds(clear(X), State),
     -- differ(X, table)]).

input_clause(pickup_2,axiom,
    [++ holds(clear(Y), do(pickup(X), State)),
     -- holds(on(X, Y), State),
     -- holds(clear(X), State),
     -- holds(empty, State)]).

input_clause(pickup_3,axiom,
    [++ holds(on(X, Y), do(pickup(Z), State)),
     -- holds(on(X, Y), State),
     -- differ(X, Z)]).

input_clause(pickup_4,axiom,
    [++ holds(clear(X), do(pickup(Z), State)),
     -- holds(clear(X), State),
     -- differ(X, Z)]).

input_clause(putdown_1,axiom,
    [++ holds(empty, do(putdown(X, Y), State)),
     -- holds(holding(X), State),
     -- holds(clear(Y), State)]).

input_clause(putdown_2,axiom,
    [++ holds(on(X, Y), do(putdown(X, Y), State)),
     -- holds(holding(X), State),
     -- holds(clear(Y), State)]).

input_clause(putdown_3,axiom,
    [++ holds(clear(X), do(putdown(X, Y), State)),
     -- holds(holding(X), State),
     -- holds(clear(Y), State)]).

input_clause(putdown_4,axiom,
    [++ holds(on(X, Y), do(putdown(Z, W), State)),
     -- holds(on(X, Y), State)]).

input_clause(putdown_5,axiom,
    [++ holds(clear(Z), do(putdown(X, Y), State)),
     -- holds(clear(Z), State),
     -- differ(Z, Y)]).

input_clause(symmetry_of_differ,axiom,
    [++ differ(X, Y),
     -- differ(Y, X)]).

input_clause(differ_a_b,axiom,
    [++ differ(a, b)]).

input_clause(differ_a_c,axiom,
    [++ differ(a, c)]).

input_clause(differ_a_d,axiom,
    [++ differ(a, d)]).

input_clause(differ_a_table,axiom,
    [++ differ(a, table)]).

input_clause(differ_b_c,axiom,
    [++ differ(b, c)]).

input_clause(differ_b_d,axiom,
    [++ differ(b, d)]).

input_clause(differ_b_table,axiom,
    [++ differ(b, table)]).

input_clause(differ_c_d,axiom,
    [++ differ(c, d)]).

input_clause(differ_c_table,axiom,
    [++ differ(c, table)]).

input_clause(differ_d_table,axiom,
    [++ differ(d, table)]).

input_clause(initial_state1,axiom,
    [++ holds(on(a, table), s0)]).

input_clause(initial_state2,axiom,
    [++ holds(on(b, table), s0)]).

input_clause(initial_state3,axiom,
    [++ holds(on(c, d), s0)]).

input_clause(initial_state4,axiom,
    [++ holds(on(d, table), s0)]).

input_clause(initial_state5,axiom,
    [++ holds(clear(a), s0)]).

input_clause(initial_state6,axiom,
    [++ holds(clear(b), s0)]).

input_clause(initial_state7,axiom,
    [++ holds(clear(c), s0)]).

input_clause(initial_state8,axiom,
    [++ holds(empty, s0)]).

input_clause(clear_table,axiom,
    [++ holds(clear(table), State)]).

input_clause(prove_DBC,conjecture,
    [-- holds(and(on(d, b), on(b, c)), State)]).
%--------------------------------------------------------------------------