%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : KRS015-1 : TPTP v3.4.2. Released v2.0.0.
% Transfm : none
% Format : tptp
% Command : faust %s
% Computer : art08.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 13:24:55 EDT 2009
% Result : Unsatisfiable 0.1s
% Output : Refutation 0.1s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 11
% Syntax : Number of formulae : 36 ( 12 unt; 0 def)
% Number of atoms : 70 ( 0 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 71 ( 37 ~; 34 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 10 ( 9 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 1 con; 0-1 aty)
% Number of variables : 34 ( 0 sgn 15 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Faust---1.0 format not known, defaulting to TPTP
fof(clause_6,plain,
! [A] :
( t(A,u1r2(A))
| ~ t2least(A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS015-1.tptp',unknown),
[] ).
cnf(159555464,plain,
( t(A,u1r2(A))
| ~ t2least(A) ),
inference(rewrite,[status(thm)],[clause_6]),
[] ).
fof(clause_2,plain,
! [A] :
( t2least(A)
| ~ c(A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS015-1.tptp',unknown),
[] ).
cnf(159524496,plain,
( t2least(A)
| ~ c(A) ),
inference(rewrite,[status(thm)],[clause_2]),
[] ).
fof(clause_18,plain,
! [A,B] :
( c(A)
| ~ e(B)
| ~ r(B,A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS015-1.tptp',unknown),
[] ).
cnf(159658784,plain,
( c(A)
| ~ e(B)
| ~ r(B,A) ),
inference(rewrite,[status(thm)],[clause_18]),
[] ).
fof(clause_1,plain,
e(exist),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS015-1.tptp',unknown),
[] ).
cnf(159517456,plain,
e(exist),
inference(rewrite,[status(thm)],[clause_1]),
[] ).
cnf(167654144,plain,
( c(A)
| ~ r(exist,A) ),
inference(resolution,[status(thm)],[159658784,159517456]),
[] ).
fof(clause_14,plain,
! [A] :
( r(A,u4r4(A))
| ~ e(A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS015-1.tptp',unknown),
[] ).
cnf(159620664,plain,
( r(A,u4r4(A))
| ~ e(A) ),
inference(rewrite,[status(thm)],[clause_14]),
[] ).
cnf(167621736,plain,
r(exist,u4r4(exist)),
inference(resolution,[status(thm)],[159620664,159517456]),
[] ).
cnf(167681528,plain,
c(u4r4(exist)),
inference(resolution,[status(thm)],[167654144,167621736]),
[] ).
cnf(167704744,plain,
t2least(u4r4(exist)),
inference(resolution,[status(thm)],[159524496,167681528]),
[] ).
cnf(167740032,plain,
t(u4r4(exist),u1r2(u4r4(exist))),
inference(resolution,[status(thm)],[159555464,167704744]),
[] ).
fof(clause_8,plain,
! [A] :
( t1most(A)
| ~ d(A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS015-1.tptp',unknown),
[] ).
cnf(159574520,plain,
( t1most(A)
| ~ d(A) ),
inference(rewrite,[status(thm)],[clause_8]),
[] ).
fof(clause_17,plain,
! [A,B] :
( d(A)
| ~ e(B)
| ~ s(B,A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS015-1.tptp',unknown),
[] ).
cnf(159651872,plain,
( d(A)
| ~ e(B)
| ~ s(B,A) ),
inference(rewrite,[status(thm)],[clause_17]),
[] ).
cnf(167636744,plain,
( d(A)
| ~ s(exist,A) ),
inference(resolution,[status(thm)],[159651872,159517456]),
[] ).
fof(clause_15,plain,
! [A,B] :
( s(A,B)
| ~ e(A)
| ~ r(A,B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS015-1.tptp',unknown),
[] ).
cnf(159629336,plain,
( s(A,B)
| ~ e(A)
| ~ r(A,B) ),
inference(rewrite,[status(thm)],[clause_15]),
[] ).
cnf(167660976,plain,
( s(exist,A)
| ~ r(exist,A) ),
inference(resolution,[status(thm)],[159629336,159517456]),
[] ).
cnf(167689856,plain,
s(exist,u4r4(exist)),
inference(resolution,[status(thm)],[167660976,167621736]),
[] ).
cnf(167767720,plain,
d(u4r4(exist)),
inference(resolution,[status(thm)],[167636744,167689856]),
[] ).
cnf(167778424,plain,
t1most(u4r4(exist)),
inference(resolution,[status(thm)],[159574520,167767720]),
[] ).
fof(clause_10,plain,
! [A,B,C] :
( equalish(A,B)
| ~ t1most(C)
| ~ t(C,A)
| ~ t(C,B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS015-1.tptp',unknown),
[] ).
cnf(159591624,plain,
( equalish(A,B)
| ~ t1most(C)
| ~ t(C,A)
| ~ t(C,B) ),
inference(rewrite,[status(thm)],[clause_10]),
[] ).
fof(clause_5,plain,
! [A] :
( t(A,u1r1(A))
| ~ t2least(A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS015-1.tptp',unknown),
[] ).
cnf(159549376,plain,
( t(A,u1r1(A))
| ~ t2least(A) ),
inference(rewrite,[status(thm)],[clause_5]),
[] ).
cnf(167726864,plain,
t(u4r4(exist),u1r1(u4r4(exist))),
inference(resolution,[status(thm)],[159549376,167704744]),
[] ).
cnf(167833168,plain,
( equalish(A,u1r1(u4r4(exist)))
| ~ t(u4r4(exist),A) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[167778424,159591624,167726864]),
[] ).
fof(clause_4,plain,
! [A] :
( ~ t2least(A)
| ~ equalish(u1r2(A),u1r1(A)) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS015-1.tptp',unknown),
[] ).
cnf(159542408,plain,
( ~ t2least(A)
| ~ equalish(u1r2(A),u1r1(A)) ),
inference(rewrite,[status(thm)],[clause_4]),
[] ).
cnf(167755344,plain,
~ equalish(u1r2(u4r4(exist)),u1r1(u4r4(exist))),
inference(resolution,[status(thm)],[159542408,167704744]),
[] ).
cnf(contradiction,plain,
$false,
inference(forward_subsumption_resolution__resolution,[status(thm)],[167740032,167833168,167755344]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 0 seconds
% START OF PROOF SEQUENCE
% fof(clause_6,plain,(t(A,u1r2(A))|~t2least(A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS015-1.tptp',unknown),[]).
%
% cnf(159555464,plain,(t(A,u1r2(A))|~t2least(A)),inference(rewrite,[status(thm)],[clause_6]),[]).
%
% fof(clause_2,plain,(t2least(A)|~c(A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS015-1.tptp',unknown),[]).
%
% cnf(159524496,plain,(t2least(A)|~c(A)),inference(rewrite,[status(thm)],[clause_2]),[]).
%
% fof(clause_18,plain,(c(A)|~e(B)|~r(B,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS015-1.tptp',unknown),[]).
%
% cnf(159658784,plain,(c(A)|~e(B)|~r(B,A)),inference(rewrite,[status(thm)],[clause_18]),[]).
%
% fof(clause_1,plain,(e(exist)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS015-1.tptp',unknown),[]).
%
% cnf(159517456,plain,(e(exist)),inference(rewrite,[status(thm)],[clause_1]),[]).
%
% cnf(167654144,plain,(c(A)|~r(exist,A)),inference(resolution,[status(thm)],[159658784,159517456]),[]).
%
% fof(clause_14,plain,(r(A,u4r4(A))|~e(A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS015-1.tptp',unknown),[]).
%
% cnf(159620664,plain,(r(A,u4r4(A))|~e(A)),inference(rewrite,[status(thm)],[clause_14]),[]).
%
% cnf(167621736,plain,(r(exist,u4r4(exist))),inference(resolution,[status(thm)],[159620664,159517456]),[]).
%
% cnf(167681528,plain,(c(u4r4(exist))),inference(resolution,[status(thm)],[167654144,167621736]),[]).
%
% cnf(167704744,plain,(t2least(u4r4(exist))),inference(resolution,[status(thm)],[159524496,167681528]),[]).
%
% cnf(167740032,plain,(t(u4r4(exist),u1r2(u4r4(exist)))),inference(resolution,[status(thm)],[159555464,167704744]),[]).
%
% fof(clause_8,plain,(t1most(A)|~d(A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS015-1.tptp',unknown),[]).
%
% cnf(159574520,plain,(t1most(A)|~d(A)),inference(rewrite,[status(thm)],[clause_8]),[]).
%
% fof(clause_17,plain,(d(A)|~e(B)|~s(B,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS015-1.tptp',unknown),[]).
%
% cnf(159651872,plain,(d(A)|~e(B)|~s(B,A)),inference(rewrite,[status(thm)],[clause_17]),[]).
%
% cnf(167636744,plain,(d(A)|~s(exist,A)),inference(resolution,[status(thm)],[159651872,159517456]),[]).
%
% fof(clause_15,plain,(s(A,B)|~e(A)|~r(A,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS015-1.tptp',unknown),[]).
%
% cnf(159629336,plain,(s(A,B)|~e(A)|~r(A,B)),inference(rewrite,[status(thm)],[clause_15]),[]).
%
% cnf(167660976,plain,(s(exist,A)|~r(exist,A)),inference(resolution,[status(thm)],[159629336,159517456]),[]).
%
% cnf(167689856,plain,(s(exist,u4r4(exist))),inference(resolution,[status(thm)],[167660976,167621736]),[]).
%
% cnf(167767720,plain,(d(u4r4(exist))),inference(resolution,[status(thm)],[167636744,167689856]),[]).
%
% cnf(167778424,plain,(t1most(u4r4(exist))),inference(resolution,[status(thm)],[159574520,167767720]),[]).
%
% fof(clause_10,plain,(equalish(A,B)|~t1most(C)|~t(C,A)|~t(C,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS015-1.tptp',unknown),[]).
%
% cnf(159591624,plain,(equalish(A,B)|~t1most(C)|~t(C,A)|~t(C,B)),inference(rewrite,[status(thm)],[clause_10]),[]).
%
% fof(clause_5,plain,(t(A,u1r1(A))|~t2least(A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS015-1.tptp',unknown),[]).
%
% cnf(159549376,plain,(t(A,u1r1(A))|~t2least(A)),inference(rewrite,[status(thm)],[clause_5]),[]).
%
% cnf(167726864,plain,(t(u4r4(exist),u1r1(u4r4(exist)))),inference(resolution,[status(thm)],[159549376,167704744]),[]).
%
% cnf(167833168,plain,(equalish(A,u1r1(u4r4(exist)))|~t(u4r4(exist),A)),inference(forward_subsumption_resolution__resolution,[status(thm)],[167778424,159591624,167726864]),[]).
%
% fof(clause_4,plain,(~t2least(A)|~equalish(u1r2(A),u1r1(A))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/KRS/KRS015-1.tptp',unknown),[]).
%
% cnf(159542408,plain,(~t2least(A)|~equalish(u1r2(A),u1r1(A))),inference(rewrite,[status(thm)],[clause_4]),[]).
%
% cnf(167755344,plain,(~equalish(u1r2(u4r4(exist)),u1r1(u4r4(exist)))),inference(resolution,[status(thm)],[159542408,167704744]),[]).
%
% cnf(contradiction,plain,$false,inference(forward_subsumption_resolution__resolution,[status(thm)],[167740032,167833168,167755344]),[]).
%
% END OF PROOF SEQUENCE
%
%------------------------------------------------------------------------------