%-------------------------------------------------------------------------- % File : PLA002+0 : TPTP v7.2.0. Released v2.4.0. % Domain : Planning (Blocks world) % Axioms : Blocks world axioms % Version : [Bau99] axioms. % English : % Refs : [Bau99] Baumgartner (1999), FTP'2000 - Problem Sets % [KS96] Kautz & Selman (1996), Pushing the Envelope: Planning, % [KS92] Kautz & Selman (1992), Planning as Satisfiability % Source : [Bau99] % Names : % Status : Satisfiable % Syntax : Number of formulae : 24 ( 0 unit) % Number of atoms : 119 ( 0 equality) % Maximal formula depth : 10 ( 8 average) % Number of connectives : 120 ( 25 ~ ; 0 |; 43 &) % ( 0 <=>; 52 =>; 0 <=) % ( 0 <~>; 0 ~|; 0 ~&) % Number of predicates : 10 ( 0 propositional; 1-3 arity) % Number of functors : 1 ( 0 constant; 1-1 arity) % Number of variables : 64 ( 0 singleton; 64 !; 0 ?) % Maximal term depth : 2 ( 1 average) % SPC : % Comments : %-------------------------------------------------------------------------- % blocks_axioms: fof(place_object_block_on_destination,axiom, ( ! [I,X] : ( nonfixed(X) => ! [Z] : ( ( a_block(Z) & neq(X,Z) ) => ( ( time(I) & object(X,I) & destination(Z,I) ) => on(X,Z,s(I)) ) ) ) )). % All( x, block, ! member( x, fixed), % All( y, block, ! eql( x, y), % Disj( % Not( L2("object", x, i)); % Not( L2("source", y, i)); % Not( L3("on", x, y, 1 + i))))); fof(remove_object_block_from_source,axiom, ( ! [I,X] : ( nonfixed(X) => ! [Y] : ( ( a_block(Y) & neq(X,Y) ) => ( ( time(I) & object(X,I) & source(Y,I) ) => ~ on(X,Y,s(I)) ) ) ) )). % All( y, block, ! member( y, fixed), % Disj( % Not( L2("source", y, i)); % L2("clear", y, 1 + i); % )); fof(clear_source_after_removal,axiom, ( ! [I,Y] : ( nonfixed(Y) => ( ( time(I) & source(Y,I) ) => clear(Y,s(I)) ) ) )). % All( z, block, ! member( z, fixed), % Disj( % Not( L2("destination", z, i)); % Not( L2("clear", z, 1 + i)))); fof(not_clear_destination_after_placement,axiom, ( ! [I,Z] : ( nonfixed(Z) => ( ( time(I) & destination(Z,I) ) => ~ clear(Z,s(I)) ) ) )). fof(object_block_on_source,axiom, ( ! [I,X] : ( nonfixed(X) => ! [Y] : ( ( a_block(Y) & neq(X,Y) ) => ( ( object(X,I) & source(Y,I) ) => on(X,Y,I) ) ) ) )). % All( x, block, ! member( x, fixed), % Disj( % Not( L2("object", x, i)); % L2("clear", x, i))); fof(object_block_is_clear,axiom, ( ! [I,X] : ( nonfixed(X) => ( object(X,I) => clear(X,I) ) ) )). % All( z, block, ! member( z, fixed), % Disj( % Not( L2("destination", z, i)); % L2("clear", z, i))); fof(destination_block_is_clear,axiom, ( ! [I,Z] : ( nonfixed(Z) => ( destination(Z,I) => clear(Z,I) ) ) )). fof(non_destination_remains_clear,axiom, ( ! [I,W] : ( nonfixed(W) => ( ( time(I) & ~ destination(W,I) & clear(W,I) ) => clear(W,s(I)) ) ) )). % All( v, block, ! member( v, fixed), % All( w, block, !eql( v, w), % Disj( % L2("object", v, i); % Not( L3("on", v, w, i)) ; % L3("on", v, w, 1 + i)))); fof(non_object_remains_on,axiom, ( ! [I,V] : ( nonfixed(V) => ! [W] : ( ( a_block(W) & neq(V,W) ) => ( ( time(I) & ~ object(V,I) & on(V,W,I) ) => on(V,W,s(I)) ) ) ) )). fof(non_source_remains_not_clear,axiom, ( ! [I,W] : ( nonfixed(W) => ( ( time(I) & ~ source(W,I) & ~ clear(W,I) ) => ~ clear(W,s(I)) ) ) )). % All( v, block, ! member( v, fixed), % All( w, block, ! eql( v, w), % Disj( % L2("object", v, i); % L3("on", v, w, i) ; % Not( L3("on", v, w, 1 + i))))); fof(non_object_remains_not_on,axiom, ( ! [I,V] : ( nonfixed(V) => ! [W] : ( ( a_block(W) & neq(V,W) ) => ( ( time(I) & ~ object(V,I) & ~ on(V,W,I) ) => ~ on(V,W,s(I)) ) ) ) )). % All( v, block, ! member( v, fixed), % All( w, block, ! eql( v, w), % Disj( % L2("destination", w, i); % L3("on", v, w, i); % Not( L3("on", v, w, 1 + i))))); fof(non_destination_remains_not_on,axiom, ( ! [I,V] : ( nonfixed(V) => ! [W] : ( ( a_block(W) & neq(V,W) ) => ( ( time(I) & ~ destination(W,I) & ~ on(V,W,I) ) => ~ on(V,W,s(I)) ) ) ) )). fof(only_one_object_block,axiom, ( ! [I,X1] : ( nonfixed(X1) => ! [X2] : ( ( a_block(X2) & neq(X1,X2) ) => ~ ( object(X1,I) & object(X2,I) ) ) ) )). % All( y1, block, 1, % All( y2, block, ! eql( y1, y2), % Disj( % Not( L2("source", y1, i)); % Not( L2("source", y2, i))))); fof(only_one_source_block,axiom, ( ! [I,Y1] : ( a_block(Y1) => ! [Y2] : ( ( a_block(Y2) & neq(Y1,Y2) ) => ~ ( source(Y1,I) & source(Y2,I) ) ) ) )). % All( z1, block, 1, % All( z2, block, ! eql( z1, z2), % Disj( % Not( L2("destination", z1, i)); % Not( L2("destination", z2, i))))); fof(only_one_destination_block,axiom, ( ! [I,Z1] : ( a_block(Z1) => ! [Z2] : ( ( a_block(Z2) & neq(Z1,Z2) ) => ~ ( destination(Z1,I) & destination(Z2,I) ) ) ) )). fof(object_is_not_source,axiom, ( ! [I,X] : ( nonfixed(X) => ~ ( object(X,I) & source(X,I) ) ) )). % All( x, block, ! member( x, fixed), % Disj( % Not( L2("object", x, i)); % Not( L2("destination", x, i)))); fof(object_is_not_destination,axiom, ( ! [I,X] : ( nonfixed(X) => ~ ( object(X,I) & destination(X,I) ) ) )). % All( y, block, y, % Disj( % Not( L2("source", y, i)); % Not( L2("destination", y, i)))); fof(source_is_not_destination,axiom, ( ! [I,Y] : ( a_block(Y) => ~ ( source(Y,I) & destination(Y,I) ) ) )). %% on_axioms: fof(not_on_each_other,axiom, ( ! [I,X] : ( a_block(X) => ! [Y] : ( ( a_block(Y) & neq(X,Y) ) => ~ ( on(X,Y,I) & on(Y,X,I) ) ) ) )). fof(not_on_self,axiom, ( ! [I,X] : ( a_block(X) => ~ on(X,X,I) ) )). fof(only_one_on,axiom, ( ! [I,X] : ( nonfixed(X) => ! [Y] : ( ( nonfixed(Y) & neq(X,Y) ) => ! [Z] : ( ( nonfixed(Z) & neq(X,Z) & neq(Y,Z) ) => ~ ( on(X,Y,I) & on(Z,Y,I) ) ) ) ) )). fof(only_on_one_thing,axiom, ( ! [I,X] : ( nonfixed(X) => ! [Y] : ( ( a_block(Y) & neq(X,Y) ) => ! [Z] : ( ( a_block(Z) & neq(X,Z) & neq(Y,Z) ) => ~ ( on(X,Y,I) & on(X,Z,I) ) ) ) ) )). fof(not_clear_if_something_on,axiom, ( ! [I,X] : ( nonfixed(X) => ! [Y] : ( nonfixed(Y) => ~ ( on(X,Y,I) & clear(Y,I) ) ) ) )). fof(fixed_not_on_anything,axiom, ( ! [I,X] : ( a_block(X) => ! [Y] : ( fixed(Y) => ~ on(Y,X,I) ) ) )). %--------------------------------------------------------------------------