%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : COL098-1 : TPTP v3.4.2. Released v2.7.0.
% Transfm : none
% Format : tptp
% Command : faust %s
% Computer : art01.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 11:34:24 EDT 2009
% Result : Unsatisfiable 1.7s
% Output : Refutation 1.7s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 10
% Syntax : Number of formulae : 30 ( 13 unt; 0 def)
% Number of atoms : 55 ( 0 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 52 ( 27 ~; 25 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-3 aty)
% Number of variables : 37 ( 1 sgn 17 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Faust---1.0 format not known, defaulting to TPTP
fof(diamond_strip_lemmaD_2h2,plain,
! [A,B,C] :
( ~ member(pair(A,B),r)
| ~ member(pair(A,C),r)
| member(pair(C,sk1(A,B,C)),r) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/COL/COL098-1.tptp',unknown),
[] ).
cnf(173562616,plain,
( ~ member(pair(A,B),r)
| ~ member(pair(A,C),r)
| member(pair(C,sk1(A,B,C)),r) ),
inference(rewrite,[status(thm)],[diamond_strip_lemmaD_2h2]),
[] ).
fof(diamond_strip_lemmaD_2h4,plain,
member(pair(y,z),r),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/COL/COL098-1.tptp',unknown),
[] ).
cnf(173575200,plain,
member(pair(y,z),r),
inference(rewrite,[status(thm)],[diamond_strip_lemmaD_2h4]),
[] ).
cnf(184284752,plain,
( ~ member(pair(y,A),r)
| member(pair(z,sk1(y,A,z)),r) ),
inference(resolution,[status(thm)],[173562616,173575200]),
[] ).
fof(diamond_strip_lemmaD_2h6,plain,
! [A] :
( ~ member(pair(x,A),r)
| member(pair(y,sk2(A)),r) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/COL/COL098-1.tptp',unknown),
[] ).
cnf(173584968,plain,
( ~ member(pair(x,A),r)
| member(pair(y,sk2(A)),r) ),
inference(rewrite,[status(thm)],[diamond_strip_lemmaD_2h6]),
[] ).
fof(diamond_strip_lemmaD_2c1,plain,
member(pair(x,sk3),r),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/COL/COL098-1.tptp',unknown),
[] ).
cnf(173588688,plain,
member(pair(x,sk3),r),
inference(rewrite,[status(thm)],[diamond_strip_lemmaD_2c1]),
[] ).
cnf(184313144,plain,
member(pair(y,sk2(sk3)),r),
inference(resolution,[status(thm)],[173584968,173588688]),
[] ).
cnf(188439896,plain,
member(pair(z,sk1(y,sk2(sk3),z)),r),
inference(resolution,[status(thm)],[184284752,184313144]),
[] ).
fof(diamond_strip_lemmaD_2c2,plain,
! [A] :
( ~ member(pair(sk3,A),trancl(r))
| ~ member(pair(z,A),r) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/COL/COL098-1.tptp',unknown),
[] ).
cnf(173598448,plain,
( ~ member(pair(sk3,A),trancl(r))
| ~ member(pair(z,A),r) ),
inference(rewrite,[status(thm)],[diamond_strip_lemmaD_2c2]),
[] ).
fof(trans_trancl,plain,
! [A] : trans(trancl(A)),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/COL/COL098-1.tptp',unknown),
[] ).
cnf(173504040,plain,
trans(trancl(A)),
inference(rewrite,[status(thm)],[trans_trancl]),
[] ).
fof(transD,plain,
! [A,B,C,D] :
( ~ trans(A)
| ~ member(pair(B,C),A)
| ~ member(pair(C,D),A)
| member(pair(B,D),A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/COL/COL098-1.tptp',unknown),
[] ).
cnf(173514352,plain,
( ~ trans(A)
| ~ member(pair(B,C),A)
| ~ member(pair(C,D),A)
| member(pair(B,D),A) ),
inference(rewrite,[status(thm)],[transD]),
[] ).
fof(diamond_strip_lemmaD_2h5,plain,
! [A] :
( ~ member(pair(x,A),r)
| member(pair(A,sk2(A)),trancl(r)) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/COL/COL098-1.tptp',unknown),
[] ).
cnf(173580896,plain,
( ~ member(pair(x,A),r)
| member(pair(A,sk2(A)),trancl(r)) ),
inference(rewrite,[status(thm)],[diamond_strip_lemmaD_2h5]),
[] ).
cnf(184333360,plain,
member(pair(sk3,sk2(sk3)),trancl(r)),
inference(resolution,[status(thm)],[173580896,173588688]),
[] ).
cnf(184550376,plain,
( ~ member(pair(sk2(sk3),A),trancl(r))
| member(pair(sk3,A),trancl(r)) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[173504040,173514352,184333360]),
[] ).
fof(r_into_trancl,plain,
! [A,B,C] :
( ~ member(pair(A,B),C)
| member(pair(A,B),trancl(C)) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/COL/COL098-1.tptp',unknown),
[] ).
cnf(173494912,plain,
( ~ member(pair(A,B),C)
| member(pair(A,B),trancl(C)) ),
inference(rewrite,[status(thm)],[r_into_trancl]),
[] ).
fof(diamond_strip_lemmaD_2h1,plain,
! [A,B,C] :
( ~ member(pair(A,B),r)
| ~ member(pair(A,C),r)
| member(pair(B,sk1(A,B,C)),r) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/COL/COL098-1.tptp',unknown),
[] ).
cnf(173538344,plain,
( ~ member(pair(A,B),r)
| ~ member(pair(A,C),r)
| member(pair(B,sk1(A,B,C)),r) ),
inference(rewrite,[status(thm)],[diamond_strip_lemmaD_2h1]),
[] ).
cnf(184256664,plain,
( ~ member(pair(y,A),r)
| member(pair(A,sk1(y,A,z)),r) ),
inference(resolution,[status(thm)],[173538344,173575200]),
[] ).
cnf(188377440,plain,
member(pair(sk2(sk3),sk1(y,sk2(sk3),z)),r),
inference(resolution,[status(thm)],[184256664,184313144]),
[] ).
cnf(195280376,plain,
member(pair(sk2(sk3),sk1(y,sk2(sk3),z)),trancl(r)),
inference(resolution,[status(thm)],[173494912,188377440]),
[] ).
cnf(203998352,plain,
member(pair(sk3,sk1(y,sk2(sk3),z)),trancl(r)),
inference(resolution,[status(thm)],[184550376,195280376]),
[] ).
cnf(contradiction,plain,
$false,
inference(forward_subsumption_resolution__resolution,[status(thm)],[188439896,173598448,203998352]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 2 seconds
% START OF PROOF SEQUENCE
% fof(diamond_strip_lemmaD_2h2,plain,(~member(pair(A,B),r)|~member(pair(A,C),r)|member(pair(C,sk1(A,B,C)),r)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/COL/COL098-1.tptp',unknown),[]).
%
% cnf(173562616,plain,(~member(pair(A,B),r)|~member(pair(A,C),r)|member(pair(C,sk1(A,B,C)),r)),inference(rewrite,[status(thm)],[diamond_strip_lemmaD_2h2]),[]).
%
% fof(diamond_strip_lemmaD_2h4,plain,(member(pair(y,z),r)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/COL/COL098-1.tptp',unknown),[]).
%
% cnf(173575200,plain,(member(pair(y,z),r)),inference(rewrite,[status(thm)],[diamond_strip_lemmaD_2h4]),[]).
%
% cnf(184284752,plain,(~member(pair(y,A),r)|member(pair(z,sk1(y,A,z)),r)),inference(resolution,[status(thm)],[173562616,173575200]),[]).
%
% fof(diamond_strip_lemmaD_2h6,plain,(~member(pair(x,A),r)|member(pair(y,sk2(A)),r)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/COL/COL098-1.tptp',unknown),[]).
%
% cnf(173584968,plain,(~member(pair(x,A),r)|member(pair(y,sk2(A)),r)),inference(rewrite,[status(thm)],[diamond_strip_lemmaD_2h6]),[]).
%
% fof(diamond_strip_lemmaD_2c1,plain,(member(pair(x,sk3),r)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/COL/COL098-1.tptp',unknown),[]).
%
% cnf(173588688,plain,(member(pair(x,sk3),r)),inference(rewrite,[status(thm)],[diamond_strip_lemmaD_2c1]),[]).
%
% cnf(184313144,plain,(member(pair(y,sk2(sk3)),r)),inference(resolution,[status(thm)],[173584968,173588688]),[]).
%
% cnf(188439896,plain,(member(pair(z,sk1(y,sk2(sk3),z)),r)),inference(resolution,[status(thm)],[184284752,184313144]),[]).
%
% fof(diamond_strip_lemmaD_2c2,plain,(~member(pair(sk3,A),trancl(r))|~member(pair(z,A),r)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/COL/COL098-1.tptp',unknown),[]).
%
% cnf(173598448,plain,(~member(pair(sk3,A),trancl(r))|~member(pair(z,A),r)),inference(rewrite,[status(thm)],[diamond_strip_lemmaD_2c2]),[]).
%
% fof(trans_trancl,plain,(trans(trancl(A))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/COL/COL098-1.tptp',unknown),[]).
%
% cnf(173504040,plain,(trans(trancl(A))),inference(rewrite,[status(thm)],[trans_trancl]),[]).
%
% fof(transD,plain,(~trans(A)|~member(pair(B,C),A)|~member(pair(C,D),A)|member(pair(B,D),A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/COL/COL098-1.tptp',unknown),[]).
%
% cnf(173514352,plain,(~trans(A)|~member(pair(B,C),A)|~member(pair(C,D),A)|member(pair(B,D),A)),inference(rewrite,[status(thm)],[transD]),[]).
%
% fof(diamond_strip_lemmaD_2h5,plain,(~member(pair(x,A),r)|member(pair(A,sk2(A)),trancl(r))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/COL/COL098-1.tptp',unknown),[]).
%
% cnf(173580896,plain,(~member(pair(x,A),r)|member(pair(A,sk2(A)),trancl(r))),inference(rewrite,[status(thm)],[diamond_strip_lemmaD_2h5]),[]).
%
% cnf(184333360,plain,(member(pair(sk3,sk2(sk3)),trancl(r))),inference(resolution,[status(thm)],[173580896,173588688]),[]).
%
% cnf(184550376,plain,(~member(pair(sk2(sk3),A),trancl(r))|member(pair(sk3,A),trancl(r))),inference(forward_subsumption_resolution__resolution,[status(thm)],[173504040,173514352,184333360]),[]).
%
% fof(r_into_trancl,plain,(~member(pair(A,B),C)|member(pair(A,B),trancl(C))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/COL/COL098-1.tptp',unknown),[]).
%
% cnf(173494912,plain,(~member(pair(A,B),C)|member(pair(A,B),trancl(C))),inference(rewrite,[status(thm)],[r_into_trancl]),[]).
%
% fof(diamond_strip_lemmaD_2h1,plain,(~member(pair(A,B),r)|~member(pair(A,C),r)|member(pair(B,sk1(A,B,C)),r)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/COL/COL098-1.tptp',unknown),[]).
%
% cnf(173538344,plain,(~member(pair(A,B),r)|~member(pair(A,C),r)|member(pair(B,sk1(A,B,C)),r)),inference(rewrite,[status(thm)],[diamond_strip_lemmaD_2h1]),[]).
%
% cnf(184256664,plain,(~member(pair(y,A),r)|member(pair(A,sk1(y,A,z)),r)),inference(resolution,[status(thm)],[173538344,173575200]),[]).
%
% cnf(188377440,plain,(member(pair(sk2(sk3),sk1(y,sk2(sk3),z)),r)),inference(resolution,[status(thm)],[184256664,184313144]),[]).
%
% cnf(195280376,plain,(member(pair(sk2(sk3),sk1(y,sk2(sk3),z)),trancl(r))),inference(resolution,[status(thm)],[173494912,188377440]),[]).
%
% cnf(203998352,plain,(member(pair(sk3,sk1(y,sk2(sk3),z)),trancl(r))),inference(resolution,[status(thm)],[184550376,195280376]),[]).
%
% cnf(contradiction,plain,$false,inference(forward_subsumption_resolution__resolution,[status(thm)],[188439896,173598448,203998352]),[]).
%
% END OF PROOF SEQUENCE
%
%------------------------------------------------------------------------------