More complex blocks world axiomatization

%--------------------------------------------------------------------------
% File     : PLA001-0 : TPTP v7.2.0. Released v1.0.0.
% Domain   : Planning (Blocks world)
% Axioms   : Blocks world axioms
%--------------------------------------------------------------------------

cnf(and_definition,axiom,
    ( holds(and(X,Y),State)
    | ~ holds(X,State)
    | ~ holds(Y,State) )).

cnf(pickup_1,axiom,
    ( holds(holding(X),do(pickup(X),State))
    | ~ holds(empty,State)
    | ~ holds(clear(X),State)
    | ~ differ(X,table) )).

cnf(pickup_2,axiom,
    ( holds(clear(Y),do(pickup(X),State))
    | ~ holds(on(X,Y),State)
    | ~ holds(clear(X),State)
    | ~ holds(empty,State) )).

cnf(pickup_3,axiom,
    ( holds(on(X,Y),do(pickup(Z),State))
    | ~ holds(on(X,Y),State)
    | ~ differ(X,Z) )).

cnf(pickup_4,axiom,
    ( holds(clear(X),do(pickup(Z),State))
    | ~ holds(clear(X),State)
    | ~ differ(X,Z) )).

cnf(putdown_1,axiom,
    ( holds(empty,do(putdown(X,Y),State))
    | ~ holds(holding(X),State)
    | ~ holds(clear(Y),State) )).

cnf(putdown_2,axiom,
    ( holds(on(X,Y),do(putdown(X,Y),State))
    | ~ holds(holding(X),State)
    | ~ holds(clear(Y),State) )).

cnf(putdown_3,axiom,
    ( holds(clear(X),do(putdown(X,Y),State))
    | ~ holds(holding(X),State)
    | ~ holds(clear(Y),State) )).

cnf(putdown_4,axiom,
    ( holds(on(X,Y),do(putdown(Z,W),State))
    | ~ holds(on(X,Y),State) )).

cnf(putdown_5,axiom,
    ( holds(clear(Z),do(putdown(X,Y),State))
    | ~ holds(clear(Z),State)
    | ~ differ(Z,Y) )).
    
%--------------------------------------------------------------------------
% File     : PLA001-1 : TPTP v7.2.0. Released v1.0.0.
% Domain   : Planning (Blocks world)
% Axioms   : Blocks world difference axioms for 4 blocks
%--------------------------------------------------------------------------

cnf(symmetry_of_differ,axiom,
    ( differ(X,Y)
    | ~ differ(Y,X) )).

cnf(differ_a_b,axiom,
    ( differ(a,b) )).

cnf(differ_a_c,axiom,
    ( differ(a,c) )).

cnf(differ_a_d,axiom,
    ( differ(a,d) )).

cnf(differ_a_table,axiom,
    ( differ(a,table) )).

cnf(differ_b_c,axiom,
    ( differ(b,c) )).

cnf(differ_b_d,axiom,
    ( differ(b,d) )).

cnf(differ_b_table,axiom,
    ( differ(b,table) )).

cnf(differ_c_d,axiom,
    ( differ(c,d) )).

cnf(differ_c_table,axiom,
    ( differ(c,table) )).

cnf(differ_d_table,axiom,
    ( differ(d,table) )).

%----Initial configuration:
%
%         c
%    a    b    d   
%  -------------------------------

cnf(initial_state1,axiom,
    ( holds(on(a,table),s0) )).

cnf(initial_state2,axiom,
    ( holds(on(b,table),s0) )).

cnf(initial_state3,axiom,
    ( holds(on(c,d),s0) )).

cnf(initial_state4,axiom,
    ( holds(on(d,table),s0) )).

cnf(initial_state5,axiom,
    ( holds(clear(a),s0) )).

cnf(initial_state6,axiom,
    ( holds(clear(b),s0) )).

cnf(initial_state7,axiom,
    ( holds(clear(c),s0) )).

cnf(initial_state8,axiom,
    ( holds(empty,s0) )).

%----Table is always clear

cnf(clear_table,axiom,
    ( holds(clear(table),State) )).
  
%--------------------------------------------------------------------------
% 
% questions:
%
% the second etc are commented out: try also these (remember to outcomment others)
%
%
%
% -----------------------------------------------------------------------

 %cnf(prove_DA,negated_conjecture,
 %  ( ~ holds(on(d,a),State) )).
   
 cnf(prove_DA,negated_conjecture,
   ( ~ holds(on(d,a),State) | $ans(State))).   


% this one asks to construct this tower (which could be on table or on top of other blocks):
%
%         c 
%         b 
%         a    
%
% proving this will take ca 8 secs, during which a prover tries out several search strategies sequentially 


% cnf(prove_CBA,negated_conjecture,
%    ( ~ holds(and(on(c,b),on(b,a)),State) )).
    
    
% this one asks to construct these towers (but, they could be also on top of each other!):
%
%         c   d 
%         a   b 
    
    
    
% cnf(prove_CA_DB,negated_conjecture,
%    ( ~ holds(and(on(c,a),on(d,b)),State) )).
    
    
% this one asks to construct
%
%    d
%    c

% cnf(prove_DC,negated_conjecture,
%  ( ~ holds(on(d,c),State) )).