%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : PLA003-1 : TPTP v3.4.2. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : faust %s
% Computer : art05.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 1003MB
% OS : Linux 2.6.17-1.2142_FC4
% CPULimit : 600s
% DateTime : Wed May 6 15:07:48 EDT 2009
% Result : Unsatisfiable 0.1s
% Output : Refutation 0.1s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 8
% Syntax : Number of formulae : 25 ( 12 unt; 0 def)
% Number of atoms : 38 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 29 ( 16 ~; 13 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-3 aty)
% Number of variables : 58 ( 12 sgn 23 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Faust---1.0 format not known, defaulting to TPTP
fof(climb_up,plain,
! [A,B] :
( can(monkey(A,ceiling,nothing),ladder(A,floor),B)
| ~ can(monkey(A,floor,nothing),ladder(A,floor),B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/PLA/PLA003-1.tptp',unknown),
[] ).
cnf(167789120,plain,
( can(monkey(A,ceiling,nothing),ladder(A,floor),B)
| ~ can(monkey(A,floor,nothing),ladder(A,floor),B) ),
inference(rewrite,[status(thm)],[climb_up]),
[] ).
fof(go_holding_nothing,plain,
! [A,B,C,D] :
( can(monkey(A,floor,nothing),B,C)
| ~ can(monkey(D,floor,nothing),B,C) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/PLA/PLA003-1.tptp',unknown),
[] ).
cnf(167828704,plain,
( can(monkey(A,floor,nothing),B,C)
| ~ can(monkey(D,floor,nothing),B,C) ),
inference(rewrite,[status(thm)],[go_holding_nothing]),
[] ).
cnf(175828592,plain,
( can(monkey(A,ceiling,nothing),ladder(A,floor),B)
| ~ can(monkey(C,floor,nothing),ladder(A,floor),B) ),
inference(resolution,[status(thm)],[167789120,167828704]),
[] ).
fof(grab_ladder,plain,
! [A,B,C] :
( can(monkey(A,B,the_ladder),ladder(A,B),C)
| ~ can(monkey(A,B,nothing),ladder(A,B),C) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/PLA/PLA003-1.tptp',unknown),
[] ).
cnf(167875048,plain,
( can(monkey(A,B,the_ladder),ladder(A,B),C)
| ~ can(monkey(A,B,nothing),ladder(A,B),C) ),
inference(rewrite,[status(thm)],[grab_ladder]),
[] ).
fof(initial_situation,plain,
can(monkey(l0,floor,nothing),ladder(l1,floor),bananas(l2,ceiling)),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/PLA/PLA003-1.tptp',unknown),
[] ).
cnf(167878912,plain,
can(monkey(l0,floor,nothing),ladder(l1,floor),bananas(l2,ceiling)),
inference(rewrite,[status(thm)],[initial_situation]),
[] ).
cnf(175782232,plain,
can(monkey(A,floor,nothing),ladder(l1,floor),bananas(l2,ceiling)),
inference(resolution,[status(thm)],[167828704,167878912]),
[] ).
cnf(176032208,plain,
can(monkey(l1,floor,the_ladder),ladder(l1,floor),bananas(l2,ceiling)),
inference(resolution,[status(thm)],[167875048,175782232]),
[] ).
fof(go_holding_ladder,plain,
! [A,B,C] :
( can(monkey(A,floor,the_ladder),ladder(A,floor),B)
| ~ can(monkey(C,floor,the_ladder),ladder(C,floor),B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/PLA/PLA003-1.tptp',unknown),
[] ).
cnf(167804752,plain,
( can(monkey(A,floor,the_ladder),ladder(A,floor),B)
| ~ can(monkey(C,floor,the_ladder),ladder(C,floor),B) ),
inference(rewrite,[status(thm)],[go_holding_ladder]),
[] ).
cnf(176107328,plain,
can(monkey(A,floor,the_ladder),ladder(A,floor),bananas(l2,ceiling)),
inference(resolution,[status(thm)],[176032208,167804752]),
[] ).
fof(drop_ladder,plain,
! [A,B,C,D] :
( can(monkey(A,B,nothing),ladder(A,floor),C)
| ~ can(monkey(A,B,the_ladder),ladder(A,D),C) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/PLA/PLA003-1.tptp',unknown),
[] ).
cnf(167853312,plain,
( can(monkey(A,B,nothing),ladder(A,floor),C)
| ~ can(monkey(A,B,the_ladder),ladder(A,D),C) ),
inference(rewrite,[status(thm)],[drop_ladder]),
[] ).
cnf(176129720,plain,
can(monkey(A,floor,nothing),ladder(A,floor),bananas(l2,ceiling)),
inference(resolution,[status(thm)],[176107328,167853312]),
[] ).
cnf(176147136,plain,
can(monkey(B,floor,nothing),ladder(A,floor),bananas(l2,ceiling)),
inference(resolution,[status(thm)],[176129720,167828704]),
[] ).
cnf(176204424,plain,
can(monkey(A,ceiling,nothing),ladder(A,floor),bananas(l2,ceiling)),
inference(resolution,[status(thm)],[175828592,176147136]),
[] ).
fof(grab_bananas,plain,
! [A,B,C] :
( can(monkey(A,B,the_bananas),C,bananas(A,B))
| ~ can(monkey(A,B,nothing),C,bananas(A,B)) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/PLA/PLA003-1.tptp',unknown),
[] ).
cnf(167869240,plain,
( can(monkey(A,B,the_bananas),C,bananas(A,B))
| ~ can(monkey(A,B,nothing),C,bananas(A,B)) ),
inference(rewrite,[status(thm)],[grab_bananas]),
[] ).
fof(prove_the_monkey_can_get_the_bananas,plain,
! [A,B,C,D] : ~ can(monkey(A,B,the_bananas),C,D),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/PLA/PLA003-1.tptp',unknown),
[] ).
cnf(167888168,plain,
~ can(monkey(A,B,the_bananas),C,D),
inference(rewrite,[status(thm)],[prove_the_monkey_can_get_the_bananas]),
[] ).
cnf(175693360,plain,
~ can(monkey(A,B,nothing),C,bananas(A,B)),
inference(resolution,[status(thm)],[167869240,167888168]),
[] ).
cnf(contradiction,plain,
$false,
inference(resolution,[status(thm)],[176204424,175693360]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 0 seconds
% START OF PROOF SEQUENCE
% fof(climb_up,plain,(can(monkey(A,ceiling,nothing),ladder(A,floor),B)|~can(monkey(A,floor,nothing),ladder(A,floor),B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/PLA/PLA003-1.tptp',unknown),[]).
%
% cnf(167789120,plain,(can(monkey(A,ceiling,nothing),ladder(A,floor),B)|~can(monkey(A,floor,nothing),ladder(A,floor),B)),inference(rewrite,[status(thm)],[climb_up]),[]).
%
% fof(go_holding_nothing,plain,(can(monkey(A,floor,nothing),B,C)|~can(monkey(D,floor,nothing),B,C)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/PLA/PLA003-1.tptp',unknown),[]).
%
% cnf(167828704,plain,(can(monkey(A,floor,nothing),B,C)|~can(monkey(D,floor,nothing),B,C)),inference(rewrite,[status(thm)],[go_holding_nothing]),[]).
%
% cnf(175828592,plain,(can(monkey(A,ceiling,nothing),ladder(A,floor),B)|~can(monkey(C,floor,nothing),ladder(A,floor),B)),inference(resolution,[status(thm)],[167789120,167828704]),[]).
%
% fof(grab_ladder,plain,(can(monkey(A,B,the_ladder),ladder(A,B),C)|~can(monkey(A,B,nothing),ladder(A,B),C)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/PLA/PLA003-1.tptp',unknown),[]).
%
% cnf(167875048,plain,(can(monkey(A,B,the_ladder),ladder(A,B),C)|~can(monkey(A,B,nothing),ladder(A,B),C)),inference(rewrite,[status(thm)],[grab_ladder]),[]).
%
% fof(initial_situation,plain,(can(monkey(l0,floor,nothing),ladder(l1,floor),bananas(l2,ceiling))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/PLA/PLA003-1.tptp',unknown),[]).
%
% cnf(167878912,plain,(can(monkey(l0,floor,nothing),ladder(l1,floor),bananas(l2,ceiling))),inference(rewrite,[status(thm)],[initial_situation]),[]).
%
% cnf(175782232,plain,(can(monkey(A,floor,nothing),ladder(l1,floor),bananas(l2,ceiling))),inference(resolution,[status(thm)],[167828704,167878912]),[]).
%
% cnf(176032208,plain,(can(monkey(l1,floor,the_ladder),ladder(l1,floor),bananas(l2,ceiling))),inference(resolution,[status(thm)],[167875048,175782232]),[]).
%
% fof(go_holding_ladder,plain,(can(monkey(A,floor,the_ladder),ladder(A,floor),B)|~can(monkey(C,floor,the_ladder),ladder(C,floor),B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/PLA/PLA003-1.tptp',unknown),[]).
%
% cnf(167804752,plain,(can(monkey(A,floor,the_ladder),ladder(A,floor),B)|~can(monkey(C,floor,the_ladder),ladder(C,floor),B)),inference(rewrite,[status(thm)],[go_holding_ladder]),[]).
%
% cnf(176107328,plain,(can(monkey(A,floor,the_ladder),ladder(A,floor),bananas(l2,ceiling))),inference(resolution,[status(thm)],[176032208,167804752]),[]).
%
% fof(drop_ladder,plain,(can(monkey(A,B,nothing),ladder(A,floor),C)|~can(monkey(A,B,the_ladder),ladder(A,D),C)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/PLA/PLA003-1.tptp',unknown),[]).
%
% cnf(167853312,plain,(can(monkey(A,B,nothing),ladder(A,floor),C)|~can(monkey(A,B,the_ladder),ladder(A,D),C)),inference(rewrite,[status(thm)],[drop_ladder]),[]).
%
% cnf(176129720,plain,(can(monkey(A,floor,nothing),ladder(A,floor),bananas(l2,ceiling))),inference(resolution,[status(thm)],[176107328,167853312]),[]).
%
% cnf(176147136,plain,(can(monkey(B,floor,nothing),ladder(A,floor),bananas(l2,ceiling))),inference(resolution,[status(thm)],[176129720,167828704]),[]).
%
% cnf(176204424,plain,(can(monkey(A,ceiling,nothing),ladder(A,floor),bananas(l2,ceiling))),inference(resolution,[status(thm)],[175828592,176147136]),[]).
%
% fof(grab_bananas,plain,(can(monkey(A,B,the_bananas),C,bananas(A,B))|~can(monkey(A,B,nothing),C,bananas(A,B))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/PLA/PLA003-1.tptp',unknown),[]).
%
% cnf(167869240,plain,(can(monkey(A,B,the_bananas),C,bananas(A,B))|~can(monkey(A,B,nothing),C,bananas(A,B))),inference(rewrite,[status(thm)],[grab_bananas]),[]).
%
% fof(prove_the_monkey_can_get_the_bananas,plain,(~can(monkey(A,B,the_bananas),C,D)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/PLA/PLA003-1.tptp',unknown),[]).
%
% cnf(167888168,plain,(~can(monkey(A,B,the_bananas),C,D)),inference(rewrite,[status(thm)],[prove_the_monkey_can_get_the_bananas]),[]).
%
% cnf(175693360,plain,(~can(monkey(A,B,nothing),C,bananas(A,B))),inference(resolution,[status(thm)],[167869240,167888168]),[]).
%
% cnf(contradiction,plain,$false,inference(resolution,[status(thm)],[176204424,175693360]),[]).
%
% END OF PROOF SEQUENCE
%
%------------------------------------------------------------------------------