%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : GRA001-1 : TPTP v3.4.2. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : faust %s
% Computer : art06.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2794MHz
% Memory : 1003MB
% OS : Linux 2.6.11-1.1369_FC4
% CPULimit : 600s
% DateTime : Wed May 6 12:15:58 EDT 2009
% Result : Unsatisfiable 0.2s
% Output : Refutation 0.2s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 12
% Syntax : Number of formulae : 40 ( 5 unt; 0 def)
% Number of atoms : 93 ( 0 equ)
% Maximal formula atoms : 3 ( 2 avg)
% Number of connectives : 92 ( 39 ~; 53 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Maximal term depth : 0 ( 0 avg)
% Number of predicates : 6 ( 5 usr; 6 prp; 0-0 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Faust---1.0 format not known, defaulting to TPTP
fof(clause_5,plain,
( ~ a
| c
| d ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),
[] ).
cnf(149188656,plain,
( ~ a
| c
| d ),
inference(rewrite,[status(thm)],[clause_5]),
[] ).
fof(clause_1,plain,
( a
| b ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),
[] ).
cnf(149163272,plain,
( a
| b ),
inference(rewrite,[status(thm)],[clause_1]),
[] ).
cnf(185905504,plain,
( c
| d
| b ),
inference(resolution,[status(thm)],[149188656,149163272]),
[] ).
fof(clause_8,plain,
( b
| ~ c
| e ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),
[] ).
cnf(149209232,plain,
( b
| ~ c
| e ),
inference(rewrite,[status(thm)],[clause_8]),
[] ).
fof(clause_11,plain,
( d
| ~ e ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),
[] ).
cnf(149233544,plain,
( d
| ~ e ),
inference(rewrite,[status(thm)],[clause_11]),
[] ).
cnf(185968488,plain,
( b
| d ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[185905504,149209232,149233544]),
[] ).
fof(clause_2,plain,
( ~ a
| ~ b ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),
[] ).
cnf(149169760,plain,
( ~ a
| ~ b ),
inference(rewrite,[status(thm)],[clause_2]),
[] ).
cnf(185998792,plain,
( d
| ~ a ),
inference(resolution,[status(thm)],[185968488,149169760]),
[] ).
fof(clause_6,plain,
( ~ a
| ~ c
| ~ d ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),
[] ).
cnf(149195080,plain,
( ~ a
| ~ c
| ~ d ),
inference(rewrite,[status(thm)],[clause_6]),
[] ).
fof(clause_9,plain,
( ~ b
| c
| e ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),
[] ).
cnf(149221104,plain,
( ~ b
| c
| e ),
inference(rewrite,[status(thm)],[clause_9]),
[] ).
fof(clause_7,plain,
( b
| c
| ~ e ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),
[] ).
cnf(149202800,plain,
( b
| c
| ~ e ),
inference(rewrite,[status(thm)],[clause_7]),
[] ).
fof(clause_12,plain,
( ~ d
| e ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),
[] ).
cnf(149239856,plain,
( ~ d
| e ),
inference(rewrite,[status(thm)],[clause_12]),
[] ).
cnf(185932792,plain,
( b
| c ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[185905504,149202800,149239856]),
[] ).
cnf(186039640,plain,
( c
| e ),
inference(resolution,[status(thm)],[149221104,185932792]),
[] ).
cnf(185914888,plain,
( ~ a
| c
| e ),
inference(resolution,[status(thm)],[149188656,149239856]),
[] ).
cnf(185938896,plain,
( c
| ~ a ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[185914888,149202800,149169760]),
[] ).
fof(clause_3,plain,
( a
| c
| ~ d ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),
[] ).
cnf(149176032,plain,
( a
| c
| ~ d ),
inference(rewrite,[status(thm)],[clause_3]),
[] ).
cnf(185946672,plain,
( c
| ~ d ),
inference(resolution,[status(thm)],[185938896,149176032]),
[] ).
cnf(185952824,plain,
( c
| ~ e ),
inference(resolution,[status(thm)],[185946672,149233544]),
[] ).
cnf(186052456,plain,
c,
inference(resolution,[status(thm)],[186039640,185952824]),
[] ).
cnf(186136464,plain,
~ a,
inference(forward_subsumption_resolution__resolution,[status(thm)],[185998792,149195080,186052456]),
[] ).
cnf(186140896,plain,
b,
inference(resolution,[status(thm)],[186136464,149163272]),
[] ).
fof(clause_4,plain,
( a
| ~ c
| d ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),
[] ).
cnf(149182496,plain,
( a
| ~ c
| d ),
inference(rewrite,[status(thm)],[clause_4]),
[] ).
cnf(186018376,plain,
( d
| ~ c ),
inference(resolution,[status(thm)],[185998792,149182496]),
[] ).
cnf(186057744,plain,
( e
| d ),
inference(resolution,[status(thm)],[186039640,186018376]),
[] ).
cnf(186068440,plain,
e,
inference(resolution,[status(thm)],[186057744,149239856]),
[] ).
fof(clause_10,plain,
( ~ b
| ~ c
| ~ e ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),
[] ).
cnf(149159440,plain,
( ~ b
| ~ c
| ~ e ),
inference(rewrite,[status(thm)],[clause_10]),
[] ).
cnf(contradiction,plain,
$false,
inference(forward_subsumption_resolution__resolution,[status(thm)],[186140896,186068440,149159440,186052456]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 0 seconds
% START OF PROOF SEQUENCE
% fof(clause_5,plain,(~a|c|d),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),[]).
%
% cnf(149188656,plain,(~a|c|d),inference(rewrite,[status(thm)],[clause_5]),[]).
%
% fof(clause_1,plain,(a|b),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),[]).
%
% cnf(149163272,plain,(a|b),inference(rewrite,[status(thm)],[clause_1]),[]).
%
% cnf(185905504,plain,(c|d|b),inference(resolution,[status(thm)],[149188656,149163272]),[]).
%
% fof(clause_8,plain,(b|~c|e),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),[]).
%
% cnf(149209232,plain,(b|~c|e),inference(rewrite,[status(thm)],[clause_8]),[]).
%
% fof(clause_11,plain,(d|~e),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),[]).
%
% cnf(149233544,plain,(d|~e),inference(rewrite,[status(thm)],[clause_11]),[]).
%
% cnf(185968488,plain,(b|d),inference(forward_subsumption_resolution__resolution,[status(thm)],[185905504,149209232,149233544]),[]).
%
% fof(clause_2,plain,(~a|~b),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),[]).
%
% cnf(149169760,plain,(~a|~b),inference(rewrite,[status(thm)],[clause_2]),[]).
%
% cnf(185998792,plain,(d|~a),inference(resolution,[status(thm)],[185968488,149169760]),[]).
%
% fof(clause_6,plain,(~a|~c|~d),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),[]).
%
% cnf(149195080,plain,(~a|~c|~d),inference(rewrite,[status(thm)],[clause_6]),[]).
%
% fof(clause_9,plain,(~b|c|e),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),[]).
%
% cnf(149221104,plain,(~b|c|e),inference(rewrite,[status(thm)],[clause_9]),[]).
%
% fof(clause_7,plain,(b|c|~e),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),[]).
%
% cnf(149202800,plain,(b|c|~e),inference(rewrite,[status(thm)],[clause_7]),[]).
%
% fof(clause_12,plain,(~d|e),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),[]).
%
% cnf(149239856,plain,(~d|e),inference(rewrite,[status(thm)],[clause_12]),[]).
%
% cnf(185932792,plain,(b|c),inference(forward_subsumption_resolution__resolution,[status(thm)],[185905504,149202800,149239856]),[]).
%
% cnf(186039640,plain,(c|e),inference(resolution,[status(thm)],[149221104,185932792]),[]).
%
% cnf(185914888,plain,(~a|c|e),inference(resolution,[status(thm)],[149188656,149239856]),[]).
%
% cnf(185938896,plain,(c|~a),inference(forward_subsumption_resolution__resolution,[status(thm)],[185914888,149202800,149169760]),[]).
%
% fof(clause_3,plain,(a|c|~d),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),[]).
%
% cnf(149176032,plain,(a|c|~d),inference(rewrite,[status(thm)],[clause_3]),[]).
%
% cnf(185946672,plain,(c|~d),inference(resolution,[status(thm)],[185938896,149176032]),[]).
%
% cnf(185952824,plain,(c|~e),inference(resolution,[status(thm)],[185946672,149233544]),[]).
%
% cnf(186052456,plain,(c),inference(resolution,[status(thm)],[186039640,185952824]),[]).
%
% cnf(186136464,plain,(~a),inference(forward_subsumption_resolution__resolution,[status(thm)],[185998792,149195080,186052456]),[]).
%
% cnf(186140896,plain,(b),inference(resolution,[status(thm)],[186136464,149163272]),[]).
%
% fof(clause_4,plain,(a|~c|d),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),[]).
%
% cnf(149182496,plain,(a|~c|d),inference(rewrite,[status(thm)],[clause_4]),[]).
%
% cnf(186018376,plain,(d|~c),inference(resolution,[status(thm)],[185998792,149182496]),[]).
%
% cnf(186057744,plain,(e|d),inference(resolution,[status(thm)],[186039640,186018376]),[]).
%
% cnf(186068440,plain,(e),inference(resolution,[status(thm)],[186057744,149239856]),[]).
%
% fof(clause_10,plain,(~b|~c|~e),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/GRA/GRA001-1.tptp',unknown),[]).
%
% cnf(149159440,plain,(~b|~c|~e),inference(rewrite,[status(thm)],[clause_10]),[]).
%
% cnf(contradiction,plain,$false,inference(forward_subsumption_resolution__resolution,[status(thm)],[186140896,186068440,149159440,186052456]),[]).
%
% END OF PROOF SEQUENCE
%
%------------------------------------------------------------------------------